Georg Cantor considered the well-ordering theorem to be a "fundamental principle of thought".^[4] However, it is considered difficult or even impossible to visualize a well-ordering of ${\displaystyle \mathbb {R} }$ ; such a visualization would have to incorporate the axiom of choice.^[5] In 1904, Gyula Kőnig claimed to have proven that such a well-ordering cannot exist. A few weeks later, Felix Hausdorff found a mistake in the proof.^[6] It turned out, though, that in first-order logic the well-ordering theorem is equivalent to the axiom of choice, in the sense that the Zermelo–Fraenkel axioms with the axiom of choice included are sufficient to prove the well-ordering theorem, and conversely, the Zermelo–Fraenkel axioms without the axiom of choice but with the well-ordering theorem included are sufficient to prove the axiom of choice. (The same applies to Zorn's lemma.) In second-order logic, however, the well-ordering theorem is strictly stronger than the axiom of choice: from the well-ordering theorem one may deduce the axiom of choice, but from the axiom of choice one cannot deduce the well-ordering theorem.^[7]

There is a well-known joke about the three statements, and their relative amenability to intuition:

The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn's lemma?^[8]

The well-ordering theorem follows from the axiom of choice as follows.^[9]

Let the set we are trying to well-order be ${\displaystyle A}$ , and let ${\displaystyle f}$  be a choice function for the family of non-empty subsets of ${\displaystyle A}$ . For every ordinal ${\displaystyle \alpha }$ , define an element ${\displaystyle a_{\alpha }}$  that is in ${\displaystyle A}$  by setting ${\displaystyle a_{\alpha }\ =\ f(A\smallsetminus \{a_{\xi }\mid \xi <\alpha \})}$  if this complement ${\displaystyle A\smallsetminus \{a_{\xi }\mid \xi <\alpha \}}$  is nonempty, or leave ${\displaystyle a_{\alpha }}$  undefined if it is. That is, ${\displaystyle a_{\alpha }}$  is chosen from the set of elements of ${\displaystyle A}$  that have not yet been assigned a place in the ordering (or undefined if the entirety of ${\displaystyle A}$  has been successfully enumerated). Then the order ${\displaystyle <}$  on ${\displaystyle A}$  defined by ${\displaystyle a_{\alpha }<a_{\beta }}$  if and only if ${\displaystyle \alpha <\beta }$  (in the usual well-order of the ordinals) is a well-order of ${\displaystyle A}$  as desired, of order type ${\displaystyle \sup\{\alpha \mid a_{\alpha }{\text{ is defined}}\}}$ .

The axiom of choice can be proven from the well-ordering theorem as follows.

To make a choice function for a collection of non-empty sets, ${\displaystyle E}$ , take the union of the sets in ${\displaystyle E}$  and call it ${\displaystyle X}$ . There exists a well-ordering of ${\displaystyle X}$ ; let ${\displaystyle R}$  be such an ordering. The function that to each set ${\displaystyle S}$  of ${\displaystyle E}$  associates the smallest element of ${\displaystyle S}$ , as ordered by (the restriction to ${\displaystyle S}$  of) ${\displaystyle R}$ , is a choice function for the collection ${\displaystyle E}$ .

An essential point of this proof is that it involves only a single arbitrary choice, that of ${\displaystyle R}$ ; applying the well-ordering theorem to each member ${\displaystyle S}$  of ${\displaystyle E}$  separately would not work, since the theorem only asserts the existence of a well-ordering, and choosing for each ${\displaystyle S}$  a well-ordering would require just as many choices as simply choosing an element from each ${\displaystyle S}$ . Particularly, if ${\displaystyle E}$  contains uncountably many sets, making all uncountably many choices is not allowed under the axioms of Zermelo-Fraenkel set theory without the axiom of choice.

• Mizar system proof: http://mizar.org/version/current/html/wellord2.html