How to prove that Von Neumann's set of natural numbers only contains 0 and it's successors? I have been delving into ZFC set theory on my own for some time, and I am now learning about the possible definitions of $\mathbb N$ in this theory.
I am lead to believe (and inclined to agree) that Von Neumann's definition is attractive in many regards. It states that $\mathbb N$ is the "intersection of all inductive sets", where an inductive set is one whose existence is postulated by the axiom of infinity.
I quickly managed to convince myself that this is indeed a set permited by ZFC.
Indeed, the axiom of infinity declares the existance of at least one inductive set that we can call $I$.
One can then show that the following set
$$
\lbrace x\in I\ |\ \forall J\ [j\in J\Rightarrow\mathcal{S}(j)\in J])\Rightarrow x\in J\rbrace
$$
which is permited by the axioms of ZFC, contains exactly the elements which are members of all inductive sets. It is therefore the set defined by Von Neumann.
I am also aware that if one defines each natural number individually in an inductive fashion, like so:

*

*$0=\emptyset$

*$\forall n\quad n+1 = S(n) = n\cup\lbrace n\rbrace = \lbrace 0,1,\cdots,n\rbrace$
then all of these sets are in $\mathbb N$ since, by Von Neumann's definition, one can show that $\mathbb N$ is inductive.
Here is my question: How does one prove that the converse is true ? i.e. that $\mathbb N$ only contains $0$ and its successors.

My research so far: I have searched the math stack exchange for an answer.

*

*The accepted answer of
this
question says that

The fact that we take the smallest possible inductive set is what corresponds to the idea that the set only contains zero and its
successors, i.e. the only things that we need to be there in order
to have an inductive set.

While it helps me get an intuition of why it would be true, I'm not
quite satisfied and would like to have a proof.


*Again, the answer to this question says that

The set ($\mathbb N$) contains exactly $\emptyset$ and its successors

but does not explain why.


*In the comments of
this
other question, someone sugests to first prove that $\lbrace
n\in\mathbb N\mid n\subseteq\mathbb N\rbrace$ is inductive, which
implies that $\lbrace n\in\mathbb N\mid n\subseteq\mathbb N\rbrace = \mathbb N$, i.e.
every natural number is itself a set of natural numbers.
I have done so, and I feel like it got me closer to what I'm looking for, but from there I still
don't know how to show that any element of $\mathbb N$ is some successor of $0$.

Update:
From studying the problem further I managed to prove (hopefully without errors) a few results. For the sake of brevity I've omitted the proofs, and I write $\mathbb N^*$ for $\forall x\in\mathbb N\setminus\lbrace 0\rbrace$.


*$\forall x\forall y\ S(x)=S(y)\Rightarrow x=y$
Given a set $x$, the set $\lbrace k\in\mathbb N|S(k)=x\rbrace$ is a set
allowed under the axioms of ZFC.
Let then $P(x)=\cup\lbrace k\in\mathbb N|S(k)=x\rbrace$.
If there is no $k\in\mathbb N$ whose successor is $x$, then $P(x)=\emptyset$ ; if
there is such a $k$, then according to 0. it's the only one and thus, $P(x)=k$
and $S(P(x))=x$.

*

*$\forall x\quad P(x)\in\mathbb N$

*$\forall n\in\mathbb N \quad \neg(\exists k\in\mathbb N\ S(k)=n)
\Rightarrow n=0$

*$\forall x\in\mathbb N^* \quad S(P(x))=x$
and
$\forall y\in\mathbb N\quad P(S(x))=x$

*$\forall m\in\mathbb N^* \quad \forall n\in\mathbb N\quad
(m=S(n)\Leftrightarrow P(m)=n)$
But still cannot find a way to prove that $\mathbb N$ is exactly "$0$ and its
successors".
I've tried to define things like "Given a set $a$:

*

*$S_\emptyset(a)=a$

*$S_x(a)=S(S_{P(x)}(a))$ where $x$ is a set."

and then go from there. But here for instance, to say that $S_x(a)$ is a valid set, one must justify that $S(S_{P(x)}(a))$ is one too, and so justify that
$S(S(S_{P(P(x))}(a)))$ is one too, and so forth... which I don't think is doable.
"$S_{S(x)}(a)=S(S_x(a))$" has the same issue.
I wanted to show that $\lbrace v\in\mathbb N|\exists n\in\mathbb N\quad
v=S_n(0)\rbrace=\mathbb N$
 A: Okay ! After some time and a lot of efforts, I managed to find an answer that I find satisfying.
The big problem I had was that I had no way yet to rigorously write a formula that said "$n$ is a successor of $m$" for any natural numbers $n$ and $m$.
I tried to recursively define what it meant to be the "$n$-th successor of $0$" (where we define $0$ to be $\emptyset$), and I was on the right track, but I ran into trouble because I hadn't proven beforehand that I was allowed to define things recursively.
To prove that, there are a quite a few steps I had to take so, for the sake of brevity, I will only provide an outline of the proofs ; if anyone sees this with the same question I had and wants the details, just ask.

*

*The Theorem of Induction states that
$$
\forall A\ (0\in A\ \wedge\ \forall k\in\Bbb N\ (k\in A\Rightarrow\mathcal S(k)\in A))\Rightarrow\Bbb N\subseteq A
$$
It can be proven by showing that $A\cap\Bbb N$ is inductive so
$\Bbb N\subseteq A\cap\Bbb N$ and, since $A\cap\Bbb N\subseteq A$, we conclude that
$\Bbb N\subseteq A$.


*To make my life simpler, I then proved that, given a property $P$
$$
[P(0)\,\wedge\,(\,\forall x\ P(x)\Rightarrow P(\mathcal S(n))\,)]\Rightarrow\forall n\in\Bbb N\quad P(n)
$$
It follows directly from 1. Just let $A=\{n\in\Bbb N\mid P(n)\}$ and apply 1. to it.


*From there we prove this bad boy, the Recursion Theorem, which says that
$$
\forall X\quad X\neq\emptyset\Rightarrow[\ \forall a\in X\ \forall f:X\rightarrow X\ \exists!F:\Bbb N\rightarrow X\quad \underbrace {F(0)=a\ \wedge\ \forall n\in\Bbb N\enspace F(\mathcal S(n))=f(F(n))}_{\text {(a)}}\ ]
$$
i.e. For all non-empty $X$, $a\in X$ and $f:X\rightarrow X$, there is a unique function $F:\Bbb N\rightarrow X$ such that $\text {(a)}$.
The proof is a long and tedious one which relies on proving that a specific subset of $\Bbb N$ is inductive and, therefore, equal to $\Bbb N$. It gets messy real quick and I got lost multiple time doing it, so I'll redirect you to this book (Naive Set theory, by Paul R. Halmos) on pages 48-49, which is where I got it from.


*Finally, armed with 3. we can safely define things recursively.
We apply the recursion theorem with $X=\Bbb N$, an $a\in X$ whose value we don't specify, and $f=\mathcal S$ the successor function. There exists a unique function that satisfies $\text {(a)}$ and, since it depends on $a$ what that function is, lets call it $F_a$. (It also depends on $X$ and $f$, but we fixed their values. Only $a$ is unspecified.) $F_a$ is defined on all of $\Bbb N$.
Let's rewrite the property $\text {(a)}$:
$$
F_a(0)=a\ \wedge\ \forall n\in\Bbb N\enspace F_a(\mathcal S(n))=\mathcal S(F_a(n))
$$
I hope that you'll agree that, for any $n\in\Bbb N$, $F_a(n)$ is the result of applying $\mathcal S$ to $a$ $n$ times over, i.e. the "$n$-th successor of $a$".


*Let's now, at last, prove by induction that
$$
\forall n\in\Bbb N\quad F_0(n)=n
$$
i.e. Any natural number $n$ is, in fact, the $n$-th successor of $0$.
Base case: $F_0(0)=0$
Induction step: For a given $n\in\Bbb N$, suppose that $F_0(n)=n$.
$$
F_0(\mathcal S(n))=\mathcal S(F_0(n))\\
\phantom {F_0(\mathcal S(n))}=\mathcal S(n)\phantom {F_0()}
$$
We then conclude that $\Bbb N=\{F_0(n)\mid n\in\Bbb N\}$, i.e. that $\Bbb N$ is the set of $0$ and its successors. And finally, it is done. Sure hope I didn't mess up !

Afterthought: This whole demonstration makes copious use of $\Bbb N$'s definition, it's properties, and results that are deduced from its existence. Therefore, for it to hold, one must first define $\Bbb N$ as the smalest inductive set, and then show that it's the set of $0$ and its successors.
I don't see any way that one could go the other way around, as in how $\Bbb N$ could be defined, from the get-go, to be the set of $0$ and its successors.
