A proof of $ZF \vdash AC^L$

I'm studying Set Theory on my own and I have a question about a proof. The book I am reading wants to prove $ZF \vdash (AC)^L$ in order to prove the relative consistency of AC from ZF. I have no problems with the proof of the following theorem:

1) $ZF \vdash (V = L)^L.$

Here comes the problem: my book is a bit concise and I am not sure if the following proof of mine is correct. It would be very kind if you could check it:

We have a formula $\Phi$ which is $\exists \xi \psi$ where $\psi$ is $\Delta^{ZF}_1$ (I do not know if you are familiar with this $\psi$ but it should be the canonical well-ordering of $L$), so from 1 we have $$ZF \vdash \forall x \in L (\Phi \text{ Well orders } x)^L$$ which is equivalent to $$ZF \vdash \forall x \in L (\Phi^L \text{ Well orders } x)$$ (because the formula $\Phi^L \text{ Well orders } x$ is $\Delta_1^{ZF}$)

which is equivalent to $$ZF \vdash \forall x \in L (\Phi \text{ Well orders } x)$$ (because $\Phi$ is $\exists \xi \psi$ and all the ordinals are in $L$)

which is $$ZF \vdash WOT^L$$ (where WOT is the Well Ordering Theorem)

But also $ZF \vdash WOT \leftrightarrow AC$ so $ZF \vdash AC^L$.

QED?

Note: The last passage works because we have $ZF \vdash WOT^L \leftrightarrow AC^L$ because $WOT \leftrightarrow AC$ is $\Delta_1^{ZF}$.

-

If you write out in the obvious way the equivalence $WOT\iff AC$, it won't be $\Delta_1$; the ony reason it's $\Delta_1^{ZF}$ is that it's provable in ZF (hence provably equivalent to $0=0$).

My general impression of your argument is that you're making things unnecessarily complicated. Once you have that ZF proves the relativizations to $L$ of the axioms of ZF and of $V=L$, then it follows by general logic (not anything specific to set theory) that "ZF + ($V=L$)" is consistent if ZF is. Since AC is provable in the theory "ZF + ($V=L$)", it follows (still by general logic) that "ZF + AC" is consistent if ZF is.

-
I suppose you mean 0 = 0, a tautology. I know I am making things a bit too complicated but for reasons which would take too long to explain I need an explicit proof of $ZF \vdash AC^L$. – Archbishop Jul 9 '12 at 17:01
@Archbishop: Thanks for the correction; I've edited it into the answer. For an explicit proof of $AC^L$ in ZF, take the proof of AC from ZF plus $V=L$; relativize everything to $L$; and, wherever the original proof used $V=L$ or a ZF-axiom $\alpha$, insert the proof from ZF of $(V=L)^L$ or of $\alpha^L$. Depending on how you formalized logic, you may also need to insert justifications for the relativizations of logical axioms and rules. This is what I had in mind with "general logc" in my answer. – Andreas Blass Jul 9 '12 at 17:11
Thank you very much for the tautology thing. I totally missed it. Now even the Drake's proof makes sense. He proves that $ZF \vdash (V=L)^L$ and $ZF \vdash V=L \rightarrow AC$. Then he claims $ZF \vdash AC^L$ and that is because $V=L \rightarrow AC$ is equivalent to $0 = 0$, so we also have $ZF \vdash (V=L)^L\rightarrow AC^L$ (and L is a model of ZF). – Archbishop Jul 9 '12 at 17:28

The usual strategy is to define inductively a well-ordering on $L(\alpha)$ for each ordinal $\alpha$. Since under the assumption $V=L$, any set $x \in L (or$ $V), x\subseteq L(\beta)$ for some $\beta \in ORD$, thus $x$ is well-orderable. I guess your approach is correct. I suppose the canonical well-ordering you are talking about is as that in Kunen's book.

-
It is from Drake's book, but it should be more or less the same, if I remember correctly. – Archbishop Jul 9 '12 at 17:03