[proofplan]
We derive the Well-Ordering Theorem from [Zorn's Lemma](/theorems/1226). The idea is to consider the collection of all well-orderings of subsets of $S$, partially ordered by extension. Zorn's Lemma produces a maximal well-ordering, and we show that a maximal well-ordering must exhaust all of $S$ — for otherwise, we could extend it by appending an unused element.
[/proofplan]
[step:Define the partial order on well-orderings of subsets of $S$]
Let $S$ be a set. Define $\mathcal{W}$ to be the collection of all pairs $(A, \preceq)$ where $A \subset S$ and $\preceq$ is a well-ordering on $A$. We partially order $\mathcal{W}$ by extension: $(A, \preceq_A) \le (B, \preceq_B)$ if and only if
\begin{align*}
&A \subset B, \\
&\preceq_A \text{ agrees with } \preceq_B \text{ on } A \text{ (i.e., for all } a, a' \in A,\ a \preceq_A a' \iff a \preceq_B a'), \\
&\text{every element of } B \setminus A \text{ is a } \preceq_B\text{-upper bound for } A \text{ (i.e., } a \preceq_B b \text{ for all } a \in A, b \in B \setminus A).
\end{align*}
The third condition is essential: it says that $B$ extends $A$ by adding elements *after* all elements of $A$. This ensures that the well-ordering of $A$ is an initial segment of the well-ordering of $B$.
The set $\mathcal{W}$ is nonempty since $(\varnothing, \varnothing) \in \mathcal{W}$.
[guided]
The choice of partial order is the crucial design decision. If we merely required $A \subset B$ and $\preceq_A = \preceq_B|_A$, then chains in $\mathcal{W}$ might not have upper bounds: two well-orderings could agree on their common elements but interleave new elements in incompatible ways. The third condition — that new elements go at the end — prevents this. It ensures that the union of a chain of well-orderings is itself a well-ordering (as we verify in the next step).
Formally, $(A, \preceq_A) \le (B, \preceq_B)$ means $A$ is an initial segment of $(B, \preceq_B)$: every element of $A$ precedes every element of $B \setminus A$.
[/guided]
[/step]
[step:Verify the chain condition: every chain in $\mathcal{W}$ has an upper bound]
Let $\mathcal{C} = \{(A_i, \preceq_i)\}_{i \in I}$ be a chain in $\mathcal{W}$. Define
\begin{align*}
A := \bigcup_{i \in I} A_i,
\end{align*}
and define a relation $\preceq$ on $A$ by: for $a, b \in A$, set $a \preceq b$ if and only if $a \preceq_i b$ for some (equivalently, any) $i \in I$ with $a, b \in A_i$.
This is well-defined: if $a, b \in A_j \cap A_k$ for $j, k \in I$, then since $\mathcal{C}$ is a chain, either $(A_j, \preceq_j) \le (A_k, \preceq_k)$ or vice versa. In either case, $\preceq_j$ and $\preceq_k$ agree on $A_j \cap A_k$.
We verify $(A, \preceq)$ is a well-ordering. It is a total order because any two elements $a, b \in A$ belong to some common $A_i$ (since the $A_i$ form a chain under inclusion), and $\preceq_i$ totally orders $A_i$. For the well-ordering property, let $\varnothing \neq B \subset A$. Choose any $b \in B$, so $b \in A_j$ for some $j$. The set $B \cap A_j$ is nonempty (it contains $b$) and is a subset of the well-ordered set $(A_j, \preceq_j)$, so it has a $\preceq_j$-least element $m$. We claim $m$ is the $\preceq$-least element of $B$. Let $b' \in B$ be arbitrary. If $b' \in A_j$, then $m \preceq_j b'$, so $m \preceq b'$. If $b' \notin A_j$, then since $\mathcal{C}$ is a chain and $b' \in A_k$ for some $k$, either $A_j \subset A_k$ or $A_k \subset A_j$. Since $b' \notin A_j$, we must have $A_j \subsetneq A_k$, so $(A_j, \preceq_j) \le (A_k, \preceq_k)$, meaning every element of $A_j$ precedes every element of $A_k \setminus A_j$ under $\preceq_k$. In particular, $m \in A_j$ and $b' \in A_k \setminus A_j$, so $m \preceq_k b'$, hence $m \preceq b'$.
Therefore $(A, \preceq) \in \mathcal{W}$ and $(A_i, \preceq_i) \le (A, \preceq)$ for all $i \in I$, so $(A, \preceq)$ is an upper bound for $\mathcal{C}$.
[/step]
[step:Apply Zorn's Lemma and show the maximal element well-orders all of $S$]
By [Zorn's Lemma](/theorems/1226), $\mathcal{W}$ has a maximal element $(M, \preceq_M)$. We claim $M = S$.
Suppose for contradiction that $M \neq S$. Choose any $s \in S \setminus M$. Define $M' := M \cup \{s\}$ and extend $\preceq_M$ to $M'$ by declaring $m \preceq_{M'} s$ for all $m \in M$, and $s \preceq_{M'} s$. On $M$, $\preceq_{M'}$ agrees with $\preceq_M$. The element $s$ is placed after all elements of $M$.
The relation $\preceq_{M'}$ is a well-ordering on $M'$: it is a total order (every pair is comparable since $\preceq_M$ is total on $M$ and $s$ is declared larger than everything in $M$). For the well-ordering property, let $\varnothing \neq B \subset M'$. If $B \cap M \neq \varnothing$, the $\preceq_M$-least element of $B \cap M$ is the $\preceq_{M'}$-least element of $B$ (since all elements of $M$ precede $s$). If $B \cap M = \varnothing$, then $B = \{s\}$, and $s$ is its own least element.
Therefore $(M', \preceq_{M'}) \in \mathcal{W}$ and $(M, \preceq_M) < (M', \preceq_{M'})$ (strict, since $M \subsetneq M'$), contradicting maximality of $(M, \preceq_M)$. Hence $M = S$, and $\preceq_M$ is a well-ordering of $S$.
[guided]
The argument is by contradiction. If the maximal well-ordering $(M, \preceq_M)$ does not cover all of $S$, pick any $s \in S \setminus M$ and append it as a new maximum. Formally, define $M' = M \cup \{s\}$ with the order:
\begin{align*}
a \preceq_{M'} b \iff \begin{cases} a \preceq_M b & \text{if } a, b \in M, \\ \text{true} & \text{if } a \in M \text{ and } b = s, \\ a = b = s & \text{if } a = s. \end{cases}
\end{align*}
This places $s$ strictly after every element of $M$. The key verifications are:
1. **Agreement on $M$:** $\preceq_{M'}$ restricted to $M$ is $\preceq_M$.
2. **Initial segment condition:** Every element of $M' \setminus M = \{s\}$ exceeds all elements of $M$.
3. **Well-ordering:** Any nonempty subset of $M'$ not containing $s$ has a least element by $\preceq_M$; if it does contain $s$ and also intersects $M$, the least element in $M$ is still least; if it equals $\{s\}$, then $s$ is least.
Since $(M', \preceq_{M'})$ strictly extends $(M, \preceq_M)$ in $\mathcal{W}$, this contradicts maximality. Therefore $M = S$.
[/guided]
[/step]