Proving that the axiom of choice implies the well-ordering principle I am trying to prove that Axiom of choice implies well-ordering principle.
Proof: If $A = \emptyset,$ then, take $\alpha = 0$ and' $\alpha \cong $ 
So given a nonempty set $A$, $\exists a_0 \in A$. Define by recursion, the following function $F:ON \rightarrow V$ 
$$F(\alpha)=\begin{cases}
\alpha_0,&\text{if }\alpha=1\\
F(\beta)\cup\{x\},&\text{if }\alpha=\beta+1\text{ and }A\setminus F(\beta\ne\varnothing\text{ and }x\in A\setminus F(\beta)\\
\bigcup_{\beta<\alpha}F(\beta),&\text{if }\alpha\text{ is a limit ordinal}\\
F(\beta),&\text{if }\alpha=\beta+1\text{ and }A\setminus F(\beta)=\varnothing\;.
\end{cases}$$
What do you think, Is this ok? If yes, I was thinking of continuing by induction on this function. But I am not sure what is there left to prove. we do know, by the recursion thm, that the function exists uniquely. Do we know whether it is well-defined?
Thank you!
Shir
By the way, how can I add left brackets, in Latex, to definition of this function?
 A: You did right to begin with the case where $A$ is empty, indeed it is well-ordered as it is itself an ordinal. So we can assume that $A$ is not empty.
The first and foremost is that you're not using the axiom of choice. What you should have done was to say "Fix $g$ to be a choice function from $\mathcal P(A)\setminus\{\varnothing\}$" at the beginning, and then $g$ is your bootstrap.
Meaning, $a_0$ is not some arbitrary element, it is $g(A)$. In the successor step, you don't add some arbitrary $x$, you take $g(A\setminus\{x_\beta\mid\beta<\alpha\})$. As it stands the successor case is completely not well-defined. There might be many $x\notin A\setminus F(\beta)$.
Finally, you should also begin with $\alpha=0$ and not $\alpha=1$.
The idea behind the proof is that it completely avoids arbitrary choices, because you have a uniform way of making that choice: $g$ whose existence is assured by the axiom of choice (yes, $g$ itself is arbitrary, but that's the only arbitrary choice you are going to make here).
A: I think you are close, but not quite there.  In particular, you haven't really defined a function anywhere.
Note that by $\mathsf{AC}$ if $A$ is nonempty there is a choice function $c$ for $\mathcal{P} ( A ) \setminus \{ \varnothing \}$.  Note, also, by various simple properties of ordinals, there is an ordinal $\delta$ such that there is no injection $\delta \to A$.
We can now start applying the Recursion Theorem to the following function $F$ (where $*$ is some object not in $A$):
$$F( \langle x_\xi \rangle_{\xi < \alpha} ) = 
\begin{cases}
c ( A \setminus \{ x_\xi : \xi < \alpha \} ), &\text{if }* \notin \{ x_\xi : \xi < \alpha \} \subsetneq A\\
*, &\text{otherwise.}
\end{cases}$$
(So the domain of $F$ is transfinite sequences in $A \cup \{ * \}$, and the range of $F$ is $A \cup \{ * \}$.)
The Recursion Theorem then yields a $\delta$-sequence $\langle x_\xi \rangle_{\xi < \delta}$ such that $$x_\alpha = F ( \langle x_\xi \rangle_{\xi < \alpha} )$$ for all $\alpha < \delta$.  Note that each element of $A$ can appear at most once in this sequence, and by choice of $\delta$ it must be that $x_\alpha = *$ for some $\alpha < \delta$.
