[proofplan] We fix an arbitrary starting point $x_0 \in X$ and build a non-decreasing transfinite sequence $(x_\alpha)_\alpha$ in $X$ by iterating $f$ at successor stages and taking suprema at limit stages. Chain-completeness of $X$ makes the suprema well-defined, and the inflationary property of $f$ makes the sequence non-decreasing. By [Hartogs' Theorem](/theorems/1472) there is an ordinal $\gamma$ that does not inject into $X$, so the sequence cannot stay strictly increasing through $\gamma$; the first repetition $x_{\alpha+1} = x_\alpha$ gives $f(x_\alpha) = x_\alpha$. Notably, because the recursion is **deterministic**, no application of the Axiom of Choice is required. [/proofplan] [step:Define the transfinite iteration by recursion] Fix any $x_0 \in X$. We define, by transfinite recursion on the ordinals, a class function \begin{align*} F: \mathrm{Ord} &\to X, & F(0) &= x_0, \\ F(\alpha + 1) &= f(F(\alpha)), \\ F(\lambda) &= \sup\{F(\alpha) : \alpha < \lambda\} \quad \text{for limit ordinals } \lambda > 0. \end{align*} Writing $x_\alpha := F(\alpha)$, the recursion is: \begin{align*} x_0 &= x_0, \\ x_{\alpha + 1} &= f(x_\alpha), \\ x_\lambda &= \sup\{x_\alpha : \alpha < \lambda\} \quad (\lambda \text{ limit, } \lambda > 0). \end{align*} Two facts must be verified for this to be a legitimate definition by transfinite recursion: (a) **The supremum at limit stages exists.** This requires that $\{x_\alpha : \alpha < \lambda\}$ be a chain in $(X, \leq)$, so that chain-completeness of $X$ applies. We verify this in the next step. (b) **The rule is definable.** The recursion rule, as a function of the sequence $(x_\beta)_{\beta < \alpha}$, is given by a definable class function: successor stages apply the set function $f$, and limit stages take the supremum (which, if it exists and is unique, is definable from the poset structure). This makes the recursion a legitimate instance of the [Transfinite Recursion Theorem](/theorems/1464). [guided] We want to iterate $f$ transfinitely starting from some $x_0 \in X$, taking suprema at limit ordinals. Pick any $x_0 \in X$ (since $X$ has a least element $\bot$ in the chain-complete case, one could take $x_0 = \bot$, but any choice works). Define the sequence by transfinite recursion: \begin{align*} x_0 &= x_0, \\ x_{\alpha + 1} &= f(x_\alpha) \qquad \text{(successor stage)}, \\ x_\lambda &= \sup\{x_\alpha : \alpha < \lambda\} \qquad \text{(limit stage, } \lambda > 0\text{)}. \end{align*} Why is this legitimate? The Transfinite Recursion Theorem says: given a definable rule that, for each ordinal $\alpha$, specifies $x_\alpha$ as a function of the sequence $(x_\beta)_{\beta < \alpha}$, there is a unique sequence satisfying the rule. Our rule is definable — apply $f$ at successors, take the sup at limits — but we need the suprema to actually exist. That requires the sets $\{x_\alpha : \alpha < \lambda\}$ to be chains (so chain-completeness applies). A crucial observation: **no choices are being made**. At each stage the value $x_\alpha$ is uniquely determined by the earlier values. This is why the proof goes through in ZF without AC — all the work of Zorn-type arguments (where one might be tempted to pick elements) has been bypassed by the inflationary hypothesis, which determines the next step canonically. [/guided] [/step] [step:Verify by induction that the partial sequences are non-decreasing chains] We prove by transfinite induction on $\alpha$ that (i) $\{x_\beta : \beta \leq \alpha\}$ is a chain in $X$, and (ii) $x_\beta \leq x_\gamma$ whenever $\beta \leq \gamma \leq \alpha$. **Base case ($\alpha = 0$).** The singleton $\{x_0\}$ is a chain, and (ii) is vacuous. **Successor case ($\alpha = \delta + 1$).** Assume (i) and (ii) hold at $\delta$. Since $f$ is inflationary, $x_{\delta+1} = f(x_\delta) \geq x_\delta$. By the inductive hypothesis $x_\beta \leq x_\delta$ for all $\beta \leq \delta$, so $x_\beta \leq x_\delta \leq x_{\delta+1}$ by transitivity of $\leq$. Hence (ii) extends to $\alpha = \delta + 1$. Every pair of elements in $\{x_\beta : \beta \leq \delta + 1\}$ is then comparable (either both in the chain $\{x_\beta : \beta \leq \delta\}$ by (i), or the pair involves $x_{\delta+1}$ and is handled by what we just proved), establishing (i). **Limit case ($\alpha = \lambda$, limit).** Assume (i) and (ii) hold for all $\delta < \lambda$. The set \begin{align*} C_\lambda := \{x_\beta : \beta < \lambda\} \end{align*} is a chain: any two elements $x_\beta, x_{\beta'} \in C_\lambda$ with (say) $\beta \leq \beta'$ lie in $\{x_\gamma : \gamma \leq \beta'\}$, which is a chain by (i) at $\beta' < \lambda$, so $x_\beta, x_{\beta'}$ are comparable. Moreover by (ii) at any $\delta$ with $\beta, \beta' \leq \delta < \lambda$, we have $x_\beta \leq x_{\beta'}$. By chain-completeness of $X$, the supremum $x_\lambda := \sup C_\lambda$ exists in $X$ and satisfies $x_\beta \leq x_\lambda$ for every $\beta < \lambda$. Therefore (ii) holds at $\lambda$: if $\beta \leq \gamma \leq \lambda$, either $\gamma < \lambda$ (use the inductive hypothesis) or $\gamma = \lambda$ (use $x_\beta \leq x_\lambda$). And $\{x_\beta : \beta \leq \lambda\} = C_\lambda \cup \{x_\lambda\}$ is a chain because $x_\lambda$ is comparable to every $x_\beta$ (indeed $x_\lambda \geq x_\beta$ for $\beta < \lambda$), and $C_\lambda$ is a chain. This completes the transfinite induction, showing that the sequence $(x_\alpha)$ is defined for all ordinals and is non-decreasing: $x_\beta \leq x_\gamma$ whenever $\beta \leq \gamma$. [guided] The recursion uses suprema at limit stages, and chain-completeness only guarantees suprema of **chains**. So we must verify — by transfinite induction — that the partial sequences assembled so far are always chains. We simultaneously prove monotonicity $x_\beta \leq x_\gamma$ (for $\beta \leq \gamma$), which is the stronger statement we actually need downstream. **Base case.** The singleton $\{x_0\}$ is a chain. **Successor step.** Assume the segment up to $x_\delta$ is a chain and monotone. Now $x_{\delta+1} = f(x_\delta)$. Why is this $\geq x_\delta$? Because $f$ is inflationary, meaning $f(y) \geq y$ for every $y \in X$. Apply with $y = x_\delta$ to get $x_{\delta+1} \geq x_\delta$. By the inductive monotonicity, every $x_\beta$ with $\beta \leq \delta$ satisfies $x_\beta \leq x_\delta \leq x_{\delta+1}$. So the extended segment is a chain (each new pair is comparable) and monotone (the new element dominates all earlier ones). **Limit step.** Assume monotonicity for all $\delta < \lambda$. The set \begin{align*} C_\lambda = \{x_\beta : \beta < \lambda\} \end{align*} is the union of all the segments built so far. Is it a chain? Pick any two elements $x_\beta, x_{\beta'}$ with $\beta \leq \beta'$. Both lie in the segment up to $x_{\beta'}$, which is a chain by the inductive hypothesis at $\beta' < \lambda$. So $x_\beta$ and $x_{\beta'}$ are comparable (in fact, $x_\beta \leq x_{\beta'}$ by the inductive monotonicity). Hence $C_\lambda$ is a chain. Now chain-completeness of $X$ activates: the supremum $x_\lambda := \sup C_\lambda$ exists in $X$. By the defining property of a supremum, $x_\lambda \geq x_\beta$ for every $\beta < \lambda$, so monotonicity extends. And $\{x_\beta : \beta \leq \lambda\} = C_\lambda \cup \{x_\lambda\}$ is still a chain because $x_\lambda$ is comparable to everything in $C_\lambda$ (it sits above them). We have now established the transfinite sequence $(x_\alpha)$ is defined for **all** ordinals and is non-decreasing. [/guided] [/step] [step:Apply Hartogs' Theorem to bound the ordinal range of injectivity] By [Hartogs' Theorem](/theorems/1472) (provable in ZF without AC), for every set $X$ there is an ordinal $\gamma$ such that $\gamma$ does not inject into $X$ — equivalently, no injection $\gamma \hookrightarrow X$ exists. Call such $\gamma$ the *Hartogs ordinal* of $X$. Consider the map $F\big|_\gamma: \gamma \to X$ obtained by restricting our sequence. Since $\gamma$ does not inject into $X$, the map $F\big|_\gamma$ is not injective. Hence there exist ordinals $\beta < \alpha < \gamma$ with $x_\beta = x_\alpha$. Take the least such $\alpha$. [guided] We have a class-length sequence $(x_\alpha)_\alpha$ sitting inside the *set* $X$. Intuitively, an injection from the class of all ordinals into the set $X$ is impossible, so the sequence must eventually repeat. Hartogs' Theorem makes this rigorous without needing AC: for every set $X$, there is an ordinal $\gamma$ — concretely, the set of all ordinals that inject into $X$ — which itself does **not** inject into $X$. Consider the restriction \begin{align*} F\big|_\gamma: \gamma &\to X, & \alpha \mapsto x_\alpha. \end{align*} If this were an injection, $\gamma$ would inject into $X$, contradicting the defining property of the Hartogs ordinal. So $F\big|_\gamma$ is not injective: there are $\beta < \alpha < \gamma$ with $x_\beta = x_\alpha$. We take the least such $\alpha$. Why must we appeal to Hartogs here, and not simply to "there can't be more elements in a sequence than in $X$"? Because sequences indexed by ordinals are not sequences into a set — they are class-length. The naive "there are only $|X|$ many values" argument requires a cardinality for $X$, which in ZF without AC may not be a well-defined cardinal. Hartogs' Theorem sidesteps this issue entirely: we do not need $|X|$, we just need *some* ordinal that does not inject into $X$. [/guided] [/step] [step:Identify a fixed point from the first repetition] Let $\alpha$ be the least ordinal such that $x_\alpha = x_\beta$ for some $\beta < \alpha$. We claim that $\alpha$ must be a successor ordinal. Suppose for contradiction that $\alpha$ is a limit ordinal. Then $x_\alpha = \sup\{x_\delta : \delta < \alpha\}$, and $x_\alpha = x_\beta$ for some $\beta < \alpha$. By monotonicity (Step 2), $x_\delta \leq x_\alpha = x_\beta$ for all $\delta < \alpha$. But also $x_\beta \leq x_\delta$ for any $\delta \geq \beta$ with $\delta < \alpha$ (monotonicity again). Pick any such $\delta$ with $\beta < \delta < \alpha$ (which exists because $\alpha > \beta$ is a limit, so there are arbitrarily many ordinals strictly between $\beta$ and $\alpha$). Then $x_\beta \leq x_\delta \leq x_\beta$, so $x_\delta = x_\beta$. But then $x_\delta = x_\beta$ with $\beta < \delta < \alpha$ contradicts the minimality of $\alpha$. Hence $\alpha$ is a successor ordinal; write $\alpha = \alpha' + 1$. The repetition says $x_{\alpha' + 1} = x_\beta$ for some $\beta < \alpha' + 1$, i.e.\ $\beta \leq \alpha'$. By monotonicity $x_\beta \leq x_{\alpha'} \leq x_{\alpha' + 1} = x_\beta$, so $x_{\alpha'} = x_\beta = x_{\alpha' + 1}$. Recalling $x_{\alpha' + 1} = f(x_{\alpha'})$: \begin{align*} f(x_{\alpha'}) = x_{\alpha' + 1} = x_{\alpha'}. \end{align*} Hence $x_{\alpha'}$ is a fixed point of $f$. [guided] We know the sequence $(x_\alpha)$ eventually repeats, and $\alpha$ is the smallest ordinal at which a repetition occurs: $x_\alpha = x_\beta$ for some $\beta < \alpha$. We now show that $\alpha$ being a successor ordinal is forced, and this gives us the fixed point. **Could $\alpha$ be a limit ordinal?** Suppose so. Then $x_\alpha = \sup\{x_\delta : \delta < \alpha\}$. Combined with $x_\alpha = x_\beta$ for some $\beta < \alpha$, we deduce that $x_\beta$ is the supremum of the preceding values. But monotonicity says $x_\delta \leq x_{\delta'}$ whenever $\delta \leq \delta'$, so for any $\delta$ with $\beta \leq \delta < \alpha$ we have \begin{align*} x_\beta \leq x_\delta \leq \sup\{x_{\delta''} : \delta'' < \alpha\} = x_\alpha = x_\beta, \end{align*} forcing $x_\delta = x_\beta$. Choose any $\delta$ with $\beta < \delta < \alpha$ (possible because $\alpha$ is a limit and hence contains arbitrarily many ordinals above $\beta$). Then $x_\delta = x_\beta$ with $\beta < \delta < \alpha$. But $\alpha$ was the least ordinal exhibiting a repetition — and here $\delta < \alpha$ exhibits one. Contradiction. So $\alpha$ cannot be a limit. **Therefore $\alpha$ is a successor.** Write $\alpha = \alpha' + 1$. The repetition at $\alpha$ says $x_{\alpha' + 1} = x_\beta$ for some $\beta \leq \alpha'$. Monotonicity sandwiches $x_{\alpha'}$: \begin{align*} x_\beta \leq x_{\alpha'} \leq x_{\alpha' + 1} = x_\beta, \end{align*} so $x_{\alpha'} = x_\beta = x_{\alpha' + 1}$. But the successor rule says $x_{\alpha' + 1} = f(x_{\alpha'})$. Therefore \begin{align*} f(x_{\alpha'}) = x_{\alpha'}, \end{align*} giving the desired fixed point. [/guided] [/step] [step:Conclude the existence of a fixed point] We have exhibited an element $x_{\alpha'} \in X$ with $f(x_{\alpha'}) = x_{\alpha'}$. Hence $f$ has a fixed point, completing the proof. The argument used the Transfinite Recursion Theorem, chain-completeness of $X$, the inflationary property of $f$, and Hartogs' Theorem — all theorems of ZF. No appeal to the Axiom of Choice was made. [/step]