[proofplan] We construct an order-isomorphism $f: Y \to X$ by [transfinite recursion](/theorems/1464) with recursion rule $f(x) = \min(X \setminus \{f(y) : y \in Y, y < x\})$. The proof then has four parts: (i) show the minimum always exists, which reduces to the domination estimate $f(z) \leq z$ (established by transfinite induction); (ii) show $f$ is strictly increasing; (iii) show the image is an initial segment of $X$; (iv) derive uniqueness from the fact that any two order-isomorphisms into initial segments must coincide. The key technical content is the induction $f(z) \leq z$, which both makes the recursion well-defined and delivers the initial-segment structure of the image. [/proofplan]

[step:Define the recursion rule and justify applicability of transfinite recursion]Let $(X, <)$ be a well-ordered set and let $Y \subseteq X$ be non-empty. For $x \in Y$, write $I^Y_x := \{y \in Y : y < x\}$ (the initial segment of $Y$ below $x$, using the order on $X$ restricted to $Y$). Note that $Y$ inherits a well-order from $X$: every non-empty subset $A \subseteq Y$ is also a non-empty subset of $X$, so $A$ has a least element in $X$, which is necessarily the least element of $A$ in $Y$. Define \begin{align*} G: \mathcal{P}(Y \times X) &\to X \end{align*} by the rule: for any function $h: I^Y_x \to X$ regarded as a subset of $Y \times X$, \begin{align*} G(h) := \min\bigl(X \setminus \{h(y) : y \in \operatorname{dom}(h)\}\bigr), \end{align*} and set $G(h) := \min X$ if $\operatorname{dom}(h) = \varnothing$ (this case handles the base element $\min Y$). For arguments that do not represent functions, the value of $G$ is irrelevant and may be set arbitrarily, say to $\min X$. By [Definition by Transfinite Recursion](/theorems/1464) applied to the well-ordered set $(Y, <)$ and the set $X$ (with rule $G$), there exists a unique function \begin{align*} f: Y \to X \end{align*} such that $f(x) = G(f|_{I^Y_x})$ for every $x \in Y$. In particular, \begin{align*} f(x) = \min\bigl(X \setminus \{f(y) : y \in Y, y < x\}\bigr) \end{align*} whenever the right-hand side is well-defined, which we verify next.[/step]

[guided]The definition of $f$ uses the [Definition by Transfinite Recursion](/theorems/1464) on the well-ordered set $(Y, <_Y)$, where $<_Y$ is the restriction of $<$ to $Y$. *Is $(Y, <_Y)$ a well-ordering?* We check the defining property. Let $A \subseteq Y$ be non-empty. Since $A \subseteq Y \subseteq X$ and $A$ is non-empty, the well-ordering of $X$ provides $a_0 := \min_X A$. Because $a_0 \in A \subseteq Y$, this element is also a least element of $A$ in $Y$. So $(Y, <_Y)$ is indeed well-ordered, and transfinite recursion applies. *What is the recursion rule?* At each $x \in Y$, we want $f(x)$ to be the smallest element of $X$ that has not yet been used as a value $f(y)$ for some earlier $y$. Formally, \begin{align*} f(x) := \min\bigl(X \setminus \{f(y) : y \in Y,\, y < x\}\bigr), \end{align*} which depends on $f|_{I^Y_x}$ (the list of previously assigned values). This is exactly the form $f(x) = G(f|_{I^Y_x})$ required by transfinite recursion, with \begin{align*} G(h) := \min\bigl(X \setminus \operatorname{range}(h)\bigr). \end{align*} [Theorem 1464](/theorems/1464) produces a unique $f: Y \to X$ satisfying this equation, provided the minimum on the right-hand side always exists. The latter is the content of the next step.[/guided]

[step:Prove $f(z) \leq z$ for all $z \in Y$ by transfinite induction, which simultaneously shows the minimum exists][claim:Domination estimate] For every $z \in Y$, the set $X \setminus \{f(y) : y \in Y, y < z\}$ is non-empty, the minimum defining $f(z)$ exists, and $f(z) \leq z$. [/claim] [proof] We prove by [Transfinite Induction](/theorems/1463) on $(Y, <_Y)$ the statement \begin{align*} S := \{z \in Y : f(z) \text{ is well-defined and } f(z) \leq z\}. \end{align*} We show: for every $z \in Y$, if $y \in S$ for every $y \in Y$ with $y < z$, then $z \in S$. Fix $z \in Y$ and suppose $f(y) \leq y$ for every $y \in Y$ with $y < z$. In particular, $f(y) < z$ for every such $y$ (since $f(y) \leq y < z$), so \begin{align*} \{f(y) : y \in Y,\, y < z\} \subseteq \{w \in X : w < z\} = I_z. \end{align*} Consequently $z \notin \{f(y) : y \in Y, y < z\}$ (since $z \notin I_z$, as $<$ is irreflexive), so $z \in X \setminus \{f(y) : y \in Y, y < z\}$. The set $X \setminus \{f(y) : y \in Y, y < z\}$ is therefore non-empty (it contains $z$). Being a non-empty subset of the well-ordered set $X$, it has a minimum, so \begin{align*} f(z) = \min\bigl(X \setminus \{f(y) : y \in Y, y < z\}\bigr) \end{align*} is well-defined. Since $z$ lies in this set, $f(z) \leq z$. Hence $z \in S$, completing the inductive step. By [Transfinite Induction](/theorems/1463), $S = Y$, proving the claim. [/proof][/step]

[guided]The domination estimate $f(z) \leq z$ does two things simultaneously: it ensures the recursion is well-defined (the minimum in the recursion rule always exists), and it provides the key inequality for showing the image of $f$ is an initial segment of $X$. Apply [Transfinite Induction](/theorems/1463) to $(Y, <_Y)$ with \begin{align*} S := \{z \in Y : f(z) \text{ exists and } f(z) \leq z\}. \end{align*} The induction hypothesis for $z \in Y$ reads: $f(y) \leq y$ for every $y \in Y$ with $y < z$. *Key observation.* If $f(y) \leq y < z$, then every value $f(y)$ assigned before step $z$ is strictly below $z$. Thus the set of "previously used" values is contained in $I_z = \{w \in X : w < z\}$: \begin{align*} \{f(y) : y \in Y, y < z\} \subseteq I_z. \end{align*} *Consequence 1 — $z$ itself is unused.* The strict order is irreflexive, so $z \notin I_z$. Combined with the containment above, $z$ does *not* belong to the set of previously used values. Hence $z$ lies in its complement: \begin{align*} z \in X \setminus \{f(y) : y \in Y, y < z\}. \end{align*} *Consequence 2 — the minimum exists.* The set $X \setminus \{f(y) : y \in Y, y < z\}$ is a non-empty subset of the well-ordered set $X$ (it contains $z$), so by the definition of well-ordering it has a least element. Thus \begin{align*} f(z) := \min\bigl(X \setminus \{f(y) : y \in Y, y < z\}\bigr) \end{align*} is well-defined. Without the induction hypothesis, we would have no a priori guarantee that the set is non-empty — the recursion could fail at some point. *Consequence 3 — the bound $f(z) \leq z$.* Since $z$ lies in the set whose minimum is $f(z)$, we have $f(z) \leq z$. The induction step is complete, and [Theorem 1463](/theorems/1463) concludes $S = Y$.[/guided]

[step:Show that $f$ is strictly order-preserving]Let $y, z \in Y$ with $y < z$. By definition, \begin{align*} f(z) = \min\bigl(X \setminus \{f(w) : w \in Y, w < z\}\bigr). \end{align*} Since $y \in Y$ with $y < z$, the value $f(y)$ lies in $\{f(w) : w \in Y, w < z\}$, so $f(y) \notin X \setminus \{f(w) : w \in Y, w < z\}$. In particular $f(z) \neq f(y)$, and since $f(z)$ is in the complement set, \begin{align*} f(z) \in X \setminus \{f(w) : w \in Y, w < z\} \subseteq X \setminus \{f(y)\}. \end{align*} We now show $f(y) < f(z)$. Suppose toward contradiction that $f(z) < f(y)$. Then $f(z) \in I_{f(y)}$. The minimum defining $f(y)$ excludes all values $f(w)$ with $w < y$: \begin{align*} f(y) = \min\bigl(X \setminus \{f(w) : w \in Y, w < y\}\bigr). \end{align*} If $f(z) < f(y)$, then $f(z)$ must have been excluded from the set whose minimum is $f(y)$, i.e. $f(z) \in \{f(w) : w \in Y, w < y\}$. Thus there exists $w \in Y$ with $w < y$ and $f(z) = f(w)$. By the same argument applied to $f(w)$ versus $f(z)$ — since $w < y < z$, the value $f(z)$ is chosen as the minimum of a set that *excludes* $f(w)$ (because $w < z$), so $f(z) \neq f(w)$. This contradicts $f(z) = f(w)$. Hence $f(z) \not< f(y)$, and combined with $f(z) \neq f(y)$ we conclude $f(y) < f(z)$ by trichotomy. In particular, $f$ is injective.[/step]

[guided]We must show: $y < z$ in $Y$ implies $f(y) < f(z)$ in $X$. Fix $y < z$ in $Y$. The recursion rule at $z$ reads \begin{align*} f(z) = \min\bigl(X \setminus \{f(w) : w \in Y, w < z\}\bigr). \end{align*} Because $y \in Y$ and $y < z$, the value $f(y)$ appears among the $\{f(w) : w \in Y, w < z\}$. Hence $f(y)$ is *excluded* from the set whose minimum is $f(z)$. In particular, \begin{align*} f(z) \neq f(y). \end{align*} So $f$ is injective at this pair, and it remains to determine the direction of the inequality. *Suppose for contradiction $f(z) < f(y)$.* We ask: why was $f(z)$ not chosen as the value of $f$ at an earlier stage? Looking at the recursion rule for $f(y)$: \begin{align*} f(y) = \min\bigl(X \setminus \{f(w) : w \in Y, w < y\}\bigr), \end{align*} the value $f(y)$ is the smallest element of $X$ not previously used before step $y$. If $f(z) < f(y)$, then $f(z)$ was previously used, i.e., $f(z) = f(w)$ for some $w \in Y$ with $w < y$. *But this contradicts the exclusion at step $z$.* Since $w < y < z$, we have $w < z$, so the recursion at $z$ *excludes* the value $f(w)$. Formally, $f(w) \in \{f(u) : u \in Y, u < z\}$, so $f(z) \neq f(w)$. This contradicts $f(z) = f(w)$. So the supposition $f(z) < f(y)$ fails. Combined with $f(z) \neq f(y)$, trichotomy of the linear order $<$ on $X$ forces $f(y) < f(z)$. Since $y < z$ implies $f(y) < f(z)$, the map $f$ is strictly increasing, hence injective (if $y \neq z$, say $y < z$, then $f(y) < f(z) \neq f(y)$).[/guided]

[step:Show that the image $f(Y)$ is an initial segment of $X$]Let $J := f(Y) = \{f(z) : z \in Y\}$. We show $J$ is an initial segment of $X$: if $a \in X$ and $a < b$ for some $b \in J$, then $a \in J$. Fix $b \in J$, so $b = f(z)$ for some $z \in Y$. Let $a \in X$ with $a < b = f(z)$. By the recursion rule, \begin{align*} f(z) = \min\bigl(X \setminus \{f(y) : y \in Y, y < z\}\bigr), \end{align*} so $f(z)$ is the minimum of this complement. Since $a < f(z)$, $a$ cannot lie in the complement (else it would be a smaller element, contradicting $f(z)$ being the minimum). Therefore $a \in \{f(y) : y \in Y, y < z\}$, so there exists $y \in Y$ with $y < z$ and $a = f(y)$. In particular $a \in J$. Hence $J$ is downward-closed in $X$, i.e. an initial segment of $X$.[/step]

[guided]We show: if $a < b$ and $b \in f(Y)$, then $a \in f(Y)$. Fix $b = f(z)$ for some $z \in Y$. Given $a \in X$ with $a < b = f(z)$, we need to produce $y \in Y$ with $f(y) = a$. *The recursion rule at $z$ gives*: \begin{align*} f(z) = \min\bigl(X \setminus \{f(y) : y \in Y, y < z\}\bigr). \end{align*} So $f(z)$ is the *smallest* element of $X$ that has not been used by $f$ at an earlier step. If $a < f(z)$, then $a$ is *not* an element of the set whose minimum is $f(z)$ (else $a$ would be a smaller element of that set, contradicting $f(z) = \min$). Concretely, $a$ being excluded from $X \setminus \{f(y) : y \in Y, y < z\}$ means: \begin{align*} a \in \{f(y) : y \in Y, y < z\}, \end{align*} so $a = f(y)$ for some $y \in Y$ with $y < z$. Hence $a \in f(Y) = J$, and $J$ is downward-closed. The image is therefore an initial segment of $X$.[/guided]

[step:Conclude the order-isomorphism and uniqueness]By Steps 3 and 4, $f: Y \to J$ is strictly increasing, injective, and surjective onto the initial segment $J = f(Y) \subseteq X$. A strictly increasing bijection between linearly ordered sets is an order-isomorphism. Hence $f$ is an order-isomorphism of $Y$ onto the initial segment $J$ of $X$. For uniqueness: suppose $g: Y \to X$ is another order-isomorphism of $Y$ onto an initial segment $J'$ of $X$. We show $g = f$ by [Transfinite Induction](/theorems/1463) on $(Y, <_Y)$. Let $T := \{z \in Y : g(z) = f(z)\}$. Fix $z \in Y$ and assume $g(y) = f(y)$ for every $y \in Y$ with $y < z$. We show $g(z) = f(z)$. Since $g$ is order-preserving, $g(y) < g(z)$ for every $y < z$ in $Y$. Thus \begin{align*} \{g(y) : y \in Y, y < z\} \subseteq I_{g(z)}. \end{align*} We claim equality holds. Let $a \in I_{g(z)}$, so $a \in X$ and $a < g(z)$. Since $g(z) \in J'$ and $J'$ is an initial segment of $X$, $a \in J'$; hence $a = g(y_0)$ for some $y_0 \in Y$. Since $g$ is strictly order-preserving, $g(y_0) < g(z)$ implies $y_0 < z$. Therefore $a = g(y_0) \in \{g(y) : y \in Y, y < z\}$, giving the reverse inclusion. We conclude $\{g(y) : y \in Y, y < z\} = I_{g(z)}$, hence \begin{align*} g(z) = \min\bigl(X \setminus I_{g(z)}\bigr) = \min\bigl(X \setminus \{g(y) : y \in Y, y < z\}\bigr). \end{align*} By the induction hypothesis $g(y) = f(y)$ for $y < z$, so $\{g(y) : y \in Y, y < z\} = \{f(y) : y \in Y, y < z\}$. Therefore \begin{align*} g(z) = \min\bigl(X \setminus \{f(y) : y \in Y, y < z\}\bigr) = f(z). \end{align*} Hence $z \in T$, and by [Transfinite Induction](/theorems/1463), $T = Y$, so $g = f$. In particular $J' = g(Y) = f(Y) = J$, so the initial segment is also unique. This completes the proof that $Y$ is order-isomorphic to a unique initial segment of $X$ via a unique isomorphism.[/step]

[guided]*Why is $f$ an order-isomorphism onto $J$?* A map between linearly ordered sets is an order-isomorphism iff it is a strictly increasing bijection. We have: 1. $f: Y \to J$ is well-defined (by construction, $f(z) \in X$ for all $z \in Y$, and $J$ is defined as the image). 2. $f$ is strictly increasing (Step 3). 3. $f$ is injective (follows from strict monotonicity). 4. $f$ is surjective onto $J = f(Y)$ by definition of image. 5. $J$ is an initial segment of $X$ (Step 4). Hence $f$ is an order-isomorphism $Y \cong J$. *Uniqueness.* Let $g: Y \to X$ be any order-isomorphism onto an initial segment $J'$. We prove $g = f$ by [Transfinite Induction](/theorems/1463) on $Y$. Assume $g(y) = f(y)$ for every $y \in Y$ with $y < z$. We show $g(z) = f(z)$. **Computing the "image below $g(z)$".** Since $g$ is order-preserving, $y < z$ implies $g(y) < g(z)$, so $\{g(y) : y \in Y, y < z\} \subseteq I_{g(z)}$. For the reverse: let $a \in I_{g(z)}$, i.e. $a < g(z)$. Because $g(z) \in J'$ and $J'$ is an initial segment, $a \in J'$; by surjectivity of $g$ onto $J'$, $a = g(y_0)$ for some $y_0 \in Y$. Strict monotonicity of $g$ plus $g(y_0) = a < g(z)$ forces $y_0 < z$. So $a \in \{g(y) : y \in Y, y < z\}$. Hence \begin{align*} \{g(y) : y \in Y, y < z\} = I_{g(z)}. \end{align*} **Extracting $g(z)$ via minimisation.** From the identity above, $g(z)$ is the least element of $X$ not in $\{g(y) : y \in Y, y < z\}$: \begin{align*} g(z) = \min(X \setminus I_{g(z)}) = \min\bigl(X \setminus \{g(y) : y \in Y, y < z\}\bigr). \end{align*} By the induction hypothesis $g(y) = f(y)$ for $y < z$, so $\{g(y) : y < z\} = \{f(y) : y < z\}$, giving \begin{align*} g(z) = \min\bigl(X \setminus \{f(y) : y \in Y, y < z\}\bigr) = f(z) \end{align*} by the defining recursion for $f$. The induction step is complete, [Theorem 1463](/theorems/1463) gives $g = f$ on all of $Y$, and in particular $J' = g(Y) = f(Y) = J$. Thus $Y$ is order-isomorphic to a unique initial segment of $X$, via a unique isomorphism. This completes the proof.[/guided]