Proving $n\not\in n$ for $n\in\mathbb N$ without regularity Is there a way to prove in ZF theory without regularity axiom $\forall n\in\mathbb N$, $n\not\in n$? At this point, I haven't proved yet that $\mathbb N$ is a well-ordered set, so a proof of the well-order shall not use $\forall n\in\mathbb N, n\not\in n$.
I tried induction, but I struggle with the recursive step as I only found that $n\not\in n\Leftrightarrow n\neq n^+$.
 A: First you can prove that the relation $\in$ is transitive on $\mathbb{N}$.  That is, if $x,y,z\in\mathbb{N}$ satisfy $x\in y$ and $y\in z$, then $x\in z$.  The proof of this is quite straightforward by induction on $z$.  (For the induction step, if $x\in y$ and $y\in z^+$ then either $y\in z$ so $x\in z\subseteq z^+$ by the induction hypothesis or $y=z$ so $x\in z\subseteq z^+$.)
Now let us prove that $n\not\in n$ for all $n\in\mathbb{N}$ by induction.  The base case $n=\emptyset$ is trivial.  In the induction step, suppose we know $n\not\in n$ and we wish to show $n^+\not\in n^+$.  Well, if $n^+\in n^+=n\cup\{n\}$ then either $n^+\in n$ or $n^+=n$.  In the first case, we have both $n\in n^+$ and $n^+\in n$ so by transitivity $n\in n$, contradicting the induction hypothesis.  In the second case, we have $n\in n^+= n$, again contradicting the induction hypothesis.
A: We will demonstrate that $\in$ is well-founded on $\mathbb{N}$.
Suppose we have some $W$. Suppose that for all $k \in \mathbb{N}$, if (for all $j \in \mathbb{N}$, if $j \in k$ then $j \in W$), then $k \in W$. I claim that $\mathbb{N} \subseteq W$.
To prove this, we will show that for all $n \in \mathbb{N}$, $n \subseteq W$. We do this by induction on $n$.
In the base case of $n = \emptyset$, the claim that $n \subseteq W$ is immediate.
For the inductive step, suppose that $k \subseteq W$. We wish to show that $k \cup \{k\} \subseteq W$. To do so, it suffices to show that $k \in W$, since we already know that $k \subseteq W$ by the inductive hypothesis. Now consider some arbitrary $j \in \mathbb{N}$ such that $j \in k$. Then $j \in k \subseteq W$, so $j \in W$. Therefore, we see that $k \in W$ as claimed. The induction is complete.
In particular, then, given some $n \in \mathbb{N}$, we have $n \in n \cup \{n\} \subseteq W$, so $n \in W$. This completes the proof that $\in$ is well-founded on $\mathbb{N}$. $\square$
Now suppose that $R$ is well-founded on set $S$. Suppose we had some $s \in S$ such That $s R s$. Then define $S’ = S \setminus \{s\}$.
Now consider some arbitrary $w \in S$. Suppose that for all $w’ \in S$, if $w’ R w$ then $w’ \in S’$. Now suppose $w \in \{s\}$; that is, suppose $w = s$. Then $w \in w$, so in particular, $w \in S’$. But then $w \notin \{s\}$; contradiction. Therefore, $w \notin \{s\}$. Thus, $w \in S’$.
Therefore, by well-foundedness, $s \in S \subseteq S’$. Then $s \in S’$. Contradiction. Therefore, we must in fact have had $\neg (s R s)$. $\square$
Combining these two facts completes the proof.
