Proof that the minimal inductive set does not contain any more elements than $\{\emptyset, s(\emptyset), s(s(\emptyset)),s(s(s(\emptyset))),...\}$? I am studying axiomatic (ZF) set theory and in particular the construction of the natural numbers from axiomatic set theory. Let me start by giving some introduction to my question. 
The axiom of infinity says that there exists at least one inductive set. An inductive set is defined to be a set $I$ for which $\emptyset\in I$ and $(a\in I \Rightarrow s(a)\in I)$, where $s(a) = a\cup\{a\}$. One can then prove that there also exists a minimal inductive set $S$ such that $S\subseteq I$ for all inductive sets $I$ and that $S = \cap\{A\subseteq I : \text{A is a inductive set}\}$. This definition does not depend on the choice of $I$. The set $S$ then is claimed to satisfy the Paeno axioms, by which it can act as a model for the natural numbers. I'd like to prove this, and my question is about one of the first steps of this proof, I think.
What I am trying to prove is that $S = E$, where $E = \{\emptyset, s(\emptyset), s(s(\emptyset)),s(s(s(\emptyset))),...\}$. I think it's clear that, if $E$ exists, $E$ is the minimal inductive set. But I am not sure how to prove that $E$ exists. I do have an idea, but I am wondering if it is valid. It goes simply like this.
We can describe $E$ as $E=\{x\in S : x\in \{\emptyset, s(\emptyset), s(s(\emptyset)),s(s(s(\emptyset))),...\}$. Then, by the separation axiom, E exists.
My main question is basically: does this work? Is this (part of the) proof valid? The reason that I doubt this is because the condition $x\in \{\emptyset, s(\emptyset), s(s(\emptyset)),s(s(s(\emptyset))),...\}$ might not be a valid condition that can be used together with the separation axiom. A difficulty is for example that it is not always clear if a given set $B$ is an element of $E$, as we need to check if $B$ is any of the elements in $E$, of which there are infinite.
Another question, closely related to the former, is whether or not the separation axiom implies that all 'subcollections' of a given set are in fact themselves sets. If this is true, then indeed this guarantees that $E$ exists.
EDIT:
I think I found an anwser to my first question. We can prove that the minimal inductive set is $E = \{\emptyset, s(\emptyset), s(s(\emptyset)),s(s(s(\emptyset))),...\}$ by using the separation axiom. We just need to describe  $E$ in terms of first order logical propositions. We can do this as follows. 
$E = \{n \in S : (\neg \exists m(m\in S \wedge(s(m)=n)))\rightarrow n=\emptyset  \}$. Basically, it says that each element $n$ of $E$ either has a 'predecessor' $m$ (such that $s(m)=n$) or is the empty set. This makes sure the empty set is the only 'starting point' and thus all other elements are  related to the empty set by repeated succession. This is correct ZF language, I believe, so this should do the trick. By the separation axiom $E$ exists. And since $C$ is itself an inductive set, and is contained in the minimal inductive set, it should itself be the minimal inductive set.
If anyone agrees or disagrees, I would love to hear it!
 A: To have any hope of proving, in axiomatic set theory, that $S=\{\emptyset,s(\emptyset),s(s(\emptyset)),\dots\}$, you'd first have to express $\{\emptyset,s(\emptyset),s(s(\emptyset)),\dots\}$ in the language of axiomatic set theory.  The difficulty here is the ellipsis "$\dots$". I don't see any way to define that without a prior notion of "natural number" or "finite" or some such concept.  I think you'll be much better off of you try to prove directly from the definition of $S$ that it satisfies the Peano axioms.
You're right that the separation axioms won't give you $E$, at least not until you handle the issue of expressing $E$ in the language of axiomatic set theory.  The separation axioms apply only to formulas in that language.  In particular, they do not say that all "subcollections" of a given set are again sets.
A: The basic problem with your plan is that your $E$ does not necessarily constitute a set in a model of ZF. Sure, it will exist (and then equal $S$) in the intended interpretation of set theory, consisting of some Platonic universe of sets. But if ZF is consistent at all, it will also have "non-standard" models where the elements of the form $0, s(0), s(s(0))$ do not form a set.
Since what you're trying to prove is not true in all models, you wouldn't be able to prove it from the axioms even if you had a way to express it (which, as Andreas explains, you don't).
The problem is not specific to ZF in particular, but is endemic to all first-order theories that aim to allow reasoning about the integers. In a first-order theory you can always use compactness to get a model where there is an element that behaves like an integer (in the sense that it has every expressible property that all the integers have, such as being an element of $S$) yet does not equal any $s(s(\cdots s(0)\cdots))$.
Your edit doesn't work to define $E$ because in a non-standard model where $S$ contains additional elements, all of those additional elements will have predecessors too. Such an additional element will have an infinitely descending chain of predecessors, so the model is not well-founded. But that does not contradict the Axiom of Regularity because the elements of that infinitely descending chain will not constitute a set either.

(The compactness argument goes like this: Add a new constant letter $c$ to the language of the theory. Add new axioms $c\ne s(s(\cdots s(0)\cdots))$ for every number of $s$. And finally, for every property that $\phi$ that all integers of your favorite model have, add the axiom $\phi(c)$. The extended theory is consistent because every finite subset of it is -- a finite subset only contains finitely many of the $c\ne s(\cdots)$ axioms, so there's always some standard integer that can play the role of $c$. But since the extended theory is consistent, it has a model, and in that model $c$ cannot equal any of the standard integers.)
A: I think $E$ cannot be a set in ZF, as long as $E\ne S$. That is, one cannot construct a model for ZF in which $E$ is a proper subset of $S$: If $E\subsetneq S$ were a set, then there would be a least element $x$ in the nonempty set $S\setminus E$, since $S$ is well ordered with respect to $<$ (i.e., $\in$). By $\emptyset\in E$, we know $x\ne\emptyset$, implying a predecessor $y\in S$ with $s(y)=x$. Since $x$ is a least element of $S\setminus E$, we have $y\in E$.
It follows from the definition of $E$ that $x=s(y)\in E$, contradicting $x\in S\setminus E$.
