Axiom schema of replacement

Every definable function-class maps a set-sized domain to a set-sized range. Functionality means that the defining formula assigns exactly one output to each input in the domain.

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.

For each formula, if every member of a domain set has a witness, a set contains witnesses for all those members. It permits extra members and does not require unique witnesses. For hereditarily countable sets, use ambient axiom of choice to select one internal witness for each member of the countable domain, and use countable-subset closure to keep the resulting witness set internal.

If $V_{\lambda }$, for an infinite cardinal number $\lambda$, satisfies Axiom schema of replacement for every external functional class, then an external cofinal function from an ordinal below $\lambda$ cannot exist: its range would have rank of a set $\lambda$ and would have to belong to $V_{\lambda }$. Similarly, a surjection $\mathcal{P}(\theta )\to \lambda$ with $\theta <\lambda$ is impossible. Infinity therefore makes $\lambda$ an uncountable regular cardinal and a strong limit cardinal. Full semantics for second-order logic, allowing arbitrary external functional relations, is essential.