Solution (source code)

= Solution

For <Hartogs theorem>, collect all well-order relations on all subsets of a set $x$. They form a set, since the relations belong to the power set of $x\times x$. Replacement collects their <ordinal> order types in a set $T$. Define
$$
\alpha=\sup\{\beta+1:\beta\in T\}.
$$
If there were an injection $\alpha\to x$, transfer the well-order of $\alpha$ to its image. Its type would put $\alpha$ in $T$, giving $\alpha+1\leq\alpha$, impossible. Thus \b[some <ordinal> does not inject into $x$], without using choice.

Assume the <axiom of choice> and let a nonempty <partially ordered set> $P$ have an upper bound for every chain. Suppose it has no maximal element. Choose, from every subset of $P$ with a nonempty set of strict upper bounds, one such strict upper bound. Every chain has a strict upper bound: first take an upper bound and then a strictly larger element, using the absence of maximal elements. Take a Hartogs <ordinal> $\alpha$ for $P$. <Transfinite recursion> chooses $p_\beta$, for each $\beta<\alpha$, strictly above all previously chosen elements. Their predecessors form a chain at every stage, so this recursion is defined and strictly increasing. It gives an injection $\alpha\to P$, contradicting the choice of $\alpha$. Hence $P$ has a maximal element, proving <Zorn's lemma>.

For the <well-ordering theorem>, take a choice function on the nonempty subsets of $x$ and recursively choose an element of $x$ not previously selected. If this process had not exhausted $x$ at any stage below its Hartogs <ordinal> $\alpha$, it would define an injection $\alpha\to x$, again impossible. Therefore it exhausts $x$ at some <ordinal> stage $\beta<\alpha$. Order each element by its unique selection index; this transfers the <ordinal> well-order to all of $x$. The empty set is already well-ordered. These proofs use <transfinite recursion>, not an unstated fixed-point theorem.