Countable fixed point of a normal ordinal function (source code)

= Countable fixed point of a normal ordinal function
{title2=$\alpha=\sup_{n<\omega}\Phi^n(0)$}

If a <normal function on an ordinal> begins at a <countable> value and preserves countability from $\Phi(\xi)$ to $\Phi(\xi+1)$, <transfinite induction> shows it maps all <countable ordinals> to <countable ordinals>. At <countable> limits this uses <countable> unions of <countable sets>, hence <axiom of countable choice> in the usual proof. Iteration from zero either stabilizes at a <countable> fixed point or has a <countable> limit fixed by continuity. Applying this to $\omega^\alpha$ gives the <countable> epsilon number $\epsilon_0$.