Solution (source code)

= Solution

For a <countable fixed point of a normal ordinal function>, first show that $\Phi$ maps every <countable ordinal> to a <countable ordinal>. Use <transfinite induction> below $\omega_1$. The zero case is assumed, and the successor case is the stated preservation property. If $\lambda$ is a <countable> limit, normality gives $\Phi(\lambda)=\bigcup_{\alpha<\lambda}\Phi(\alpha)$, a <countable union of countable sets>, hence <countable>. This countable-union step is where <axiom of countable choice> is used; the assumed <axiom of choice> supplies it.

Now set $\alpha_0=0$, $\alpha_{n+1}=\Phi(\alpha_n)$. The preceding result makes every term <countable>, and the domination proved earlier makes the <sequence> nondecreasing. If it ever stabilizes, it already gives the required fixed point. Otherwise $\alpha=\sup_{n<\omega}\alpha_n$ is a <countable> nonzero limit, using <axiom of countable choice> again for countability of the union. Its defining <sequence> is cofinal, so monotonicity and continuity give
$$
\boxed{\Phi(\alpha)=\sup_n\Phi(\alpha_n)=\sup_n\alpha_{n+1}=\alpha.}
$$
Apply this to $\Phi(\alpha)=\omega^\alpha$. This is normal, begins at $1$, and $\omega^{\alpha+1}=\omega^\alpha\cdot\omega$ is <countable> whenever $\omega^\alpha$ is <countable>. Thus a <countable> $\epsilon$ satisfies $\boxed{\epsilon=\omega^\epsilon}$. Starting at zero gives the familiar tower <sequence> $0,1,\omega,\omega^\omega,\ldots$, whose <supremum> is $\epsilon_0$. The finite recursion, <ordinal> identities and fixed-point continuity do not require choice; the uses of choice above concern <countable> unions of <countable ordinals>.