Axiom of Choice implies Well-Ordering Principle 
Axiom of Choice implies Well-Ordering Principle.


My textbook only presents the construction of function $F$ and does not provide details on how to define such well-ordering. I try to fill in the remaining blanks in my attempt. Does it look fine or contain logical flaws/gaps?
Thank you for your help!

My attempt:
Let $A$ be a set. By Axiom of Choice, there is a choice function $f:\mathcal{P}(A) \setminus \{\emptyset\} \to A$ such that $f(X) \in X$ for all $X \in \mathcal{P}(A) \setminus \{\emptyset\}$. Let $V$ be the class of all sets. We define a function $G:V \to V$ as follows: $$G(x)=\begin{cases}
f(A \setminus {\rm ran} (x))&\text{if }x\text{ is a function and }A \setminus {\rm ran} (x) \neq \emptyset\\A&\text{otherwise}\end{cases}$$
By Transfinite Recursion Theorem, there is a function $F: {\rm Ord} \to V$ such that $F(\alpha)=G(F \restriction \alpha)$ for all $\alpha \in {\rm Ord}$.


*

*There do not exist $\alpha_1<\alpha_2 \in {\rm Ord}$ such that $F(\alpha_1)=F(\alpha_2)=a$ for some $a\in A$
If not, $F(\alpha_1)=F(\alpha_2)=a$ for some $a\in A$. We have $F(\alpha_2)=G(F \restriction \alpha_2)$. There are only two cases.


*

*$F(\alpha_2)=A \neq a =F (\alpha_1)$

*$F(\alpha_2)=f(A \setminus {\rm ran} (F \restriction \alpha_2))$
$f(A \setminus {\rm ran} (F \restriction \alpha_2)) \in A \setminus {\rm ran} (F \restriction \alpha_2) \implies f(A \setminus {\rm ran} (F \restriction \alpha_2)) \notin {\rm ran} (F \restriction \alpha_2) \implies$ $F(\alpha_2) \notin {\rm ran} (F \restriction \alpha_2) \implies F(\alpha_2) \neq F(\alpha_1) \in {\rm ran} (F \restriction \alpha_2)$. 
Both cases lead to a contradiction.


*$A=F(\lambda)$ for some $\lambda < h(A)$ where $h(A)$ is the Hartogs number of $A$
If not, $A \neq F(\lambda)$ for all $\lambda < h(A)$ and consequently $F(\lambda) \in A$ for all $\lambda < h(A)$. Then $F \restriction h(A)$ is an injection from $h(A)$ to $A$ and thus $|h(A)| \le |A|$. This contradicts the definition of $h(A)$.


*$A={\rm ran} (F \restriction \beta)$ for some $\beta \in {\rm Ord}$
Let $\beta = \min \{\lambda \in {\rm Ord} \mid A=F(\lambda)\}$. Then $F(\alpha) \in A$ for all $\alpha<\beta$. If not, $F(\alpha) = A$ for some $\alpha<\beta$. This contradicts the minimality of $\beta$. It follows that ${\rm ran} (F \restriction \beta) \subseteq A$. Moreover, $F(\beta)=A \implies G(F \restriction \beta)=A \implies A \setminus {\rm ran} (F \restriction \beta) =\emptyset \implies A \subseteq {\rm ran} (F \restriction \beta)$.
To sum up, ${\rm ran} (F \restriction \beta) = A$. Hence $F \restriction \beta$ is a bijection from $\beta$ to $A$. We define an ordering $\prec$ on $A$ by $a\prec b \iff F^{-1}(a) < F^{-1}(b)$ for all $a,b\in A$. Since $F \restriction \beta$ is a bijection from $\beta$ to $A$, $F \restriction \beta$ is an isomorphism between $(\beta,<)$ and $(A,\prec)$.
Since $<$ is a well-ordering on $\beta$, so is $\prec$ on $A$.
 A: Here's the usual approach. Define $G$ on ordinals, rather than arbitrary sets, by transfinite recursion. Explicitly $$G(\alpha):=f(\{x\in A|\forall\beta\in\alpha (G(\beta)\ne x)\}).$$Obviously, $G$ never takes the same value twice.
If $G(\alpha)$ exists for every ordinal $\alpha$, all ordinals can be injected into $A$, contradicting replacement and the Burali-Forti paradox.
Therefore $G(\alpha)$ is undefined for some minimal ordinal $\alpha$, and then $\{x\in A|\forall\beta\in\alpha (G(\beta)\ne x)\}=\emptyset$ (because $f(B)$ exists for any non-empty subset of $A$), i.e. $A=\{G(\beta)|\beta\in\alpha\}$. This provides a well-ordering of $A$ isomorphic to the $\in$ ordering of $\alpha$.
Incidentally, the well-ordering principle also implies the axiom of choice. To invent a choice function $f$ on some set $X$ with $\emptyset\not\in X$, well-order $Y:=\bigcup X$. Any $y\in X$ is a non-empty subset of $Y$. Then define $f(y)$ as the minimum element of $y$.
A: 
Let $V$ be the class of all sets. We define a function $G: V\rightarrow V$ as follows: [...]

Nope, that's not valid in Zermelo-Fraenkel (ZFC), because ZFC has no proper classes at all.  So you can't have a "class of all sets," much less use it as the domain and codomain of a function!  If you want to use something other than ZFC, you have to say so explicitly, but your proof doesn't say anything of the sort.
(Good ideas for "something other than ZFC" include NBG and NF(U), depending on what you are trying to achieve.)

Your argument can be interpreted as a metatheoretical "proof that there is a proof" of the Well-Ordering Theorem.  But WOT is a straightforward theorem of ZFC.  It should not require the use of metatheory to prove.  Contrast for example Goodstein's theorem, which cannot be proven from within Peano Arithmetic and therefore does require the use of metatheory.
