I am working on the ZFC construction of $\mathbb{N}$ :
Axiom of infinity :
there exists a set E such that $\varnothing \in \text{E} \,\wedge \forall s \in \text{E}, s\cup \{s\} \in \text{E}. $ E is said inductive
Let's note $$\mathbb{N}=\bigcap_{x \in \mathcal{P}(\text{E})} \{x | x \text{ is inductive}\}$$
and $$s^+=s\cup\{s\},0=\varnothing$$
Then, it is easy to prove that $\mathbb{N}$ is inductive and the smallest inductive set (for the inclusion relation) ie
$\mathbb{N}$ is inductive and $\mathbb{N} \subset {\text{E}}$
From there, induction follows.
I now want to prove the following :
$\subset$ is a well-order relation on $\mathbb{N}$
I have proven that $ \forall n \in \mathbb{N}, 0\subset n $ and $n\subset n^+$
I will shortly write the proof of each of these propositions
but I am stuck now, my goal is to prove that $n=0 \vee \exists m, n=m^+$
Thanks for the help
T.D
Go directly for your goal: Let $$N=\{\,x\in\Bbb N\mid x=0\lor \exists m\in \Bbb N, x=m^+\,\}. $$ Then $N$ is inductive. Indeed, clearly $0\in N$. Assume $n\in N$. We want to show that $n^+\in N$. But that is immediate from $n^+=m^+$ with $m:=n$. As $N$ is an inductive subset of $E$, it is a superset of $\Bbb N$, but is also a subset of $\Bbb N$, hence $N=\Bbb N$.