Solution (source code)

= Solution

In first-order <set> theory a <class in set theory> is a definable collection, written schematically $\{x:\theta(x,\vec p)\}$ using a <logical formula> and <set> parameters. A <class term> is an abbreviation for such a defining condition; it does not add a new kind of object to the <quantifiers> of <ZF>. A <class in set theory> is proper if it is not the collection of elements of any <set>.

Define the <cumulative hierarchy> by <transfinite recursion>:
$$
V_0=\varnothing,\qquad V_{\alpha+1}=\mathcal P(V_\alpha),\qquad
V_\lambda=\bigcup_{\alpha<\lambda}V_\alpha\quad(\lambda\text{ a nonzero limit ordinal}),
$$
and let $V=\{x:\exists\alpha\text{ ordinal }(x\in V_\alpha)\}$. Without <foundation> this denotes the well-founded part produced by the hierarchy; it must not simply be assumed to contain every ambient <set>. <Transfinite recursion> on <ordinals> and the relevant <set> constructions remain available in <ZF without foundation>.

Prove transitivity by <transfinite induction>. The empty stage is transitive. Suppose $T=V_\alpha$ is transitive. Then each member of $T$ is a <subset> of $T$, so $T\subseteq\mathcal P(T)$. Also $\mathcal P(T)$ is transitive: if $u\in v\in\mathcal P(T)$, then $u\in T$ and, by transitivity of $T$, $u\subseteq T$, so $u\in\mathcal P(T)$. At a limit stage, a <union> of <transitive sets> is transitive. This proves transitivity at every stage.

Finally transitivity of $V_\alpha$ itself implies that every member is a <subset> of $V_\alpha$, giving
$$
\boxed{V_\alpha\subseteq\mathcal P(V_\alpha)=V_{\alpha+1}.}
$$
These successive inclusions and the limit definition also imply $V_\alpha\subseteq V_\beta$ whenever $\alpha\le\beta$. The argument has not used <foundation>. This leaf includes the unnumbered definitions preceding the source's three claims.