I'm not sure whether my proof contains any error. Please help me check it out.
Let $\mathbb N$ is the set of natural numbers by Von Neumann construction (https://www.wikiwand.com/en/Natural_number#/Formal_definitions).
Theorem: For all $n,m\in\mathbb N$, we define order relation $<$ as follows $$n\lt m\iff n\subsetneq m$$, then $\forall n,m\in\mathbb N$, either $n<m, m<n$, or $m=n$.
Lemma 0: $\forall k,n \in\mathbb N:k\in n\implies k\subsetneq n$.
I presented one proof for this lemma in $\forall k,n \in\mathbb N:k\in n\iff k\subsetneq n$ [Proof Verification and Suggestion for shorter or simpler proof].
Lemma 1: $\forall k,n\in\mathbb N:k\subsetneq n\implies k+1\subseteq n$.
Let $T=\{n\in\mathbb N\mid \forall k\in\mathbb N:k\subsetneq n\implies k+1\subseteq n\}$. It's clear that $0=\varnothing\in T$ vacuously. Assume $n\in T$. For $k\subsetneq n+1=n\cup\{n\}$, there are two cases in total.
If $n\in k$, then $n\subsetneq k\subsetneq n\cup\{n\}\subseteq k$. Thus $k\subsetneq k$, which is impossible to happen. So this case is not possible.
If $n\notin k$, then $k\subseteq n$. If $k=n$, then $k+1=n+1$, hence $k+1\subseteq n+1$. If $k\subsetneq n$, then $k+1\subseteq n$ [Since $n\in T$], hence $k+1\subseteq n\cup\{n\}=n+1$.
Either way, $\forall k \in\mathbb N:k\subsetneq n+1\implies k+1\subseteq n+1$. Thus $n+1\in T$. By principle of induction, $T=\mathbb N$.
Lemma 2: $\forall k,n\in\mathbb N:k+1\subseteq n\implies k\subsetneq n$.
Let $T=\{n\in\mathbb N\mid \forall k \in\mathbb N:k+1\subseteq n\implies k\subsetneq n\}$. It's clear that $0=\varnothing\in T$ vacuously. Assume $n\in T$. For $k+1\subseteq n+1$, or equivalently $k\cup\{k\}\subseteq n\cup \{n\}$, there are two cases in total.
If $k\in n$, then $k\subsetneq n$ by Lemma 0, hence $k\subsetneq n\subsetneq n\cup\{n\}=n+1$. Thus $k\subsetneq n+1$.
If $k\notin n$, then $k\in\{n\}$, hence $k=n$. Consequently, $k=n\subsetneq n\cup\{n\}=n+1$. Thus $k\subsetneq n+1$.
Either way, $\forall k\in\mathbb N:k+1\subseteq n+1\implies k\subsetneq n+1$. Thus $n+1\in T$. By principle of induction, $T=\mathbb N$.
Lemma 3: $\forall k,n\in\mathbb N:k\subsetneq n\iff k+1\subseteq n$.
This is a combined direct corollary of Lemma 1 and Lemma 2.
Now we use above lemmas to prove the theorem.
Let $T=\{n\in\mathbb N\mid \forall m\in\mathbb N:n<m \text{ or } m<n \text{ or } m=n\}$. It's clear that $0\in T$. Assume that $n\in T$. For any $m\in\mathbb N$, there are 3 cases in total.
-
$n<m\iff n \subsetneq m\implies n+1\subseteq m$ by Lemma 3 $\implies n+1\subsetneq m$ or $n+1=m$ $\implies n+1<m$ or $n+1=m$.
-
$n=m\implies m=n\subsetneq n\cup\{n\}=n+1\implies m<n+1$.
-
$m<n\implies m\subsetneq n\subsetneq n\cup\{n\}\implies m\subsetneq n\cup\{n\}=n+1\implies m\subsetneq n+1\implies m<n+1$.
Thus $n+1\in T$. By principle of induction, $T=\mathbb N$. $\Box$
Best Answer
I have a few notes about lemma 2
First you didn't use the induction step, so there is no need to create $T$, it is direct proof.
Second it is a lot easier to use the definition of subset: $$k\cup\{k\}\subseteq n\overset{def}\iff \forall x(x\in k\cup\{k\}\implies x\in n)$$ and $$k\in k\cup\{k\}\implies k\in n\overset{Lemma~0}\iff k\subsetneq n$$So there is no second case
Apart from this it is great!(It Appear to be that your questions are the only featured questions that I can/have patience to answer!)