Regular cardinalhood is Pi-one definable (source code)

= Regular cardinalhood is Pi-one definable

An infinite <cardinal number> $\kappa$ is a <regular cardinal> if every function from an ordinal $\delta<\kappa$ into $\kappa$ has bounded range. Write this as $\forall f\,\forall\delta\in\kappa\,(\operatorname{Map}(f,\delta,\kappa)\Rightarrow\exists\beta\in\kappa\,\forall\xi\in\delta\ f(\xi)<\beta)$. The graph predicates are <bounded formulas in set theory>, and <cardinalhood is Pi-one definable>, so adding infinite cardinalhood yields a <Pi-one formula modulo ZF>.