I am trying to write a formula in the language of ZF that checks for von Neumann naturals. This is how far I got:
The predicate "Ind(a)" is true, if and only if $a$ is inductive.
$$Ind(a) \leftrightarrow \varnothing \in a \; \land \forall b \, (b \in a \rightarrow b \; \cup \; \lbrace b \rbrace \in a) $$
Is the following predicate true, if and only if $a$ is a von Neumann natural?
$$Neu(a) \leftrightarrow \forall i \, (Ind(i) \rightarrow a \in i)$$
My thinking is the following: All inductive sets contain by definition all von Neumann naturals. Therefore the predicate $Neu(a)$ is true if $a$ is a von Neumann natural. The axiom of infinity asserts the existence of an inductive set, which I will call $I$. The power set of $I$ contains (among others) inductive sets. One of these sets contains exactly the von Neumann naturals(for any inductive set with non-von Neumann members, there is another set in $P(I)$ which does not contain those). If $a$ is not a von Neumann natural, then $a$ is not member of the set I just mentioned, and therefore the predicate $Neu(a)$ will be false.
Does this make any sense?