[proofplan] The strategy is to iterate $f$ countably many times starting from $\alpha$ and take the sup. Define $\alpha_0 = \alpha$, $\alpha_{n+1} = f(\alpha_n)$, and $\beta := \sup_{n < \omega} \alpha_n$. Two cases arise. If the sequence stabilises — some $\alpha_{n+1} = \alpha_n$ — then $\alpha_n$ is already a fixed point at or above $\alpha$. Otherwise the sequence is strictly increasing (by domination of the identity, see [Normal Functions are Strictly Increasing and Dominate the Identity](/theorems/1474)), so $\beta$ is a limit ordinal. Applying [preservation of suprema](/theorems/1475) — the defining continuity of normal functions in disguise — we compute $f(\beta) = \sup_n f(\alpha_n) = \sup_n \alpha_{n+1} = \beta$, using that shifting a sequence by one index preserves its supremum. [/proofplan] [step:Define the iteration sequence $\alpha_n$ recursively by $\alpha_{n+1} = f(\alpha_n)$] Define $(\alpha_n)_{n < \omega}$ by the recursion \begin{align*} \alpha_0 &= \alpha, \\ \alpha_{n+1} &= f(\alpha_n) \quad \text{for } n < \omega. \end{align*} This is a function $\omega \to \mathrm{Ord}$ defined by ordinary recursion on $\omega$, so no transfinite machinery is needed. By [$f(\gamma) \geq \gamma$ for every ordinal $\gamma$](/theorems/1474) applied at $\gamma = \alpha_n$, each step is non-decreasing: \begin{align*} \alpha_{n+1} = f(\alpha_n) \geq \alpha_n. \end{align*} Hence $(\alpha_n)$ is a weakly increasing sequence of ordinals. Define \begin{align*} \beta := \sup_{n < \omega} \alpha_n. \end{align*} Since $\alpha_0 = \alpha$ appears in the sequence, $\beta \geq \alpha_0 = \alpha$. It remains to show $f(\beta) = \beta$. [guided] The idea behind "iterate and take the sup" is a general recipe for manufacturing fixed points: any closure-like operator that pushes a point upward, when applied infinitely often, produces a value that is stable under one more application. Here $f$ is the operator and stability means $f(\beta) = \beta$. Formally, we recursively define a sequence by $\alpha_0 = \alpha$ and $\alpha_{n+1} = f(\alpha_n)$. The recursion runs over the natural numbers $\omega$, so it is ordinary recursion, not transfinite — this is the only place the use of $\omega$ is essential (we cannot iterate across arbitrary ordinals because we want the supremum to be a *limit of $\omega$-length sequence*, which is key in the final step). Why is $(\alpha_n)$ weakly increasing? We proved in [Normal Functions are Strictly Increasing and Dominate the Identity](/theorems/1474) that a normal function dominates the identity: $f(\gamma) \geq \gamma$ for every ordinal $\gamma$. Applying this with $\gamma = \alpha_n$: \begin{align*} \alpha_{n+1} = f(\alpha_n) \geq \alpha_n. \end{align*} The candidate fixed point is $\beta := \sup_n \alpha_n$, the supremum of the sequence. Since the sequence is weakly increasing, the supremum "tracks the limit" of the iteration. Note $\beta \geq \alpha_0 = \alpha$ automatically, handling the "$\beta \geq \alpha$" part of the claim — we need only establish $f(\beta) = \beta$. [/guided] [/step] [step:Handle the case where the sequence stabilises] Suppose there exists $n < \omega$ with $\alpha_{n+1} = \alpha_n$. Then $f(\alpha_n) = \alpha_{n+1} = \alpha_n$, so $\alpha_n$ is itself a fixed point of $f$. By the weakly-increasing property established above, $\alpha_m = \alpha_n$ for all $m \geq n$ (the sequence becomes constant after step $n$, since $\alpha_{m+1} = f(\alpha_m) \geq \alpha_m$, and in fact a standard induction on $m$ shows equality is maintained — but it suffices that no term exceeds $\alpha_n$ because monotonicity gives $\alpha_m \leq \alpha_n$ for $m \leq n$ and equality for $m \geq n$ is a consequence of $\alpha_{n+1} = \alpha_n$ propagating). More carefully: $\alpha_{n+1} = \alpha_n$ gives $\alpha_{n+2} = f(\alpha_{n+1}) = f(\alpha_n) = \alpha_{n+1} = \alpha_n$, and iterating by induction on $k$, $\alpha_{n+k} = \alpha_n$ for every $k \geq 0$. Consequently \begin{align*} \beta = \sup_{m < \omega} \alpha_m = \alpha_n, \end{align*} and $f(\beta) = f(\alpha_n) = \alpha_n = \beta$. The fixed-point property holds in this case, and $\beta = \alpha_n \geq \alpha_0 = \alpha$. [/step] [step:In the non-stabilising case, identify $\beta$ as a limit ordinal] Suppose $\alpha_{n+1} \neq \alpha_n$ for all $n < \omega$. Combined with $\alpha_{n+1} \geq \alpha_n$, this gives strict inequality: \begin{align*} \alpha_{n+1} > \alpha_n \quad \text{for all } n < \omega. \end{align*} Hence $(\alpha_n)$ is strictly increasing. We claim $\beta$ is a limit ordinal. If not, either $\beta = 0$ or $\beta$ is a successor. - **If $\beta = 0$:** then $\alpha_n \leq 0$ for every $n$, so $\alpha_0 = \alpha = 0$. But $\alpha_1 = f(\alpha_0) > \alpha_0 = 0$ by strictness, contradicting $\alpha_1 \leq \beta = 0$. - **If $\beta = \delta^+$:** then each $\alpha_n \leq \delta^+$, i.e. $\alpha_n < \delta^+$ or $\alpha_n = \delta^+$. Since $(\alpha_n)$ is strictly increasing and has no maximum (if $\alpha_N$ were the maximum, then $\alpha_{N+1} > \alpha_N$ would contradict maximality), each $\alpha_n$ is strictly less than the supremum $\beta$, so $\alpha_n < \delta^+$, which gives $\alpha_n \leq \delta$. Then $\delta$ is an upper bound for $(\alpha_n)$, so $\beta \leq \delta < \delta^+ = \beta$, a contradiction. Hence $\beta$ is a limit ordinal. [guided] In the non-stabilising case, we upgrade "$\alpha_{n+1} \neq \alpha_n$" and "$\alpha_{n+1} \geq \alpha_n$" to the strict inequality $\alpha_{n+1} > \alpha_n$. The weak inequality came from $f$ dominating the identity; strictness comes from our assumption that the sequence never plateaus. Once the sequence is strictly increasing, the sup $\beta$ of a strictly increasing $\omega$-length sequence is a limit ordinal. Let's verify: an ordinal is zero, a successor, or a limit, and we rule out the first two. - $\beta = 0$: would force every $\alpha_n \leq 0$, hence $\alpha_n = 0$ for all $n$, contradicting strictness (we'd need $\alpha_1 > \alpha_0 = 0$). - $\beta = \delta^+$: the strictly increasing sequence has no maximum (the $(n+1)$-th term always exceeds the $n$-th), so every $\alpha_n$ is strictly less than the sup, $\alpha_n < \delta^+$. On the ordinals, $\alpha_n < \delta^+$ is equivalent to $\alpha_n \leq \delta$, so $\delta$ would be an upper bound less than $\beta$ — contradicting minimality of $\beta$ as the least upper bound. Only the limit case remains. This matters because the definition of "continuous at limits" — the very property that makes $f$ normal — can now be applied at $\beta$. [/guided] [/step] [step:Apply supremum preservation to compute $f(\beta) = \beta$] Since $\beta$ is a limit ordinal and $(\alpha_n)_{n < \omega}$ is a non-empty family of ordinals with supremum $\beta$, we apply [Normal Functions Preserve All Suprema](/theorems/1475): \begin{align*} f(\beta) = f\!\left(\sup_{n < \omega} \alpha_n\right) = \sup_{n < \omega} f(\alpha_n) = \sup_{n < \omega} \alpha_{n+1}. \end{align*} The last sup is a reindexing of the sequence, and reindexing a sequence by one position preserves the supremum: \begin{align*} \sup_{n < \omega} \alpha_{n+1} = \sup_{n \geq 1} \alpha_n = \sup_{n < \omega} \alpha_n = \beta. \end{align*} The middle equality holds because dropping the single term $\alpha_0$ from a sequence can only decrease the supremum, and since $\alpha_0 \leq \alpha_1 \leq \sup_{n \geq 1} \alpha_n$, the supremum is unchanged. Hence $f(\beta) = \beta$, and by the previous steps $\beta \geq \alpha_0 = \alpha$. This completes the proof. [guided] With $\beta$ identified as a limit ordinal and $(\alpha_n)$ a non-empty family with supremum $\beta$, we may invoke [Normal Functions Preserve All Suprema](/theorems/1475). Theorem 1475 requires $f$ to be normal (our hypothesis) and the family to be non-empty (true — it contains $\alpha_0$). Both conditions check. Applying the theorem to the $\omega$-indexed family $(\alpha_n)_{n < \omega}$: \begin{align*} f(\beta) = f\!\left(\sup_{n < \omega} \alpha_n\right) = \sup_{n < \omega} f(\alpha_n). \end{align*} By definition of the sequence, $f(\alpha_n) = \alpha_{n+1}$. Substituting: \begin{align*} f(\beta) = \sup_{n < \omega} \alpha_{n+1}. \end{align*} Now the key observation: $\sup_{n < \omega} \alpha_{n+1}$ is the supremum of the sequence $\alpha_1, \alpha_2, \alpha_3, \ldots$ — the original sequence with the first term dropped. For a weakly increasing (indeed strictly increasing) sequence, dropping a single initial term never changes the supremum: the remaining terms have $\alpha_1$ as their smallest, and the $\alpha_0$ we dropped satisfies $\alpha_0 \leq \alpha_1$, so every upper bound of $\{\alpha_1, \alpha_2, \ldots\}$ is already an upper bound of $\{\alpha_0, \alpha_1, \ldots\}$. Hence: \begin{align*} \sup_{n < \omega} \alpha_{n+1} = \sup_{n < \omega} \alpha_n = \beta. \end{align*} Combining: $f(\beta) = \beta$. Together with $\beta \geq \alpha$ from the first step, this gives the required fixed point $\beta \geq \alpha$ with $f(\beta) = \beta$. The proof has produced an explicit construction — $\beta$ is the supremum of the forward orbit of $\alpha$ under $f$ — not merely an existence argument. This orbit-supremum idea recurs throughout ordinal analysis (e.g., the construction of $\varepsilon_0$ by iterating $\alpha \mapsto \omega^\alpha$). [/guided] [/step]