H_omega equals V_omega

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

In ZF, for every infinite initial ordinal $\kappa$, $H_{\kappa }$ is a transitive set and $H_{\kappa }\subseteq V_{\kappa }$. For infinite initial ordinals $\kappa \le \mu$, one has $H_{\kappa }\subseteq H_{\mu }$. (H_kappa is a transitive subset of V_kappa)

In ZF without Foundation define the cumulative hierarchy by $V_0=\mathrm{\varnothing },V_{\alpha +1}=\mathcal{P}(V_{\alpha }),V_{\lambda }={\bigcup }_{\beta <\lambda }{V}_{\beta }(\lambda \text{ a nonzero limit ordinal})\mathrm{.}$ For each ordinal $\theta$, use the set well-order recursion schema on $\theta +1$. On histories of domain $0$ return $\mathrm{\varnothing }$; on domain $\beta +1$ return the power set of the last value; on nonzero limit domains return the union of the range. Each is a unique set. Recursions on different ordinal intervals agree on overlaps by the uniqueness clause applied to the smaller interval. Hence the definition of $V_{\alpha }$ as the value at $\alpha$ is uniform and independent of the chosen interval. Power Set is used at successors and Replacement and Union at limits. The notation $⟨V_{\alpha }:\alpha \in \mathrm{Ord}⟩$ denotes a definable class function, not a set sequence. Conventions and prerequisites: thm-transfinite-recursion, lem-ordinal-basics, def-limit-ordinal. (The cumulative hierarchy)