[proofplan] We prove the equivalence by establishing a cycle of implications. The implication (AC) $\Rightarrow$ (Zorn) is taken as already established in the proof of [Zorn's Lemma](/theorems/1226). We prove the remaining three implications: (Zorn) $\Rightarrow$ (AC) by applying Zorn to the poset of partial choice functions ordered by extension; (AC) $\Rightarrow$ (Well-Ordering) by a transfinite recursion that at each stage uses a choice function to extract a "next" element outside the already-enumerated portion; and (Well-Ordering) $\Rightarrow$ (AC) by the trivial observation that a well-ordering on the union of a family gives a canonical choice of least element from each set. [/proofplan]

[step:Recall the implication (AC) $\Rightarrow$ (Zorn)] The implication (1) $\Rightarrow$ (2) has been established in the proof of [Zorn's Lemma](/theorems/1226) from the Axiom of Choice. We do not repeat it here. The remaining three implications, (2) $\Rightarrow$ (1), (1) $\Rightarrow$ (3), and (3) $\Rightarrow$ (1), will close the equivalence cycle. [/step]

[step:Derive AC from Zorn via the poset of partial choice functions]Assume Zorn's Lemma. Let $\{A_i : i \in I\}$ be a family of non-empty sets, indexed by a set $I$. We seek a function \begin{align*} f: I &\to \bigcup_{i \in I} A_i \end{align*} such that $f(i) \in A_i$ for every $i \in I$. Define the set $X$ of **partial choice functions**: \begin{align*} X := \left\{ (J, f) \;:\; J \subseteq I,\ f: J \to \bigcup_{i \in I} A_i,\ f(j) \in A_j \text{ for all } j \in J \right\}. \end{align*} Note $X$ is non-empty: pick any $i_0 \in I$ (which exists if $I \neq \varnothing$; if $I = \varnothing$ the empty function is vacuously a choice function and we are done) and any $a_0 \in A_{i_0}$, and then $(\{i_0\}, i_0 \mapsto a_0) \in X$. Order $X$ by extension: \begin{align*} (J, f) \leq (J', f') \iff J \subseteq J' \text{ and } f'\big|_J = f. \end{align*} This is a partial order: reflexivity and antisymmetry are immediate; transitivity follows because $J \subseteq J' \subseteq J''$ and the compatibility conditions chain. We verify that every chain in $X$ has an upper bound. Let $\mathcal{C} = \{(J_k, f_k) : k \in K\}$ be a chain in $X$. Define \begin{align*} J^* := \bigcup_{k \in K} J_k, \qquad f^*: J^* \to \bigcup_{i \in I} A_i, \end{align*} where $f^*(j) := f_k(j)$ for any $k \in K$ with $j \in J_k$. This is well-defined: if $j \in J_k \cap J_{k'}$, then since $\mathcal{C}$ is a chain either $(J_k, f_k) \leq (J_{k'}, f_{k'})$ or vice versa, and in either case the larger element extends the smaller, so $f_k(j) = f_{k'}(j)$. Moreover $f^*(j) \in A_j$ because $f^*(j) = f_k(j) \in A_j$ for the chosen $k$. Hence $(J^*, f^*) \in X$ and it is an upper bound for $\mathcal{C}$ by construction. By Zorn's Lemma, $X$ contains a maximal element $(J, f)$. We claim $J = I$. Suppose for contradiction that $J \subsetneq I$. Choose $i_0 \in I \setminus J$; this is possible because $I \setminus J \neq \varnothing$. Since $A_{i_0}$ is non-empty, choose $a_0 \in A_{i_0}$. Define \begin{align*} J' := J \cup \{i_0\}, \qquad f': J' \to \bigcup_{i \in I} A_i, \qquad f'(j) := \begin{cases} f(j) & \text{if } j \in J, \\ a_0 & \text{if } j = i_0. \end{cases} \end{align*} Then $(J', f') \in X$ and $(J, f) < (J', f')$, contradicting maximality. Hence $J = I$ and $f$ is the required choice function.[/step]

[guided]Assume Zorn's Lemma. Let $\{A_i : i \in I\}$ be a family of non-empty sets indexed by a set $I$. Our task is to produce a function $f: I \to \bigcup_i A_i$ with $f(i) \in A_i$ for every $i$. The strategy is to construct $f$ one coordinate at a time, using Zorn's Lemma to guarantee we can extend indefinitely. The natural object to put into Zorn's Lemma is not a choice function itself but a **partial** choice function — a function defined only on a subset of $I$ — because partial choice functions can be non-trivially compared and extended. Define \begin{align*} X := \left\{ (J, f) \;:\; J \subseteq I,\ f: J \to \bigcup_{i \in I} A_i,\ f(j) \in A_j \text{ for all } j \in J \right\}, \end{align*} the set of all partial choice functions. We want Zorn's Lemma to hand us a maximal partial choice function; then we argue that a maximal partial choice function must actually be total. Is $X$ non-empty? If $I = \varnothing$, the empty function $\varnothing \to \varnothing$ is vacuously a choice function and we are done. Otherwise pick any $i_0 \in I$ and any $a_0 \in A_{i_0}$ (which exists because $A_{i_0}$ is non-empty). Then $(\{i_0\}, i_0 \mapsto a_0) \in X$. We order $X$ by extension: \begin{align*} (J, f) \leq (J', f') \iff J \subseteq J' \text{ and } f'\big|_J = f. \end{align*} A larger partial choice function has a larger domain and agrees with the smaller one where they overlap. This is a partial order: reflexivity and antisymmetry are direct, and transitivity chains through nested domains. Zorn's Lemma requires that every chain in $X$ have an upper bound. Let $\mathcal{C} = \{(J_k, f_k) : k \in K\}$ be a chain in $X$. The obvious candidate upper bound is the "union" of $\mathcal{C}$: \begin{align*} J^* := \bigcup_{k \in K} J_k, \qquad f^*: J^* \to \bigcup_{i \in I} A_i, \qquad f^*(j) := f_k(j) \text{ for any } k \text{ with } j \in J_k. \end{align*} Is $f^*$ well-defined? The concern is that if $j \in J_k \cap J_{k'}$ for two different $k$, the values $f_k(j)$ and $f_{k'}(j)$ might disagree. This is where the chain property saves us: either $(J_k, f_k) \leq (J_{k'}, f_{k'})$ or $(J_{k'}, f_{k'}) \leq (J_k, f_k)$, and in either case the larger function restricts to the smaller one on the shared domain, so $f_k(j) = f_{k'}(j)$. And $f^*(j) \in A_j$ by inheritance from $f_k$. So $(J^*, f^*) \in X$, and it dominates every element of $\mathcal{C}$. Zorn's Lemma now produces a maximal element $(J, f) \in X$. The final claim is that $J = I$. Suppose not — suppose $J \subsetneq I$. Then there is some $i_0 \in I \setminus J$. Because $A_{i_0}$ is non-empty, we can pick $a_0 \in A_{i_0}$. Now define a strictly larger partial choice function: \begin{align*} J' := J \cup \{i_0\}, \qquad f'(j) := \begin{cases} f(j) & \text{if } j \in J, \\ a_0 & \text{if } j = i_0. \end{cases} \end{align*} Then $(J', f') \in X$ strictly extends $(J, f)$, contradicting maximality. Therefore $J = I$ and $f: I \to \bigcup_i A_i$ is a choice function. Notice that the only place we "chose" anything in this proof was the final step, where we picked $a_0 \in A_{i_0}$. This is *one* choice from *one* non-empty set — which ZF allows without AC. All the heavy lifting of making infinitely many choices simultaneously has been delegated to Zorn's Lemma.[/guided]

[step:Derive the Well-Ordering Principle from AC by transfinite recursion]Assume the Axiom of Choice. Let $X$ be any set; we construct a well-ordering of $X$. Let $\mathcal{P}(X)$ denote the power set of $X$, and let $\mathcal{P}^*(X) := \{A \in \mathcal{P}(X) : A \subsetneq X\}$ be the collection of proper subsets. For each $A \in \mathcal{P}^*(X)$, the complement $X \setminus A$ is non-empty. By the Axiom of Choice applied to the family $\{X \setminus A : A \in \mathcal{P}^*(X)\}$, there exists a function \begin{align*} \gamma: \mathcal{P}^*(X) &\to X, & \gamma(A) \in X \setminus A \text{ for all } A \in \mathcal{P}^*(X). \end{align*} We now define a sequence $(x_\alpha)$ indexed by ordinals $\alpha$ by transfinite recursion. Fix any set $\star \notin X$ (e.g., $\star = X$ itself, which is not a member of itself by the Axiom of Foundation, but one can also use $\{X\}$). Define \begin{align*} F: \mathrm{Ord} \to X \cup \{\star\}, \qquad F(\alpha) := \begin{cases} \gamma(\{F(\beta) : \beta < \alpha\}) & \text{if } \{F(\beta) : \beta < \alpha\} \subsetneq X, \\ \star & \text{otherwise}. \end{cases} \end{align*} The recursion is justified by the Transfinite Recursion Theorem: the value at stage $\alpha$ depends only on the function $F\big|_\alpha$, and the rule defining $F(\alpha)$ from $F\big|_\alpha$ is given by a definable class function. Write $X_\alpha := \{F(\beta) : \beta < \alpha, F(\beta) \neq \star\}$. By induction on $\alpha$, so long as $F(\alpha) \neq \star$, the values $F(\beta)$ for $\beta < \alpha$ are pairwise distinct: indeed if $F(\alpha) = \gamma(X_\alpha) \in X \setminus X_\alpha$, then $F(\alpha) \neq F(\beta)$ for any $\beta < \alpha$. We claim there exists an ordinal $\alpha$ with $F(\alpha) = \star$. Suppose for contradiction that $F(\alpha) \in X$ for every ordinal $\alpha$. Then the map $\alpha \mapsto F(\alpha)$ is injective from the class $\mathrm{Ord}$ of all ordinals into $X$. By [Hartogs' Theorem](/theorems/1472), there exists an ordinal $\kappa$ that does not inject into $X$. But our injection restricted to $\kappa$ is an injection $\kappa \hookrightarrow X$, a contradiction. Let $\alpha_0$ be the least ordinal with $F(\alpha_0) = \star$. Then for every $\beta < \alpha_0$ we have $F(\beta) \in X$, and by definition of the recursion $X_{\alpha_0} = X$ (otherwise $F(\alpha_0)$ would have been $\gamma(X_{\alpha_0}) \in X$, not $\star$). The map \begin{align*} F\big|_{\alpha_0}: \alpha_0 &\to X \end{align*} is therefore a bijection (surjectivity: $X_{\alpha_0} = X$; injectivity: as noted above). Transporting the well-order of $\alpha_0$ through this bijection, we obtain a well-order $\preceq$ on $X$ defined by \begin{align*} x \preceq y \iff F^{-1}(x) \leq F^{-1}(y). \end{align*}[/step]

[guided]Assume AC. Given an arbitrary set $X$, we must produce a well-ordering of $X$. The strategy: enumerate the elements of $X$ one by one, using AC at each stage to pick the "next" element, and continue transfinitely until $X$ is exhausted. First we prepare a selector. For each proper subset $A \subsetneq X$, the complement $X \setminus A$ is non-empty. AC applied to the family $\{X \setminus A : A \subsetneq X\}$ gives a function \begin{align*} \gamma: \mathcal{P}^*(X) &\to X, & \gamma(A) \in X \setminus A. \end{align*} Think of $\gamma(A)$ as "the next element after we've used $A$ already". Now we recursively build up an enumeration. We need a "halt" value for when the enumeration has exhausted $X$; pick any $\star \notin X$. Define \begin{align*} F(\alpha) := \begin{cases} \gamma(\{F(\beta) : \beta < \alpha\}) & \text{if } \{F(\beta) : \beta < \alpha\} \subsetneq X, \\ \star & \text{otherwise}. \end{cases} \end{align*} This is a legitimate definition by the Transfinite Recursion Theorem: at each stage $\alpha$, we look at everything enumerated so far, check whether it already covers $X$, and if not, apply $\gamma$ to pick something new. Writing $X_\alpha := \{F(\beta) : \beta < \alpha, F(\beta) \neq \star\}$, we can express this as: $F(\alpha) = \gamma(X_\alpha)$ so long as $X_\alpha \neq X$, and $F(\alpha) = \star$ otherwise. **The values are pairwise distinct until we hit $\star$.** At stage $\alpha$, if $F(\alpha) \neq \star$, then $F(\alpha) = \gamma(X_\alpha) \in X \setminus X_\alpha$, so $F(\alpha) \notin X_\alpha = \{F(\beta) : \beta < \alpha\}$. Thus the non-$\star$ portion of the sequence is injective. **The enumeration must halt.** Why can't the enumeration continue through every ordinal? If it did, $F$ would give an injection from the class $\mathrm{Ord}$ of all ordinals into $X$. But by [Hartogs' Theorem](/theorems/1472) — a theorem of ZF that does NOT need AC — there is an ordinal $\kappa$ that does not inject into $X$. Restricting our injection to $\kappa$ would give $\kappa \hookrightarrow X$, contradiction. So there is some least $\alpha_0$ with $F(\alpha_0) = \star$. **The halt happens exactly when $X$ is exhausted.** At stage $\alpha_0$, we have $F(\alpha_0) = \star$, which by definition of the recursion means $X_{\alpha_0} = X$. The map \begin{align*} F\big|_{\alpha_0}: \alpha_0 &\to X \end{align*} is a bijection: surjective because $X_{\alpha_0} = X$, injective by the distinctness established above. Pull the well-order of $\alpha_0$ across this bijection: declare $x \preceq y$ iff $F^{-1}(x) \leq F^{-1}(y)$. This gives a well-order on $X$. Why did AC enter? Only in the selector $\gamma$: we made a single application of AC to pick one element from each non-empty complement, and then the recursion used that fixed $\gamma$ without making further choices.[/guided]

[step:Derive AC from Well-Ordering by taking least elements] Assume the Well-Ordering Principle. Let $\{A_i : i \in I\}$ be a family of non-empty sets. Let \begin{align*} Y := \bigcup_{i \in I} A_i. \end{align*} By the Well-Ordering Principle, there exists a well-order $\leq$ on $Y$. For each $i \in I$, the set $A_i \subseteq Y$ is non-empty, so by the defining property of a well-order it has a least element \begin{align*} m_i := \min\nolimits_{\leq} A_i \in A_i. \end{align*} Define \begin{align*} f: I &\to Y, & f(i) := m_i. \end{align*} Then $f(i) = m_i \in A_i$ for every $i \in I$, so $f$ is a choice function for $\{A_i : i \in I\}$. [/step]

[step:Close the cycle] We have shown (1) $\Rightarrow$ (2) $\Rightarrow$ (1) $\Rightarrow$ (3) $\Rightarrow$ (1). The first two links give (1) $\iff$ (2). Chaining (1) $\Rightarrow$ (3) $\Rightarrow$ (1) together with (1) $\iff$ (2) yields (3) $\iff$ (1) $\iff$ (2). Hence all three statements are equivalent over ZF. [/step]