Solution (source code)

= Solution

We prove the stronger <ordinal> identity
$$
V_\alpha\cap\operatorname{Ord}=\alpha
$$
by <transfinite induction>. It holds at zero. At a successor stage an <ordinal> $\gamma$ belongs to $\mathcal P(V_\beta)$ exactly when every $\delta<\gamma$ belongs to $V_\beta$. By induction this means every $\delta<\gamma$ is less than $\beta$, equivalently $\gamma\leq\beta$. Thus the <ordinals> in $V_{\beta+1}$ are precisely those less than $\beta+1$. At a limit the identity follows by taking unions.

Every $\beta<\alpha$ consequently belongs to $V_\alpha$, so $\alpha\subseteq V_\alpha$ and $\alpha\in\mathcal P(V_\alpha)=V_{\alpha+1}$. But $\alpha\notin V_\alpha$, since an <ordinal> is not less than itself. Hence
$$
\boxed{\alpha\in V_{\alpha+1}\setminus V_\alpha.}
$$
The only well-foundedness used is that of the <ordinal> order, available independently of <Foundation> for arbitrary ambient sets.