Replacement failure at V omega plus omega (source code)

= Replacement failure at V omega plus omega
{title2=$V_{\omega+\omega}\not\models\mathrm{Replacement}$}

The transitive rank stage $V_{\omega+\omega}$ contains $\omega$ and every <ordinal> $\omega+n$. The relation mapping a finite <ordinal> $n$ to the $n$th successor of $\omega$ is internally definable using finite successor chains, whose finite coding overhead remains below this limit rank. Its image would have rank $\sup_n(\omega+n+1)=\omega+\omega$, so it is not an element of the stage. This is a failure to collect existing values, rather than a missing individual value.