= Solution
By the <natural-number recursion theorem>, let $\alpha_0=0$ and $\alpha_{n+1}=F(\alpha_n)$. These <ordinals> form a nondecreasing sequence by the preceding bound. If $\alpha_{n+1}=\alpha_n$ for some $n$, it is already a fixed point.
Otherwise the sequence is strictly increasing. Its supremum $\lambda=\bigcup_{n<\omega}\alpha_n$ is a <limit ordinal>, and the sequence is cofinal in it. Continuity and monotonicity give
$$
F(\lambda)=\sup_{\beta<\lambda}F(\beta)=\sup_{n<\omega}F(\alpha_n)=\sup_{n<\omega}\alpha_{n+1}=\lambda.
$$
For the middle equality, every $\beta<\lambda$ is below some $\alpha_n$, while every $\alpha_n<\lambda$. Therefore \b[$F$ has a fixed point]. The sequence is a set by <Axiom schema of replacement>, since $F$ is a definable <set-theoretic class function>.
Back to article page
