 Proof outline of Zorn's lemma

Assume the axiom of choice and suppose a poset satisfying the hypothesis has no maximal element. Fix a choice function on its nonempty subsets. By transfinite recursion, choose at each ordinal stage an upper bound of the chain in a partial order already constructed, then choose a strictly larger member. Both choices are available, including the initial empty stage. This produces distinct members throughout the Hartogs ordinal of $P$, contradicting the Hartogs theorem. Thus a maximal element exists. Conversely, apply Zorn's lemma to partial choice functions on a family of nonempty sets, ordered by extension. A chain in a partial order has the compatible union as an upper bound, and a maximal element must be defined on the whole family, since one missing value could be adjoined.

Zorn's lemma was introduced in 1935 to shorten algebra proofs using choice or the well-ordering theorem.^[ref]