Existence of $\{\omega, \omega+1,...\}$ via the axiom of replacement I want to prove the existence of $\{\omega, \omega+1,\cdots\}$ using axiom of replacement by defining a function $f:\omega \mapsto \omega+\omega$ with $f(n)=\omega+n$. But the class function needs to be definable by some formula. I am not very sure of how to write that formula explicitly (within ZFC).
Thanks in advance!
 A: This sort of thing is in general the function of the recursion theorem. Here's how it works in this specific case:
We have a recursively defined "function" $F$, which we want to show can actually be expressed by a formula (and hence, by replacement, by a bona fide function). $F$ needs to be defined on $\omega$ and to satisfy


*

*$F(0)=\omega$

*$F(s(n))=s(F(n))$


where $s$ is the successor function.
Say that a function $f$ is an attempt at defining $F$ if its domain is an initial segment of $\omega$, and it satisfies the above equations whenever they make sense. All this can be easily expressed as a formula:
$$(f \text{ is a function}) \land (\exists n \in \omega (\mathrm{dom}(f)=n))\land (0 \in \mathrm{dom}(f) \to f(0)=\omega) \land (\forall n \in \omega (s(n)\in \mathrm{dom}(f) \to f(s(n))=s(f(n))))$$
It's easy to prove by induction that for any $n$, there's an attempt defined at $n$, and that any two attempts agree on the intersections of their domains. We can thus define $F$ by declaring $F(a)=b$ to mean "there exists an attempt $f$ defined at $a$ with $f(a)=b$".
