[proofplan] Let $B$ denote the collection of all ordinals that inject into $X$. The proof has three main parts. First, we show $B$ is a set: each $\alpha \in B$ arises as the order type of a well-ordering of some subset of $X$, and well-orderings of subsets of $X$ form a definable subset of $\mathcal{P}(X \times X)$ — hence a set. Replacement then makes $B$ a set. Second, we form the successor of the supremum, $\gamma(X) := (\sup B)^+$, which is an ordinal. Third, we show directly from the sup property that $\gamma(X) \notin B$: any $\beta \in B$ satisfies $\beta \leq \sup B < (\sup B)^+ = \gamma(X)$, so $\gamma(X) \neq \beta$ for every $\beta \in B$, which means no injection $\gamma(X) \hookrightarrow X$ exists. [/proofplan]

[step:Define the candidate set $B$ of ordinals injecting into $X$]Define \begin{align*} B := \{\alpha : \alpha \text{ is an ordinal and there exists an injection } \alpha \hookrightarrow X\}. \end{align*} Here "injection $\alpha \hookrightarrow X$" means an injective function from the underlying set of the ordinal $\alpha$ to $X$. We do not yet know that $B$ is a set. That is the content of the next step.[/step]

[guided]The strategy is to collect every ordinal that *can* inject into $X$, and then produce one that cannot by going strictly past the supremum. For this to work, we need $B$ to be a genuine set — otherwise $\sup B$ makes no sense, and we would be helping ourselves to the very kind of illegitimate totality the [Burali-Forti Paradox](/theorems/1471) forbids. So we face a subtle question right at the start: why should $B$ be a set at all? A priori, $B$ is defined using a quantifier over the class of all ordinals ($\alpha$ ranges over every ordinal), which is not a set. The next step resolves this by finding a *surrogate* set — a set whose elements naturally parametrise $B$ — and then applying the Axiom of Replacement.[/guided]

[step:Show $B$ is a set via the Axiom of Replacement applied to well-orderings of subsets of $X$]Define \begin{align*} A := \{R \subseteq X \times X : R \text{ is a well-ordering of } \operatorname{fld}(R)\}, \end{align*} where $\operatorname{fld}(R) := \{x \in X : \exists y \in X,\, (x,y) \in R \text{ or } (y,x) \in R\}$ is the field of $R$ and is a subset of $X$. $A$ is a set because $A \subseteq \mathcal{P}(X \times X)$ and "$R$ is a well-ordering of its field" is a definable property (irreflexivity, transitivity, trichotomy on the field, and well-foundedness — each expressible with bounded quantifiers over $X \times X$). By the Axioms of Power Set and Separation, $A$ is a set. For each $R \in A$, by [Every Well-Ordered Set Has an Order Type](/theorems/1469), there is a unique ordinal $\operatorname{otp}(R)$ — the order type of $(\operatorname{fld}(R), R)$. Define \begin{align*} F: A &\to \mathrm{Ord} \\ R &\mapsto \operatorname{otp}(R). \end{align*} [claim:$B$ is exactly the image of $F$] *$B \subseteq F(A)$:* Let $\alpha \in B$. There is an injection $f: \alpha \to X$. Define $R \subseteq X \times X$ by \begin{align*} R := \{(f(\beta), f(\gamma)) : \beta, \gamma \in \alpha,\, \beta \in \gamma\}. \end{align*} Since $f$ is injective, the map $f$ is an order isomorphism from $(\alpha, \in)$ onto $(\operatorname{fld}(R), R) = (f(\alpha), R)$. Because $(\alpha, \in)$ is a well-ordering, so is $(f(\alpha), R)$. Hence $R \in A$ and $\operatorname{otp}(R) = \alpha$, giving $\alpha \in F(A)$. *$F(A) \subseteq B$:* Let $\alpha = F(R) = \operatorname{otp}(R)$ for some $R \in A$. By the order type theorem, there is an order isomorphism $g: (\operatorname{fld}(R), R) \to (\alpha, \in)$. Its inverse $g^{-1}: \alpha \to \operatorname{fld}(R) \subseteq X$ is, in particular, an injection $\alpha \to X$. Hence $\alpha \in B$. [proof] The inclusion $B \subseteq F(A)$: given $\alpha \in B$ and an injection $f: \alpha \to X$, the pushforward order $R := \{(f(\beta), f(\gamma)) : \beta \in \gamma \text{ in } \alpha\}$ is a well-ordering of $f(\alpha) \subseteq X$ with order type $\alpha$. The reverse inclusion $F(A) \subseteq B$: given $R \in A$ with order type $\alpha$, the order isomorphism $g: \operatorname{fld}(R) \to \alpha$ has inverse $g^{-1}: \alpha \to X$, which is an injection. [/proof] [/claim] By the Axiom of Replacement applied to the definable function $F$ with domain the set $A$, the image $F(A)$ is a set. Since $B = F(A)$ by the claim, $B$ is a set.[/step]

[guided]The technical heart of Hartogs' lemma is showing $B$ is a set. The idea is: *Any ordinal in $B$ injects into $X$ — and via that injection, it pulls back a well-ordering from $\alpha$ onto a subset of $X$.* Hence every element of $B$ is "witnessed" by a well-ordering of some subset of $X$. Well-orderings of subsets of $X$ form a genuinely small collection: they sit inside $\mathcal{P}(X \times X)$, which is a set by the Power Set axiom. That gives us our bounded domain $A$. We now set up the function $F: A \to \mathrm{Ord}$ sending each well-ordering to its order type. This function is definable — its defining property is "$\alpha$ is the unique ordinal order-isomorphic to $(\operatorname{fld}(R), R)$", which is expressible in the language of set theory. That is all the Axiom of Replacement needs: given a definable functional relation $F$ and a set $A$ in its domain, the image $F(A)$ is a set. The [claim] verifies that $F(A)$ is exactly $B$: - Every $\alpha \in B$ gives rise to some $R \in A$ with $\operatorname{otp}(R) = \alpha$. Take the injection $f: \alpha \to X$ witnessing $\alpha \in B$ and push the order of $\alpha$ forward onto $f(\alpha) \subseteq X$. The resulting relation $R$ is a well-ordering of $f(\alpha)$ with the same order type $\alpha$. - Conversely, every $R \in A$ has an order type $\alpha$ that lies in $B$: invert the canonical order isomorphism $\operatorname{fld}(R) \to \alpha$ to get an injection $\alpha \to X$. Combining: $B = F(A)$, and by Replacement, $F(A)$ is a set. Crucially, we avoided ever quantifying over all ordinals directly: the domain $A$ is a set, and Replacement only requires the functional relation to be definable.[/guided]

[step:Define $\gamma(X) := (\sup B)^+$ and note it is an ordinal]Since $B$ is a set of ordinals, by [Supremum of a Set of Ordinals](/theorems/1470), the supremum \begin{align*} s := \sup B = \bigcup_{\alpha \in B} \alpha \end{align*} is itself an ordinal, with $\alpha \leq s$ for every $\alpha \in B$. Define \begin{align*} \gamma(X) := s^+ = s \cup \{s\}, \end{align*} the successor ordinal of $s$. By construction, $\gamma(X)$ is an ordinal, and $s < \gamma(X)$.[/step]

[guided]A fundamental fact about ordinals: any set of ordinals has a supremum, which is itself an ordinal. Concretely, the supremum is computed as the union $\bigcup B$; this is a set by the Axiom of Union, and one checks it is transitive and well-ordered by $\in$, hence an ordinal. We verify the hypothesis of the supremum theorem: $B$ must be a **set**. This is exactly what the previous step established — without Step 2, we could not take the sup here. We then pass to the *successor* $\gamma(X) := s^+ = s \cup \{s\}$. The successor operation is always defined on ordinals, producing a strictly larger ordinal: $s \in s^+$, so $s < s^+ = \gamma(X)$ in the ordinal order. Why the successor rather than the supremum itself? Because we need an ordinal *strictly larger* than everything in $B$. The supremum $s$ might or might not be a member of $B$ (depending on whether $B$ has a maximum), but $\gamma(X) = s^+$ is guaranteed to exceed every element of $B$ strictly. That strict separation is exactly what will prevent $\gamma(X)$ from injecting into $X$ in the next step.[/guided]

[step:Prove $\gamma(X)$ does not inject into $X$]We show $\gamma(X) \notin B$ directly from the sup property. Suppose for contradiction that $\gamma(X) \in B$. Then $\gamma(X)$ is one of the ordinals whose supremum defines $s$, so by the definition of supremum, \begin{align*} \gamma(X) \leq s. \end{align*} On the other hand, $\gamma(X) = s^+$ and by the definition of the successor ordinal, $s \in s^+ = \gamma(X)$, i.e. \begin{align*} s < \gamma(X). \end{align*} Combining, \begin{align*} \gamma(X) \leq s < \gamma(X), \end{align*} which contradicts the irreflexivity of the ordinal order. Hence $\gamma(X) \notin B$. By the definition of $B$, this means there is no injection $\gamma(X) \hookrightarrow X$. $\blacksquare$[/step]

[guided]We have set things up so that the non-injection property falls out of pure ordinal arithmetic — no case analysis on surjectivity, no auxiliary constructions. The logic is: 1. Suppose $\gamma(X) \in B$, i.e., suppose $\gamma(X)$ does inject into $X$. 2. By the sup property, every element of $B$ is $\leq s$. In particular $\gamma(X) \leq s$. 3. But $\gamma(X) = s^+$ was defined as the successor of $s$, so $s \in \gamma(X)$, which in the ordinal order means $s < \gamma(X)$. 4. We have derived $\gamma(X) \leq s$ and $s < \gamma(X)$ simultaneously, i.e., $\gamma(X) < \gamma(X)$, which is impossible: ordinals are well-ordered by $\in$, and $<$ is irreflexive. The power of defining $\gamma(X)$ as $(\sup B)^+$ rather than as $\sup B$ itself is that it sidesteps the question of whether $\sup B$ is or is not a member of $B$. This question depends on $X$ (if $X$ is finite with $n$ elements, $\sup B = n$ and $n \notin B$; if $X$ is countably infinite, $\sup B = \omega$ and whether $\omega \in B$ depends on $X$), but we do not need to resolve it. The successor ordinal $s^+$ is strictly larger than $s$, hence strictly larger than every element of $B$, regardless of whether $B$ attains its supremum. This contradiction proof uses exactly one property of the ordinal order: irreflexivity. Every other fact has been encapsulated: that the supremum exists and dominates $B$ (from the previous step), that the successor is strictly larger (from the definition of $s^+$). Thus $\gamma(X) \notin B$, and by the definition of $B$, no injection $\gamma(X) \hookrightarrow X$ exists — exactly the conclusion of Hartogs' lemma. The ordinal $\gamma(X)$ (the **Hartogs number** of $X$) is an ordinal that cannot be embedded into $X$, as desired.[/guided]