Cardinalhood is Pi-one definable
= 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 $\operatorname{Ord}(\kappa)\land\forall f\,\forall\alpha\in\kappa\,\neg\operatorname{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>.