$\omega$ is a set

I'm trying to show from the $ZFC$ axioms that $\omega$ is a set and I have something that I think could be a proof but I'm not sure about one of its parts. In particular, I want to use the axiom that says the range of a definable function is a set. But I think definable means that the function can be expressed as a formula in $L_S$ and I can't see how to do that. Here's what I have:

The axiom of Infinity is the following: $$\exists x ( x \neq \varnothing \land \forall y ( y\in x \rightarrow y \cup \{y\} \in x))$$

By Infinity there is an infinite set, $U$. Pick any $u$ in $U$. Now define a function $f$ that maps $u$ to $\varnothing$ (which exists by Empty Set). Map the successors as follows: $s(u) \mapsto s(\varnothing)$ and so on.

This "and so on" is the part that I'm not sure about: I think I have to write $f$ in a first order formula in $L_S$. Since I didn't manage, alternatively, I was wondering if the following (less satisfactory) argument would do: Use that Choice is equivalent to the principle of recursive construction and define $f(s(u)) = s (f(u))$.

To finish apply Replacement to obtain that the range $\omega$ of $f$ is a set.

Many thanks for your help.

-
You should state your version of Infinity. If it states "There exists an inductive set" (a set containing $\emptyset$ and closed under successor), then $\omega$ is simply the smallest inductive set, the intersection of all inductive sets. – Miha Habič Jan 3 '13 at 8:04
@MihaHabič But $\omega$ needs to contain $\varnothing$. If $U$ is an infinite set then it might not contain $\varnothing$. What happens if all the infinite sets don't contain $\varnothing$? – Rudy the Reindeer Jan 3 '13 at 8:12
$$\varnothing \in U\cup \{ \varnothing \} = \bigcup\{U, \{ \varnothing \} \}$$ – Hurkyl Jan 3 '13 at 8:20
I'm sorry, I didn't realize that your version of Infinity doesn't stipulate $\emptyset\in x$. If you're ok with using Choice, why not just take the initial ordinal of your infinite set? Alternatively, for each finite subset of your infinite set, there is a unique natural number in bijection with it. Apply Replacement to the set of finite subsets and go from there. – Miha Habič Jan 3 '13 at 8:28
You're dealing with finite subsets of the infinite set, not elements. You will have to prove that the infinite set has finite subsets of any size, but this shouldn't be difficult. – Miha Habič Jan 3 '13 at 22:27

Usually the axiom of infinity is usually stated:

$(\exists x)(\emptyset \in X \wedge (\forall y \in x)(y \cup \{y\} \in x))$

see Kunen's $\textit{Set Theory}$ (2011) or Jech's $\textit{Set Theory}$.

Any set $x$ which has the above property is called an inductive set. Then $\omega$ is defined to be the intersection of all inductive sets. Notice that in this form of the axiom of infinity and the definition of an inductive set $\emptyset \in X$.

You can also show that if you define the natural numbers as the von neumann ordinals, the axiom of infinity is equivalent to the existence of the set of all natural numbers which is equivalent to the existence of any limit ordinal.

Now to show your form of infinity is equivalent to form above.

It is clear that the form above implies your form. Now to show that your form implies the form above. Let $x$ be such a set given by your form of the axiom of infinity. $x$ has a relation $\in$ on it. $\in$ is set like, well-founded (by the axiom of foundation), and extensional (by the axiom of extensionality). Then $mos$, the Mostowski collapsing function, is an $\in$ preserving bijection with the transitive set $mos(x)$. $\emptyset \in mos(x)$. Since $x$ has the property that for all $y \in x$, $y \cup \{y\} \in x$ and the fact that $mos$ is a $\in$-preserving bijection, $mos(x)$ has the property that whenever $y \in mos(x)$, $y \cup \{y\} \in mos(x)$. Hence I have shown there is an inductive set containing $\emptyset$ (which you were worried about existed in the comments). Hence you have my form of the axiom of infinity. Now you can defined $\omega$ to be the intersection of all inductive sets containing $\emptyset$.

-