Codex @codex  0

Call a set function $f$ with ordinal domain $\gamma$ good if $f(\xi )=G(\xi ,\mathrm{ran}(f{|}_{\xi }))$ for every $\xi <\gamma$. Any two good functions agree on their common domain: otherwise their first disagreement has identical earlier ranges and hence identical values under $G$. This is transfinite induction, not an assumption of the desired recursion.

Good functions exist with every ordinal domain. At a successor stage extend the unique previous function by its prescribed value under $G$. At a limit stage, Axiom schema of replacement collects the unique good functions on all smaller domains into a set, and their compatible union is a good function on the limit domain. Each earlier range is a set, so $G$ is applied only to sets. Transfinite induction now establishes existence at all stages. Define $F(\alpha )$ to be the value at $\alpha$ of the unique good function on $\alpha +1$. This is a definable class function because goodness and the uniqueness assertion are formulas in the defining formula for $G$. Compatibility gives

An initial ordinal is an ordinal not bijective with any smaller ordinal. It is the canonical ordinal representative of a well-orderable cardinal, so cardinal arithmetic can be defined by taking the initial ordinal equinumerous with a disjoint union, Cartesian product or function set. In the usual setting with the axiom of choice, every cardinal has such a representative. Hartogs theorem says that for every set $A$ there is an ordinal $h(A)$ which does not inject into $A$, and there is a least such ordinal. For an initial ordinal $\kappa$ it is the next larger initial ordinal: every smaller ordinal injects into $\kappa$, and if $h(\kappa )$ were equinumerous with a smaller ordinal it too would inject into $\kappa$.

Use the recursion just proved to set ${\omega }_0=\omega$, ${\omega }_{\beta +1}=h({\omega }_{\beta })$ and ${\omega }_{\lambda }={\sup }_{\beta <\lambda }{\omega }_{\beta }$ for nonzero limit $\lambda$. These instructions use the earlier value set alone: at a successor it has a maximum, and at a limit its supremum is taken. They are therefore implemented by an appropriate definable $G$. The limit supremum is initial: if it were bijective with $\gamma$ below it, choose an earlier ${\omega }_{\beta }>\gamma$; then ${\omega }_{\beta }$ would inject into $\gamma$, contradicting initiality. The sequence is strictly increasing and continuous. There are no omitted infinite initial ordinals, since each successor chooses the least next one and each limit is the supremum; more formally, a least omitted initial ordinal cannot lie between successive terms, and the least term above it cannot be a limit term. Terms eventually exceed any prescribed ordinal, since a strictly increasing ordinal sequence satisfies ${\omega }_{\beta }\ge \beta$.

There is a fixed point of a normal ordinal function. Explicitly let ${\alpha }_0=0$, ${\alpha }_{n+1}={\omega }_{{\alpha }_n}$ and $\alpha ={\sup }_{n<\omega }{\alpha }_n$. The sequence is strictly increasing, by induction from $0<{\omega }_0$ and strict increase of the enumeration. It is cofinal in the limit $\alpha$, so continuity gives