Equivalence of two formulations of the axiom of infinity I'm introducing Zermelo–Fraenkel axioms in a minimal way: only what is actually needed to introduce real numbers.
In this respect I noticed that I do not need the axiom of foundation nor the axiom of replacement. Instead I define functions as soon as possible, so it is natural to define an infinite set as a set $X$ such that there exists $f\colon X\to X$ injective, but not surjective (Dedekind-infinite) before having natural numbers.
So my statement of the axiom of infinity is: "there exists a (Dedekind-)infinite set". The usual axiom of infinity requires instead the existence of the first infinite ordinal $\omega$. If I have $\omega$ it is not difficult to prove that $\omega$ is Dedekind-infinite.
On the other hand it seems to me that without the replacement axiom it is possible that an infinite set exists even if $\omega$ does not exist. This makes sense to me: why should I suppose the existence of $\omega$ if I don't really need it?
However, this answer states that the equivalence of the two formulations can be obtained only with extensionality, pairs, unions, specification and powers. How can this be achieved?
 A: This is not true.  Consider the set $X=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\dots\}$.  Let $M$ be the closure of $X\cup\{X\}$ under the operations of taking subsets, forming pairs, forming power sets, and taking unions.  Then $M$ will be a transitive model of the Extensionality, Pairing, Union, Specification, and Powerset axioms (and also Regularity and Choice), as well as your version of Infinity since there is a non-surjective injection $f:X\to X$ given by $f(x)=\{x\}$.  However, I claim that $\omega\not\in M$.  To prove this, just note that for every $x\in M$, the transitive closure of $x$ contains only finitely many elements of $\omega$ (since this is true of $X\cup\{X\}$ and is preserved by all the operations we close it under to form $M$).
A: This may be an alternative approach:
Let $X=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\ldots\}$.
Define recursively
$$ f(x)=\begin{cases}\emptyset&\text{if }x\in X\setminus\{\emptyset,\{\emptyset\}\}\\\{\,f(y)\mid y\in x\,\}&\text{otherwise}\end{cases}$$
and let $M$ be the class of sets  $x$ such that $f(x)$ is hereditarily finite.
Then $M$ is closed under Pairing, taking subsets (hence under Specification), Union, and Powerset. Clearly $X\in M$ and $\omega\notin M$ and we have the injective non-surjective map $s\colon X\to X$, $x\mapsto \{x\}$.
Incidentally, (using Kuratowksy pairs) its graph $\{\,\langle x,s(x)\rangle \mid x\in X\,\}$ is also $\in M$ because for almost all $x\in X$, we have
$$ f(\langle x,s(x)\rangle)=f(\{\{x\},\{x,s(x)\}\})=\{f(\{x\}),f(\{x,s(x)\})\}
=\{\emptyset,\{f(x),f(s(x))\}\}
=\{\emptyset,\{\emptyset,\emptyset\}\}=\{\emptyset,\{\emptyset\}\}$$
