Its dangerous to go alone. Take this!

So, finally, this is part 4 of my series about the irrefutability of the AC from ZF. We are almost there!

Theorem 1: Let ZF-Formulae \phi_0(\vec{x}),\ldots,\phi_n(\vec{x}) be given. Then \forall_\alpha\exists_{\beta\ge\alpha}\forall_{\vec{x}\in V_\beta} \bigwedge\limits_{i=0}^n (\phi_i(\vec{x})\leftrightarrow\phi_i^{V_\beta}(\vec{x})). We then say that V_\beta reflects the \phi_i.
Proof: Let \alpha be given. Without loss of generality we may assume that the \phi_i can be written without universal quantifiers, as we can replace every universal quantifier by a negated existential quantifier of the negated quantfied formula.
Recursively define a sequence \left<\beta_n \mid n<\omega\right> where \beta_0=\alpha and \beta_{n+1} is the smallest ordinal \gamma>\beta_n, such that if \exists_y\theta(\vec{z},y) is a subformula of one of the \phi_i, we have \forall_{\vec{z}\in V_{\beta_n}}((\exists_y\theta(\vec{z},y))\rightarrow\exists_{y\in V_\gamma}\theta(\vec{z},y)). Let \beta be the supremum of the \beta_i. It is sufficient to show that for all subformulae \psi(\vec{z}) of any \phi_i we have \forall_{\vec{z}\in V_\beta}(\psi(\vec{z})\leftrightarrow\psi^{V_\beta}(\vec{z})), which goes by structural induction. If \psi is of the form x\in y this is trivial. The step over \rightarrow,\wedge,\bot is clear. We can assume that every occurence of \forall is in the scope of an occurence of \exists, and therefore, instead of having an induction step for \forall, we have an induction step for \exists: \psi=\exists_y\theta(\vec{z},y), and let \vec{z}\in V_\beta. By induction hypothesis, \psi^{V_\beta}(\vec{z})\rightarrow\psi(\vec{z}). For the other direction, let \exists_y\theta(\vec{z},y), then \exists_y\in V_{\beta_{n+1}}\theta(\vec{z},y). By induction hypothesis, we have \exists_{y\in V_\beta}\theta^{V_\beta}(\vec{z},y).

We can do everything we did in Part 1 as well directly in ZF. Alphabets become sets, and formulae become finite sequences. Especially, there is a set of all formulae, which is countable. Notice that there is no need to fix a special "encoding" for formulae, it is clear that one exists, and it is clear that all such encodings have to be equivalent. For a ZF-formula \phi, let \lceil\phi\rceil be its embedding into ZF, that is, \lceil\phi\rceil is a set.

For every set u we can define an interpretation, interpreting \in by \{\left<x,y\right>\in u\times u \mid x\in y\}. We write u\models \phi if this interpretation (for all valuations) models \lceil\phi\rceil, notice that in this case, \models is a relation inside ZF. Trivially, we have \forall_{\vec{a}\in u}((u\models\phi(\vec{a})) \Leftrightarrow\phi^u(\vec{a})).

Definition: Now we can define the class of OD of ordinal definable sets:

OD:=\{x \mid \exists_{\alpha\in On}\exists_{\vec{p}\in\alpha}\exists_{\lceil\phi\rceil} x=\{y\in V_\alpha \mid  V_\alpha\models \phi(y,\vec{p})\}\}

where we write \exists_{\lceil\phi\rceil} to denote that there must exist an encoded ZF-formula.

This class is interesting, as it messes around with the intuition about two meta-layers. However, it is not yet our goal.

Definition: The transitive closure TC(x) of a set x is the smallest y\supseteq x such that every element of y is also subset of y.

Definition: The class HOD of hereditary ordinal definable sets is defined by

HOD:=\{x \mid TC(\{x\})\subseteq OD\}

Since x\in TC(\{x\}), trivially HOD\subseteq OD.

Lemma 1: x\in HOD \Leftrightarrow x\in OD\wedge x\subseteq HOD.
Proof: "=>": From x\in HOD directly follows TC(\{x\}\subseteq OD, therefore, x\in OD. For y\in x we have TC(\{y\})\subseteq TC(\{x\})\subseteq OD\subseteq HOD, that is, y\in HOD, therefore, x\subseteq HOD.
"<=": For x\in OD and TC(\{x\})\subseteq HOD we have TC(\{x\})=\{x\}\cup\bigcup_{y\in x} TC(\{y\})\subseteq OD. Therefore, x\in HOD.

Lemma 2: For every ZF-formula \phi(x,\vec{y}) we have \forall_{\vec{\gamma}\in On}(\{x \mid \phi(x,\vec{\gamma})\}\in V\rightarrow\{x \mid \phi(x,\vec{\gamma})\}\in OD.
Proof: Let \{x \mid \phi(x,\vec{\gamma)}\in V, \alpha such that \{x \mid \phi(x,\vec{\gamma)}\in V_\alpha, and \vec{\gamma}<\alpha. By Theorem 1 there is a \beta\ge\alpha such that V_\beta reflects \phi, therefore \{x \mid \phi(x,\vec{\gamma})\} = \{x\in V_\beta \mid \phi^{V_\beta}(x,\vec{\gamma})\} = \{x\in V_\beta \mid V_\beta\models\phi(x,\vec{\gamma})\}\in OD.

Theorem 2: HOD is an inner model.
Proof: Due to Part 3, it is sufficient to show (I1), (I2) and (I3). By Lemma 1, (I1) holds.
Let x\subseteq HOD, and \alpha such that x\subseteq V_\alpha. Then trivially, x\subseteq V_\alpha\cap HOD. But by Lemma 2 we have V_\alpha\cap HOD=\{x \mid x\in V_\alpha\wedge x\in HOD\}\in OD. Trivially, we also have V_\alpha\cap HOD\subseteq HOD, so by Lemma 1, V_\alpha\cap HOD\in HOD. Thus, (I2) holds.
For (I3), let \phi(x,\vec{z}) be a \Sigma_0-formula, choose arbitrary \vec{z},u\in HOD, and let a=\{x\in u \mid \phi(x,\vec{z})\}. Then a\subseteq u\subseteq HOD by (I1), so by Lemma 1, it is sufficient to show that a\in OD. As HOD\subseteq OD we have \vec{z},u\in OD, therefore there are \vec{\lceil\phi\rceil},\lceil\psi\rceil and \vec{\alpha},\gamma\in On and for i=1,\ldots,n there are p_i\in \alpha_i^{<\omega}, q\in\gamma^{<\omega} sucht hat z_i = \{y\in V_{\alpha_i} \mid V_{\alpha_i}\models\phi_i(y,p_i)\} and u=\{y\in V_\gamma \mid V_\gamma\models\psi(y,q)\}. Let \alpha=\max\{\vec{alpha},\gamma\}, and \chi(x,y)=\lceil y=V_x\rceil. By Theorem 1 we get a \beta>\alpha such that V_\beta reflects \chi. Therefore

a=\{x\in V_\beta  \mid  V_\beta\models \exists_{\vec{w}}\exists_w(\chi(\gamma, w)\wedge
(\bigwedge\limits_{i=1}^n\chi(\alpha_i,w_i))\wedge
\exists_{\vec{v}}\forall_y (\psi^w(x,q)\wedge\phi(x,\wedge{v})\wedge\bigwedge\limits_{i=1}^n (y\in v_i\leftrightarrow\phi_i^{w_i}(y,p_i))))\}

which is in OD. Therefore, a\in HOD.

Lemma 3: There exists a surjective functor F:On\rightarrow OD.
Proof: In Part 2 we proved that there is a bijection G:On\rightarrow\omega\times On^{<\omega}, so it is sufficient to give a surjective functor F:\omega\times On^{<\omega}\rightarrow OD. Now let \left<\phi_n \mid n<\omega\right> be an enumeration of all ZF-formulae. Define

F(n,p) = \left\{\begin{array}{rl} \{x\in V_{p(m)} \mid V_{p(m)}\models\phi_n(x,p \mid _m)\} & \mbox{ for } \operatorname{dom}(p)=m+1 \\ \emptyset & \mbox{ otherwise}\end{array}\right.

Then F is surjective.

Lemma 4: There exists a surjective functor H:On\rightarrow HOD
Proof: Since HOD\subseteq OD, use H=F \mid _{HOD}.

Theorem: (AC) holds in HOD
Proof: By Lemma 4, we have our surjective H:On\rightarrow HOD. For \alpha\in On, define g_\alpha= H \mid _\alpha. By Lemma 2 we know that for every \alpha, g_\alpha\in OD, and since g_\alpha\subseteq HOD, we have g_\alpha\in HOD. Let u\in HOD be arbitrary but fixed. Then there exists an \alpha such that u\subseteq \operatorname{ran}(g_\alpha). Now define a well-ordering r\subseteq u\times u by

\{\left<x;y\right> \mid \min\{\gamma \mid x=g_\alpha(\gamma)\}<\min\{\gamma \mid y=g_\alpha(\gamma)\}

r is a well-ordering, and r\in HOD. Thus, in HOD, the well-ordering theorem holds, therefore, AC holds in HOD.