Can Peano's Axioms be derived from ZFC without AOI? From "Axiom of Infinity," Wikipedia:

[T]here is a set I (the set which is postulated to be infinite), such
  that the empty set is in I and such that whenever any x is a member of
  I, the set formed by taking the union of x with its singleton {x} is
  also a member of I.[...]
The infinite set I is a superset of the natural numbers. To show that
  the natural numbers themselves constitute a set, the axiom schema of
  specification can be applied to remove unwanted elements, leaving the
  set N of all natural numbers.

I presume that some version of Peano's Axioms will be derived in this process of extracting the natural numbers.
It has been suggested by a contributor at sci.math (not a crank), that it may be possible to derive Peano's Axioms using ZFC without AOI. Can this be true?

EDIT:
Specifically, without citing AOI, can we prove the existence of a set $N$, function $S: N \to N$ and $0\in N$ such that:
$\forall x,y \in N: [S(x)=S(y) \implies x=y]$
$\forall x\in N: S(x)\ne 0$ 
$\forall P\subset N: [0\in P \land \forall x\in P: [S(x)\in P] \implies P=N]$
 A: EDIT: For the new version of the question, the answer is no: it is a good exercise to show that $V_\omega$, the class of hereditarily finite sets, is a counterexample. Note that while of course there is a class in $V_\omega$ with the desired properties - namely, $\omega$ itself - there is no such set. And this is an important distinction, with the class version of the question having a number of subtleties; see my original answer, which is below the fold.
Incidentally, ZF-AOI is equiconsistent with (first-order) PA. PA proves that PA has no finite model; roughly, this means that models of ZF-AOI which "come from" models of PA (essentially, which satisfy $\neg AOI$ - in particular $V_\omega$ "comes from" $\mathbb{N}$ itself) do not have an inductive set.

As usual with this type of question, the answer depends on exactly what you mean.
Here's a thing that is true:

If $M$ is a model of ZF-AOI, then $FinOrd^M$ - the set (class, as far as $M$'s concerned, but set externally) of $M$-finite ordinals is a model of first-order $PA$ (with $+, \times$ defined as usual in this context).

Now, I suspect you're actually interested in second-order PA, which I'll denote "$PA_2$". But this produces some subtleties. Namely, second-order PA only makes sense in a model of set theory. One might respond instinctively, "Well, look at $M$'s version of $PA_2$!" But there's a problem with that - remember that $FinOrd^M$ is (a priori) a class in $M$, rather than a set! So when we ask "Does $FinOrd^M$ satsisfy $PA_2^M$?", what we really mean is "Does $FinOrd^M$ satisfy the 'class version' of $PA_2^M$?".
That is, I think the right way to ask the question you're getting at is the following:


*

*Let $M\models ZF-AOI$. Then is it necessarily the case that, for all formulas $\varphi(x, \overline{y})$ in the language of set theory and all parameters $\overline{a}\in M$, we have $$M\models \varphi(0, \overline{a})\wedge \forall x\in FinOrd[\varphi(x, \overline{a})\implies \varphi(x+1, \overline{a})]\implies \forall x\in FinOrd(\varphi(x,\overline{a}))?$$


(The point is that the classes of the form "$\{x\in FinOrd^M: M\models\varphi(x,\overline{a})\}$" represent all the sub"sets" of $FinOrd^M$ which $M$ can "see", and so they're the ones it makes sense to query with respect to satisfying the right version of $PA_2$.
The answer to this question is yes, since ZF-AOI proves that the ordinals are well-ordered and that every finite ordinal has a predecessor.
However, there are a couple caveats (for simplicity I assume the $M$'s below satisfy $\neg$AOI):


*

*First, note that while $M$ can express "$FinOrd\models \varphi$" for a specific (first-order in the language of set theory - in particular, no quantifying over classes!) sentence $\varphi$, $M$ can't express "$FinOrd\models\Gamma$" for $\Gamma$ a set of sentences. So in a certain sense, $M$ doesn't know that $FinOrd^M$ is a model of the $M$-class-version of $PA_2$.

*Second, note that if $\varphi$ is a nonstandard first-order sentence in $M$ - that is, a nonstandard finite ordinal in $M$ which $M$ thinks is the Goedel number of a sentence - then $M$ can't express "$FinOrd\models\varphi$"! This isn't really an issue here, but it's worth keeping in mind.

*Finally, it's worth noting that ZF-AOI does not prove the Completeness Theorem - in particular, a model of ZF-AOI may not contain a set model of even first-order PA, even if it thinks that theory is consistent! ($V_\omega$ is an example of this.)
