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!
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
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$".