Editing Zorn's lemma (section)

== Zorn's lemma implies the axiom of choice ==
A proof that Zorn's lemma implies the axiom of choice illustrates a typical application of Zorn's lemma.<ref>{{harvnb|Halmos|1960|loc=§ 16. Exercise.}}</ref> (The structure of the proof is exactly the same as the one for the [[Hahn–Banach theorem]].)

Given a set <math>X</math> of nonempty sets and its union <math>U := \bigcup X</math> (which exists by the [[axiom of union]]), we want to show there is a function
:<math>f : X \to U</math>
such that <math>f(S) \in S</math> for each <math>S \in X</math>. For that end, consider the set
:<math>P = \{ f : X' \to U \mid X' \subset X, f(S) \in S \}</math>.
It is partially ordered by extension; i.e., <math>f \le g</math> if and only if <math>f</math> is the restriction of <math>g</math>. If <math>f_i : X_i \to U</math> is a chain in <math>P</math>, then we can define the function <math>f</math> on the union <math>X' = \cup_i X_i</math> by setting <math>f(x) = f_i(x)</math> when <math>x \in X_i</math>. This is well-defined since if <math>i < j</math>, then <math>f_i</math> is the restriction of <math>f_j</math>. The function <math>f</math> is also an element of <math>P</math> and is a common extension of all <math>f_i</math>'s. Thus, we have shown that each chain in <math>P</math> has an upper bound in <math>P</math>. Hence, by Zorn's lemma, there is a maximal element <math>f</math> in <math>P</math> that is defined on some <math>X' \subset X</math>. We want to show <math>X' = X</math>. Suppose otherwise; then there is a set <math>S \in X - X'</math>. As <math>S</math> is nonempty, it contains an element <math>s</math>. We can then extend <math>f</math> to a function <math>g</math> by setting <math>g|_{X'} = f</math> and <math>g(S) = s</math>. (Note this step does not need the axiom of choice.) The function <math>g</math> is in <math>P</math> and <math>f < g</math>, a contradiction to the maximality of <math>f</math>. <math>\square</math>

Essentially the same proof also shows that Zorn's lemma implies the [[well-ordering theorem]]: take <math>P</math> to be the set of all well-ordered subsets of a given set <math>X</math> and then shows a maximal element of <math>P</math> is <math>X</math>.<ref>{{harvnb|Halmos|1960|loc=§ 17. Exercise.}}</ref>