Element of Finite Ordinal iff Subset
- $m \in n \iff m \subseteq n$
Let $m \in n$.
Therefore, it follows directly that $m \subseteq n$.
Now let $m \subseteq n$.
We have by hypothesis that $m \ne n$.
From Natural Numbers are Comparable: Proof using Minimal Infinite Successor Set it follows that either $m \in n$ or $n \in m$.
Suppose $n \in m$.
Then $\exists x \in m: m \subseteq x$ which contradicts Finite Ordinal is not Subset of one of its Elements.
The only option left is that $m \in n$.
Hence the result.