## Formalized Statement Let $f: \mathrm{Ord} \to \mathrm{Ord}$ be a normal function and let $\alpha \in \mathrm{Ord}$ satisfy $\alpha \geq f(0)$ (equivalently, the admissible set $A := \{\beta \in \mathrm{Ord} : f(\beta) \leq \alpha\}$ is non-empty). Then there exists a (unique) maximal ordinal $\gamma$ with \begin{align*} f(\gamma) \leq \alpha. \end{align*} [proofplan] We construct the maximal $\gamma$ explicitly as the supremum of the admissible set $A := \{\beta : f(\beta) \leq \alpha\}$, which is non-empty by the hypothesis $\alpha \geq f(0)$. The two ingredients we actually need are (i) [identity-domination](/theorems/1474), $f(\beta) \geq \beta$, which bounds $A$ above by $\alpha$ and so guarantees $\gamma := \sup A$ is a bona fide ordinal; and (ii) [sup-preservation for normal functions](/theorems/1475), which gives $f(\gamma) = \sup_{\beta \in A} f(\beta) \leq \alpha$, placing $\gamma$ itself inside $A$. Once $\gamma \in A$ and $\gamma$ is an upper bound of $A$, it is automatically the maximum. [/proofplan] [step:Define the admissible set and record its upper bound] Define \begin{align*} A := \{\beta \in \mathrm{Ord} : f(\beta) \leq \alpha\}. \end{align*} By hypothesis $\alpha \geq f(0)$, so $0 \in A$ and $A \neq \varnothing$. By [$f(\beta) \geq \beta$ for every ordinal](/theorems/1474), every $\beta \in A$ satisfies \begin{align*} \beta \leq f(\beta) \leq \alpha. \end{align*} Hence $\alpha$ is an upper bound for $A$. [guided] The admissible set $A = \{\beta : f(\beta) \leq \alpha\}$ collects every ordinal whose image under $f$ does not overshoot $\alpha$. We aim to show $A$ has a maximum, and our candidate for it is $\gamma := \sup A$. For this supremum to exist as an ordinal (rather than as a proper class), $A$ must be non-empty and bounded above. *Non-emptiness.* We check $0 \in A$: this is exactly the condition $f(0) \leq \alpha$, which is our hypothesis $\alpha \geq f(0)$. *Boundedness.* Here we use [identity-domination](/theorems/1474): for every ordinal $\beta$, $f(\beta) \geq \beta$. Applied to $\beta \in A$: \begin{align*} \beta \leq f(\beta) \leq \alpha, \end{align*} so $\alpha$ itself bounds $A$ from above. The strategy going forward: set $\gamma := \sup A$, show (a) $\gamma \in A$ via sup-preservation, and (b) $\gamma$ is an upper bound of $A$, so any $\delta > \gamma$ lies outside $A$. [/guided] [/step] [step:Form $\gamma := \sup A$ and verify it is a legitimate ordinal] Every non-empty class of ordinals that is bounded above has a supremum, obtained as the union of its elements. Since $A$ is non-empty and bounded above by $\alpha$, define \begin{align*} \gamma := \sup A. \end{align*} Then $\gamma$ is an ordinal with $\gamma \leq \alpha$, and $\gamma$ is the least upper bound of $A$. [guided] We now instantiate the ordinal $\gamma$. The construction $\gamma := \sup A$ is well-defined as an ordinal precisely because of the two facts established in the previous step: 1. $A \neq \varnothing$ — otherwise the supremum would be $0$ vacuously, but more importantly the subsequent application of sup-preservation requires a non-empty family. 2. $A$ is bounded above by $\alpha$ — otherwise $\sup A$ would escape to a proper class. With both conditions in hand, $\sup A$ is the least ordinal that is $\geq \beta$ for every $\beta \in A$. Concretely, $\gamma = \bigcup_{\beta \in A} \beta$ (union of transitive sets). Note that at this stage we do not yet know whether $\gamma \in A$. The supremum might or might not belong to the set it bounds; that is the content of the next step. [/guided] [/step] [step:Verify $\gamma \in A$ via supremum preservation] We show $f(\gamma) \leq \alpha$, i.e. $\gamma \in A$. Apply [Normal Functions Preserve All Suprema](/theorems/1475) to the non-empty family $A$. The theorem requires $f$ to be normal (given) and the family to be non-empty (established above); both hold. It yields \begin{align*} f(\gamma) = f(\sup A) = \sup_{\beta \in A} f(\beta). \end{align*} For every $\beta \in A$, by definition $f(\beta) \leq \alpha$. A supremum of ordinals each $\leq \alpha$ is itself $\leq \alpha$: \begin{align*} \sup_{\beta \in A} f(\beta) \leq \alpha. \end{align*} Combining, \begin{align*} f(\gamma) \leq \alpha, \end{align*} so $\gamma \in A$. [guided] We have $\gamma = \sup A \leq \alpha$ but we do not yet know whether $\gamma \in A$ — that is, whether $\gamma$ is actually an admissible input. This is where the **continuity** of normal functions does the work. Apply [Normal Functions Preserve All Suprema](/theorems/1475). Theorem 1475 requires: - $f$ is a normal function — given; - the family whose supremum we are passing through $f$ is non-empty — we are in the case $A \neq \varnothing$. Both conditions hold, so the theorem gives \begin{align*} f(\gamma) = f(\sup A) = \sup_{\beta \in A} f(\beta). \end{align*} Each term on the right-hand side satisfies $f(\beta) \leq \alpha$ by definition of $A$. A supremum of ordinals each bounded by $\alpha$ is itself $\leq \alpha$ — because $\alpha$ is an upper bound, and the supremum is the *least* upper bound. Hence \begin{align*} f(\gamma) \leq \alpha, \end{align*} confirming $\gamma \in A$. Key takeaway: sup-preservation — not merely monotonicity — is essential. Without continuity, $f(\sup A)$ could strictly exceed $\sup_{\beta \in A} f(\beta)$, and we would have no way to conclude $f(\gamma) \leq \alpha$. This is precisely where the "normal" hypothesis (as opposed to "strictly increasing") is consumed. [/guided] [/step] [step:Verify maximality: every $\delta > \gamma$ lies outside $A$] Let $\delta$ be any ordinal with $\delta > \gamma$. Since $\gamma \in A$ and $\gamma = \sup A$, the ordinal $\gamma$ is an upper bound of $A$. Hence if $\delta \in A$, then $\delta \leq \gamma$, contradicting $\delta > \gamma$. Therefore $\delta \notin A$, which means \begin{align*} f(\delta) > \alpha. \end{align*} [guided] We have established $\gamma \in A$ with $\gamma = \sup A$. Whenever a supremum belongs to the set it bounds, it is automatically the maximum of that set. To make this explicit: suppose for contradiction that some $\delta \in A$ satisfies $\delta > \gamma$. Then $\gamma$ fails to be an upper bound of $A$ — we have exhibited an element $\delta \in A$ with $\gamma < \delta$ — contradicting $\gamma = \sup A$. Hence no $\delta > \gamma$ can lie in $A$. Equivalently, every ordinal $\delta > \gamma$ satisfies $f(\delta) > \alpha$. [/guided] [/step] [step:Conclude $\gamma$ is the maximal ordinal with $f(\gamma) \leq \alpha$] Combining the previous two steps: $\gamma \in A$ (so $f(\gamma) \leq \alpha$) and no $\delta > \gamma$ lies in $A$. Hence $\gamma$ is the maximum of $A$, i.e. the maximal ordinal with \begin{align*} f(\gamma) \leq \alpha. \end{align*} This completes the proof. [/step]