 Cardinalhood is Pi-one definable

An ordinal $\kappa$ is a cardinal number precisely when no smaller ordinal has a bijection onto it. Ordinalhood and the graph predicate for a bijection are bounded formulas in set theory, so $\mathrm{Ord}(\kappa )\wedge \forall f\forall \alpha \in \kappa \neg \mathrm{Bij}(f,\alpha ,\kappa )$ is a Pi-one formula modulo ZF. This does not assert that every set can be assigned an ordinal cardinal without the axiom of choice.