Hereditary size exhausts V under Choice

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)

Assume the Axiom of Choice (def-axiom-of-choice). Then every set $X$ can be well ordered: there is a relation on $X$ making it a well-ordered set (def-well-order). The Axiom of Choice is used only inside thm-zorn, and nowhere else in the argument below. (The well-ordering theorem)

For every set $A$ there is an ordinal (def-ordinal) that does not inject into $A$, that is, admits no injective function into $A$. The least such ordinal is the Hartogs number $\mathrm{\aleph }(A)$, and it is exactly $\mathrm{\aleph }(A)=\{\mathrm{o}\mathrm{t}(S,R):S\subseteq A\text{ and }R\text{ well-orders }S\},$ the set of order types (thm-mostowski-collapse) of the well-ordered subsets of $A$. The proof is choice free. That is the whole point of the theorem: in ZF alone, with no assumption that $A$ can be well ordered, one still gets an ordinal too long to be laid inside $A$. (Hartogs: an ordinal that does not inject into a given set)