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})](/latex?n=dcc3bd6b40b68d23d832766deb69a727c003ac45deb80524cd5a4ce54f01dfac)
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}))](/latex?n=a10429120e49211309aa00bc0afba4c1be983ea1f3a36b1720947c3d85d92a81)
. We then say that
reflects the
![\phi_i](/latex?n=f1d6855a081559259d2acaebaada3a01cd0ce444a2e41e7dac4c1d01379fec03)
.
Proof: Let
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
be given. Without loss of generality we may assume that the
![\phi_i](/latex?n=f1d6855a081559259d2acaebaada3a01cd0ce444a2e41e7dac4c1d01379fec03)
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>](/latex?n=002e453c55b01971286c61b0a47a851faf2f834c444ada440d2380b7beee801a)
where
![\beta_0=\alpha](/latex?n=95d480b2f4031fb48b45b3a406738d8d47e3f6d865af206c704b5716ce05d944)
and
![\beta_{n+1}](/latex?n=9c4856995034a9c5b404a6f98c17253410e2439c017d2244ebb70b8dfc82f4bf)
is the smallest ordinal
![\gamma>\beta_n](/latex?n=cb12fae6ea0edddc1f44cfbb6c8a10244e362dbd9e5710df0fc2d88a2c4b5cca)
, such that if
![\exists_y\theta(\vec{z},y)](/latex?n=30070b76a38b4b73c17097ee9b2db02cf3c990fbe83034d1c4d1c17033545ce0)
is a subformula of one of the
![\phi_i](/latex?n=f1d6855a081559259d2acaebaada3a01cd0ce444a2e41e7dac4c1d01379fec03)
, 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))](/latex?n=9fbaec4559524975e0003b0a5f31a989270afef5acd9340d55bcf4d36e266798)
. Let
![\beta](/latex?n=f3f3804480e8551ac91a68ccc198310e514ec1424346595aca42a3a558ddee0a)
be the supremum of the
![\beta_i](/latex?n=6cb4d369799123ceafb5a8a07522910a7f73e17725edda11a20e5aab7864d385)
. It is sufficient to show that for all subformulae
![\psi(\vec{z})](/latex?n=515c512e2854d9497d057991e57d5adec9f60c2bca7ece93fbf4e14867d88373)
of any
![\phi_i](/latex?n=f1d6855a081559259d2acaebaada3a01cd0ce444a2e41e7dac4c1d01379fec03)
we have
![\forall_{\vec{z}\in V_\beta}(\psi(\vec{z})\leftrightarrow\psi^{V_\beta}(\vec{z}))](/latex?n=0d3a11a32ebe9caf21ad264425f265c54433b389c71e8672146ffd4d7e9c1812)
, which goes by structural induction. If
![\psi](/latex?n=f301f970eb09c336d31954a22511ffad807e5a02b0371810267307048c281891)
is of the form
![x\in y](/latex?n=5c6d0e4dc8ad11c8d04112e9e183baa16120a8649eb08ac4198611b129b02a4e)
this is trivial. The step over
![\rightarrow,\wedge,\bot](/latex?n=a64b3d8a15e508a5d08b412e8aeef322a8a284bb400b350edac71537d7ed844b)
is clear. We can assume that every occurence of
![\forall](/latex?n=4ec4830bef761b7afdff1dbec2d68ed999ce4c9c549a84358533419d586d0cd3)
is in the scope of an occurence of
![\exists](/latex?n=b161bf60d6b2d19d2332e712957bbde783cc75e0f8fc505bbee1833fe4cdb8a6)
, and therefore, instead of having an induction step for
![\forall](/latex?n=4ec4830bef761b7afdff1dbec2d68ed999ce4c9c549a84358533419d586d0cd3)
, we have an induction step for
![\exists](/latex?n=b161bf60d6b2d19d2332e712957bbde783cc75e0f8fc505bbee1833fe4cdb8a6)
:
![\psi=\exists_y\theta(\vec{z},y)](/latex?n=235abae0440b3d8a22f220d9719241a371bbc9be155aaafbdf80c600e09cfd3f)
, and let
![\vec{z}\in V_\beta](/latex?n=53da8d2e1caf49871831fb6c8784a86f5c102247f61ea826e0c2d5c458a02a08)
. By induction hypothesis,
![\psi^{V_\beta}(\vec{z})\rightarrow\psi(\vec{z})](/latex?n=7d61fabf95d57585d9248321af275fdc0482b2dc4c6ed48c50d11f552153ce4d)
. For the other direction, let
![\exists_y\theta(\vec{z},y)](/latex?n=30070b76a38b4b73c17097ee9b2db02cf3c990fbe83034d1c4d1c17033545ce0)
, then
![\exists_y\in V_{\beta_{n+1}}\theta(\vec{z},y)](/latex?n=a8f1929733fb5dc0c515b7f0f4c9938d26049c40658310003c5aa91fb046ed1d)
. By induction hypothesis, we have
![\exists_{y\in V_\beta}\theta^{V_\beta}(\vec{z},y)](/latex?n=59b2e06eb19512cedc3073c6321d06d01de5f5caeddf0feeb5b3cfa6d75dcd21)
.
□
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](/latex?n=10ce0200b450ea955833553e717821c7721818b8a95cffd7e54b46e08918b512)
, let
![\lceil\phi\rceil](/latex?n=2ffad94cc899e645ac26c59d1b0478a2640357191d03003ca7ba699301ed04dd)
be its embedding into ZF, that is,
![\lceil\phi\rceil](/latex?n=2ffad94cc899e645ac26c59d1b0478a2640357191d03003ca7ba699301ed04dd)
is a set.
For every set
![u](/latex?n=0bfe935e70c321c7ca3afc75ce0d0ca2f98b5422e008bb31c00c6d7f1f1c0ad6)
we can define an interpretation, interpreting
![\in](/latex?n=729f2cd8398e996012ccabf10defcacca4f5c7343e72484f631eba1d210bc9ad)
by
![\{\left<x,y\right>\in u\times u \mid x\in y\}](/latex?n=c0be928dba5ef5d85ca32bcd5e443048cb80d74fbaf93b1756bf841a29f08634)
. We write
![u\models \phi](/latex?n=5a8120ea0cab267aea29f717f3e69f277bc07ee5392319162bbee6de97466470)
if this interpretation (for all valuations) models
![\lceil\phi\rceil](/latex?n=2ffad94cc899e645ac26c59d1b0478a2640357191d03003ca7ba699301ed04dd)
, notice that in this case,
![\models](/latex?n=7997c4f3be17c7ce998bd9f46b9abbeb9a8c4a26e57cd6f8839c029d91c2b550)
is a relation inside ZF. Trivially, we have
![\forall_{\vec{a}\in u}((u\models\phi(\vec{a})) \Leftrightarrow\phi^u(\vec{a}))](/latex?n=039e3824b654ef403f7c9c13c510de650cf57f5af462f4665b6c4ab461e84fc4)
.
Definition: Now we can define the class of
![OD](/latex?n=d7fcf32ee8e1cd3eef022fead751340276a82cd865ccaabc42af0a680ab8387d)
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})\}\}](/latex?n=db0993ec99b3541386fb814eccf5a9a02b365bb63716566b820c406b01531df9)
where we write
![\exists_{\lceil\phi\rceil}](/latex?n=8692652ee0c5bcaccc95cde327327e2e440266ad8170e98a2c73cd727e6fa1b8)
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)](/latex?n=3bf8a045db8b8f1ff10a514b3e082aca8ce9ccfb624b71ad4ff4c55fa6c64755)
of a set
![x](/latex?n=2d711642b726b04401627ca9fbac32f5c8530fb1903cc4db02258717921a4881)
is the smallest
![y\supseteq x](/latex?n=74ff2d39c2824043cddef0e80d47b24798ea23d32e3feccb64099cedfd58cc1e)
such that every element of
![y](/latex?n=a1fce4363854ff888cff4b8e7875d600c2682390412a8cf79b37d0b11148b0fa)
is also subset of
![y](/latex?n=a1fce4363854ff888cff4b8e7875d600c2682390412a8cf79b37d0b11148b0fa)
.
Definition: The class
![HOD](/latex?n=03a965247dd8ae5eceea306659a20d1ac18bbd68dfa0c9d231fa3e9b0f981426)
of
hereditary ordinal definable sets is defined by
![HOD:=\{x \mid TC(\{x\})\subseteq OD\}](/latex?n=f6358581e8b9d10c51d1238c51e9d60364dc5250733acb041b6f2731c6350d3b)
Since
![x\in TC(\{x\})](/latex?n=bc53520aa806fef9bd6412322debd7220db218befded3960d6e750508c54f0da)
, trivially
![HOD\subseteq OD](/latex?n=6656434c0bc2f31eb8914723c5557a6ffd6bf59b2799584aacbb05af8cdff314)
.
Lemma 1: ![x\in HOD \Leftrightarrow x\in OD\wedge x\subseteq HOD](/latex?n=9453d778b3203da5fafba57520b695cc6218bc7800822020662c4b403ea36af7)
.
Proof: "=>": From
![x\in HOD](/latex?n=8ed6d524f1ad95d2fc57b6a5aa058e89d0b94731038843ae5be8c99efa45c390)
directly follows
![TC(\{x\}\subseteq OD](/latex?n=0fe59538af534faef5bbe2084105bf47f94b0fafb3e27c439c4f953a2a81dacd)
, therefore,
![x\in OD](/latex?n=e2c32dfecb84c7971ea6fb611eabfb522cded8399101b8f2df5a3005c02fc2ed)
. For
![y\in x](/latex?n=e51268f91ec40cd948035eccdab1d6faa7b34cdb9e9a37f95b498c63022e739b)
we have
![TC(\{y\})\subseteq TC(\{x\})\subseteq OD\subseteq HOD](/latex?n=8bab71c6de603dab46882d97f286ffbaf9aaf2df6309627fd81e74e80944f8cd)
, that is,
![y\in HOD](/latex?n=7b1fdf1ecb2798b152f6da8f9e714709944c57c2008faa6eb07832e21c8e0c95)
, therefore,
![x\subseteq HOD](/latex?n=4471b84a60dc08dca2fb7e07cb63d7dcc608d6122e09771578b68e2876b186a4)
.
"<=": For
![x\in OD](/latex?n=e2c32dfecb84c7971ea6fb611eabfb522cded8399101b8f2df5a3005c02fc2ed)
and
![TC(\{x\})\subseteq HOD](/latex?n=83710cc8bb3810ec3cd9e2223b69bf6d98525762d13a6af6edd37219d3f38151)
we have
![TC(\{x\})=\{x\}\cup\bigcup_{y\in x} TC(\{y\})\subseteq OD](/latex?n=f4d19458627271463d6dbe1777976aa203d4cfe4cc54e173f8c2c7d1afb6688c)
. Therefore,
![x\in HOD](/latex?n=8ed6d524f1ad95d2fc57b6a5aa058e89d0b94731038843ae5be8c99efa45c390)
.
□
Lemma 2: For every ZF-formula
![\phi(x,\vec{y})](/latex?n=a09fe231d8713bb330c6bdb8291ee5433ada98f73289eefe9a758145601ad957)
we have
![\forall_{\vec{\gamma}\in On}(\{x \mid \phi(x,\vec{\gamma})\}\in V\rightarrow\{x \mid \phi(x,\vec{\gamma})\}\in OD](/latex?n=e5f5bed6c1fba530eaecd9fe452de147c8d6aeda7aaa07284881e93a6a1a4c14)
.
Proof: Let
![\{x \mid \phi(x,\vec{\gamma)}\in V](/latex?n=8d16a372d06c15fc54760a9efc5975c5418ab8631c867a8a85555051c00a577a)
,
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
such that
![\{x \mid \phi(x,\vec{\gamma)}\in V_\alpha](/latex?n=8ad83e9efee0e3d4ede0a22632de92579b0676458ec843aafa3795bfdf9bf669)
, and
![\vec{\gamma}<\alpha](/latex?n=2323efaca7a4bc40e9614f86b1363cf7f0f388719c185f040adc0a5397c55557)
. By Theorem 1 there is a
![\beta\ge\alpha](/latex?n=2ab194a8be979eff845921a77f2816dc2f0e94f4987aad5a71a7068f13f395a6)
such that
![V_\beta](/latex?n=0bf9bc170ad957d9c9881e165c651c7e34b65be9ccaa66f9e1cc1abcf463333c)
reflects
![\phi](/latex?n=10ce0200b450ea955833553e717821c7721818b8a95cffd7e54b46e08918b512)
, 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](/latex?n=2987cc40ba276b3600208cd4db80c28f29975f912847afba5fd6ab7d90672468)
.
□
Theorem 2: ![HOD](/latex?n=03a965247dd8ae5eceea306659a20d1ac18bbd68dfa0c9d231fa3e9b0f981426)
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](/latex?n=4471b84a60dc08dca2fb7e07cb63d7dcc608d6122e09771578b68e2876b186a4)
, and
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
such that
![x\subseteq V_\alpha](/latex?n=42bdf475a0ed119f4322d81aab11c4bdb975dbfa7ab0c667e4ce38c2dcb13beb)
. Then trivially,
![x\subseteq V_\alpha\cap HOD](/latex?n=d189db3cb365f44a427595fa346ba9a4deea25dd8016497b042b67f053adc456)
. But by Lemma 2 we have
![V_\alpha\cap HOD=\{x \mid x\in V_\alpha\wedge x\in HOD\}\in OD](/latex?n=b1c7b05cfbfbe537731895b60e503a5ce3d8101f750952e73c74a582a3ffb892)
. Trivially, we also have
![V_\alpha\cap HOD\subseteq HOD](/latex?n=05f3a8d4dce2fc6dd0c08ffd9bb710b90a26adb2c63da66ac80febd80cc75a51)
, so by Lemma 1,
![V_\alpha\cap HOD\in HOD](/latex?n=184398c3846429f10356cf9d6f71cd83dc637574bc0bf20f9ccc51ae63e249ad)
. Thus, (I2) holds.
For (I3), let
![\phi(x,\vec{z})](/latex?n=93b7a2c78c3f7f2efa034748e757bdb7e84ee1ceca1b61b94b508467c75f2fdc)
be a
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula, choose arbitrary
![\vec{z},u\in HOD](/latex?n=2317c2b4c5953be6528c71d723438d2308fb1c972ab82c2e5d6a75f76ffffd0b)
, and let
![a=\{x\in u \mid \phi(x,\vec{z})\}](/latex?n=f7a0e7116111edb713084b9e82907bd21f530937b52eda39ed0437a95c915fc0)
. Then
![a\subseteq u\subseteq HOD](/latex?n=1d8ba6e8ec88c375c63ad8ceaac5d4449071f10b5ba92445b9d9e89b5bec9b81)
by (I1), so by Lemma 1, it is sufficient to show that
![a\in OD](/latex?n=8f5c740c7ec4a8f4d85aba0d854d55c8e9c60fc645a934069dbee686a3f842b3)
. As
![HOD\subseteq OD](/latex?n=6656434c0bc2f31eb8914723c5557a6ffd6bf59b2799584aacbb05af8cdff314)
we have
![\vec{z},u\in OD](/latex?n=79a3f01836ae43a174d05e2791e2699fe15c05c373031442a7d952983100a061)
, therefore there are
![\vec{\lceil\phi\rceil},\lceil\psi\rceil](/latex?n=abeee9ae390fe0340e2a86f365a2b68372768d530e6bd2f619593e8c349e405b)
and
![\vec{\alpha},\gamma\in On](/latex?n=f929837f0d88c07821cad59846a8a09fa9d5792594d22050f42e44b32b68679c)
and for
![i=1,\ldots,n](/latex?n=7232a3fa3bd45a7c72b9409bb937d82547dee2fd718f55309765486f7527bddc)
there are
![p_i\in \alpha_i^{<\omega}](/latex?n=2f0f4c3d340138f29a9335b26145f9c4d52fbed654a40c6634d832b6319a0abc)
,
![q\in\gamma^{<\omega}](/latex?n=ec5b1692df52eb1bffab50900bb95cd0b376a1d3fb4be8ce51f0735dd78fb937)
sucht hat
![z_i = \{y\in V_{\alpha_i} \mid V_{\alpha_i}\models\phi_i(y,p_i)\}](/latex?n=196f6e5989c244cbe714dac9eb32ddfac2452069cc2b7013ae1de5da02de2928)
and
![u=\{y\in V_\gamma \mid V_\gamma\models\psi(y,q)\}](/latex?n=b569ac8d102a6aa36570bd6c3a6b5fe6fe9c33b7cafec560eb778c4515160a2d)
. Let
![\alpha=\max\{\vec{alpha},\gamma\}](/latex?n=dad2d38f731b9770c6cb12424e00a252df089a1f16252a81d7a46cd5b122d1d7)
, and
![\chi(x,y)=\lceil y=V_x\rceil](/latex?n=7c00a939d15b3cd8ae65c46f9f9e6401f70b857403ed3ff34d7e63a96ee4c0ee)
. By Theorem 1 we get a
![\beta>\alpha](/latex?n=4b4d1aa90b586863d93e555ff73cc8fb543148bfe678c61805bb3f83a308456b)
such that
![V_\beta](/latex?n=0bf9bc170ad957d9c9881e165c651c7e34b65be9ccaa66f9e1cc1abcf463333c)
reflects
![\chi](/latex?n=8d50b5beb7fe1e79d493a28bd7b5833f3403ebe867c4ac17d3967b67cfa06141)
. Therefore
![a=\{x\in V_\beta \mid V_\beta\models \exists_{\vec{w}}\exists_w(\chi(\gamma, w)\wedge](/latex?n=42f8f0e8b9b2e747e92afbdb479afb6a6314a9729336811555ac931703236514)
![(\bigwedge\limits_{i=1}^n\chi(\alpha_i,w_i))\wedge](/latex?n=d6de448e58e38be1695516bc1ee2404a36e396101a8af2cc98c99749aa4f4d48)
![\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))))\}](/latex?n=52d072d6703d0591201f2ccd98955a184073f3c46c20bab0dfc51751a2966f17)
which is in
![OD](/latex?n=d7fcf32ee8e1cd3eef022fead751340276a82cd865ccaabc42af0a680ab8387d)
. Therefore,
![a\in HOD](/latex?n=3f186daeea3dd5154a800d6d994660f4a5edf3e621496e7435589839f501e537)
.
□
Lemma 3: There exists a surjective functor
![F:On\rightarrow OD](/latex?n=14a5e19bcd5db7b00ee0b90dceab457919eadef3709627360d34017b1f497d10)
.
Proof: In Part 2 we proved that there is a bijection
![G:On\rightarrow\omega\times On^{<\omega}](/latex?n=56035782069ae8cdd03a29263917de5eae0deaa7f05c9338e1eff0e0aead8fef)
, so it is sufficient to give a surjective functor
![F:\omega\times On^{<\omega}\rightarrow OD](/latex?n=408f5f62e999ad8afdaedffcb0d332f6ffc807395f3f047146860b729a9339aa)
. Now let
![\left<\phi_n \mid n<\omega\right>](/latex?n=71cc5df90a6f65e22d3bb33e4ebecd47cdf970c1b05c652ed00a639a72ec7927)
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.](/latex?n=b83bf8e40e60c4b75d806dcb44b64e4d60a27cfef83232c65626f129ef2ae6a9)
Then
![F](/latex?n=f67ab10ad4e4c53121b6a5fe4da9c10ddee905b978d3788d2723d7bfacbe28a9)
is surjective.
□
Lemma 4: There exists a surjective functor
Proof: Since
![HOD\subseteq OD](/latex?n=6656434c0bc2f31eb8914723c5557a6ffd6bf59b2799584aacbb05af8cdff314)
, use
![H=F \mid _{HOD}](/latex?n=750a1c6c8f6c5a1beb2561bcea5a5e4e6501dd8dc90a74c46162e43b894df165)
.
□
Theorem: (AC) holds in
Proof: By Lemma 4, we have our surjective
![H:On\rightarrow HOD](/latex?n=9e7e3441e64b4d6450105db755ace4843398c4bb95edadbf8834bee70459dfbe)
. For
![\alpha\in On](/latex?n=813abd682fcf1dde9347cd9108a7e712d6f39d50e09e217222c3940f287ae22d)
, define
![g_\alpha= H \mid _\alpha](/latex?n=72517da88111c26ab2929d08efd89cebb8c1b2fe8bf58cc88dbfb2b1304653a2)
. By Lemma 2 we know that for every
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
,
![g_\alpha\in OD](/latex?n=6697d83721d27271883280098f5057e17371c2b3d52596206786a25bf107f8aa)
, and since
![g_\alpha\subseteq HOD](/latex?n=c36dfd93e8911cc317d72eeac52377938543f3bfbd70c7ba756335f4015c0588)
, we have
![g_\alpha\in HOD](/latex?n=3be2bff297da70087d0fba5c22d93466aaa5cbbd665f3e66f6f006815600dd7d)
. Let
![u\in HOD](/latex?n=ab641e93207bc145cde88f82de873f218990528eb4dbdf46357ee5bcd457b5c3)
be arbitrary but fixed. Then there exists an
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
such that
![u\subseteq \operatorname{ran}(g_\alpha)](/latex?n=6a8137dd99b26833fe2338a020d37d1e657da06534f310b201ec194773164715)
. Now define a well-ordering
![r\subseteq u\times u](/latex?n=b05d57d7bcbb6a85b8f82bd2c394546d8baa541ebac6f0d16d1c0d3972d890c7)
by
![\{\left<x;y\right> \mid \min\{\gamma \mid x=g_\alpha(\gamma)\}<\min\{\gamma \mid y=g_\alpha(\gamma)\}](/latex?n=7106e68800f12592e784c2aeaa1ac9531fc6722d93f0836944ac6812bd981591)
![r](/latex?n=454349e422f05297191ead13e21d3db520e5abef52055e4964b82fb213f593a1)
is a well-ordering, and
![r\in HOD](/latex?n=6937872b72d60ba46ceb664bd906508b0969bbaa7588448ad1191641346f4c7c)
. Thus, in
![HOD](/latex?n=03a965247dd8ae5eceea306659a20d1ac18bbd68dfa0c9d231fa3e9b0f981426)
, the well-ordering theorem holds, therefore, AC holds in
![HOD](/latex?n=03a965247dd8ae5eceea306659a20d1ac18bbd68dfa0c9d231fa3e9b0f981426)
.
□