How to formally use transfinite recursion to construct a sequence for a proof of Zorn's lemma I'm trying to get my head around how to prove that the axiom of choice implies Zorn's lemma using transfinite recursion:

Transfinite recursion I Let $G$ be a class function. Then there is class function $F$ from the class of ordinals so that for any ordinal $\alpha$ we have $F(\alpha) = G(F\restriction_\alpha)$.
Transfinite recursion II Let $G_1,G_2$ and $G_3$ be class functions. Then there is a class function $F$ from the class of ordinals that that

*

*$F(0) = G_1(0)$,


*for any ordinal $\alpha$, $F(\alpha + 1) = G_2(F(\alpha)),$


*for any limit ordinal $\lambda$, $F(\lambda) = G_3(F\restriction_\lambda).$

Before telling that this is a duplicate, hear me out. Most of the references on the matter I found on this site and on the internet at large contain only informal proofs or sketches. In particular, this answer by Asaf Karagila
https://math.stackexchange.com/a/97315/229776
advises to build a transfinite sequence of elements of a partially ordered set $(X,\leq)$ to find a maximal element with a choice function $f$ of $X$ by setting.
The book by Hrbacek and Jech ("Introduction to set theory") also uses Hartog's number $h(X)$ (the least ordinal not equipotent to any subset of $X$) to construct an $h(X)$-sequence.
The problem is that I simply can't see at the moment how we can formally use transfinite recursion theorems to construction a desired sequence. Any help would be appreciated.
 A: We can avoid the appeal to Hartogs numbers if we do an indirect proof instead. As a bonus, the transfinite recursion becomes a bit cleaner:
Assume that (a) $(P,\preceq)$ is a partially ordered set that satisfies the premises of Zorn's lemma, (b) $P$ has no maximal element, and (c) $C$ is a choice function on $P$. We then seek a contradiction.
Without loss of generality extend $C$ such that $C(\varnothing)=42$, no matter whether or not $42\in P$.
Apply Transfinite Recursion I to the class function
$$ G(X) = C(\{y\in P\mid \forall z\in \operatorname{Rng}(X)\cap P: z\prec y\}) $$
This gives a class function $F$ such that for every ordinal $\alpha$,
$$ F(\alpha) = C(\{y\in P \mid \forall \beta<\alpha : F(\beta)\in P \to F(\beta)\prec y\}) $$
Lemma. For all $\alpha$ it holds that $F(\alpha)\in P$ and $\forall \beta : F(\beta)\prec F(\alpha)$.
Proof. By transfinite induction on $\alpha$. The induction hypothesis tells us that $\{F(\beta)\mid \beta<\alpha\}$ is a chain in $P$ (note that it is a set in any case thanks to Replacement). The Zorn premises tells us that this chain has an upper bound; because there is no maximal element it even has a strict upper bound. In other words, $$\{y\in P \mid \forall \beta<\alpha : F(\beta)\in P \to F(\beta)\prec y\},$$ the set of all the strict upper bounds, is not empty, so $F(\alpha)$ is in $P$ and is greater than all the $F(\beta)$s.
The lemma tells us that $F$ is an order-preserving function from ON to $P$. Since $F$ preserves order, it is in particular injective. Therefore the formula
$$ H(x)=\alpha \iff F(\alpha)=x \lor (\alpha=117 \land  \forall\beta:F(\beta)\ne x) $$
is functional, and applying Replacement on $P$ and $H$ tells us that ON is a set. The Burali-Forti paradox now furnishes our desired contradiction.

Note that we never actually needed $C(\varnothing)=42$ except to make sure that $G$ was a class function so we could use the recursion theorem on it.
The proof structure here is typical: The definition by transfinite recursion is followed immediately by a transfinite induction that extracts useful facts from the recursion formula. This two-step approach is often necessary for using the general recursion machinery because we need to define $G$ in a defensive way such that we can prove that it is makes sense and is functional without depending on its argument being produced by recursion. This defensive scaffolding -- i.e., intersecting $\operatorname{Rng}(X)$ with $P$ so $z\prec y$ makes sense, and making sure that $C(\{x\in P\mid \cdots\})$ always means something even if the condition ends up filtering everything away -- is then cleaned away by the lemma once the recursive magic has done its job and we know the input to $G$ comes from a well-behaved recursion.

As an additional note, one might argue that this is not "morally" an indirect proof. The way I prefer to think about it is that I would like to assume just (a) and (c), and then in the middle of the proof of the lemma say

... this chain has an upper bound. If that upper bound is a maximal element, then we're done; otherwise there's something larger, which is therefore a strict upper bound ...

Claiming that "we're done" with the entire Zorn's Lemma when we were in the middle of an inner induction step is not really done in polite company, though. Phrasing the entire proof as an indirect proof will allow us to follow this intuition anyway, in simple yet formally acceptable way.
The part of the proof after the lemma is then just an argument that eventually we must hit one of the "we're done" conditions, because continuing forever would have absurd consequences.
A: Let $C$ be a choice function on $P.$ We can use your second transfinite recursion variation to define an ordinal sequence $F:\mathbf{Ord}\to P$ as follows:


*

*$F(0)= C(P)$

*If $F(\alpha)$ is maximal in $P$ let $F(\alpha+1) = F(\alpha).$ Otherwise the set $A=\{x\in P : x > F(\alpha)\}$ is nonempty and take $F(\alpha+1) = C(A).$

*For a limit ordinal $\lambda,$ we can see by induction that $F''(\lambda)$ is a chain. The assumption that every chain has an upper bound in $P$ means the set $$B=\{x\in P:\mbox{x is an upper bound for $F''(\lambda)$}\}$$ is nonempty. Let $F(\lambda) = C(B).$


To make the $G$'s total functions, simply define them arbitrarily for any case they aren't well-defined by the above (e.g. on things that aren't elements / subsets of $P$ or if the sets $A$ or $B$ are empty.). Induction shows that these cases never come up.
Here is where Hartog comes in. We know there is an ordinal $\alpha^*$ that does not inject into $P.$ Thus for some $\beta<\gamma < \alpha^*,$ we have $F(\beta)=F(\gamma).$ If $F(\beta)$ were not maximal, then $F(\beta+1)> F(\beta)$ so by the fact that $F$ is increasing, $F(\gamma)>F(\beta),$ contradicting the fact that $F(\gamma)=F(\beta).$ Thus $F(\beta)$ is maximal in $P$.
A: Yes, this issue baffled me for a long time as a student. Longer than I care to admit, for a matter of fact.
First, let's tackle the issue about Hartogs' theorem. You need to apply it in either case. The idea is that you construct something recursively, and this something is necessarily an injective function. You want to know that the process stabilizes at some point, and Hartogs' theorem says it has to stop at some ordinal, else we would have had an injection from the proper class of all the ordinals into our set.
Now. How to do this? Let's work backwards.
The goal is to construct a well-ordered chain that has an upper bound which is a maximal element. So $G_i$, or $G$ should provide you with a slightly longer chain if they are given a chain in the partial order. If they don't, we don't care.
Why don't we care? Because we are going to prove by induction, that our recursive application of the function always results in a chain. So anything else is irrelevant. 
Now, we use the choice function.


*

*For $x$ a subset of the partial order, $C(x)$ is a function choosing an upper-bound for $x$, which lies outside of $x$. If no such upper bound exists, then $x$ is not in the domain of $C$. Here we apply the axiom of choice.

*When $x$ is an order-preserving embedding from an ordinal $\alpha$ into the partial order with a bounded image, define $G(x)$ is $C(x)$. Namely, an upper bound that we can add to $x$.

*When $x$ is anything else, $G(x)=\varnothing$.
Now apply the transfinite recursion theorem. We get a function that tacks upper bound after another, and we will need to prove—by induction—that this is always a chain, and unless they are stabilized, they are different. So by Hartogs' theorem, there is a point where we must have stabilized, and this gives us the wanted result.
