Solution (source code)

= Solution

The <ordinal> operations are defined by <transfinite recursion> in the right argument. Addition satisfies $\alpha+0=\alpha$, $\alpha+(\beta+1)=(\alpha+\beta)+1$, and $\alpha+\lambda=\sup_{\beta<\lambda}(\alpha+\beta)$ at a nonzero limit. Multiplication satisfies $\alpha\cdot0=0$, $\alpha\cdot(\beta+1)=\alpha\cdot\beta+\alpha$, and $\alpha\cdot\lambda=\sup_{\beta<\lambda}\alpha\cdot\beta$. Exponentiation satisfies $\alpha^0=1$, $\alpha^{\beta+1}=\alpha^\beta\cdot\alpha$, and $\alpha^\lambda=\sup_{\beta<\lambda}\alpha^\beta$ at nonzero limits. These are <ordinal> operations, not commutative <cardinal arithmetic>.

For a <normal function on an ordinal>, prove domination by <transfinite induction>. At zero, $0\leq\Phi(0)$ automatically. If $\alpha\leq\Phi(\alpha)$, strict increase at successors gives $\alpha+1\leq\Phi(\alpha)+1\leq\Phi(\alpha+1)$. At a nonzero limit $\lambda$, continuity and the induction hypotheses give
$$
\Phi(\lambda)=\sup_{\alpha<\lambda}\Phi(\alpha)\geq\sup_{\alpha<\lambda}\alpha=\lambda.
$$
Therefore $\boxed{\alpha\leq\Phi(\alpha)\text{ for every ordinal }\alpha}$. No <axiom of choice> is needed for this <ordinal> induction.