Proof of The Natural Numbers Are Well Ordered

All properties of the order on $\mathbb{N}$ used below are those listed in Properties of the Order on the Natural Numbers, and $m+1=S(m)$ for the successor map $S$ is claim 1 of Arithmetic of Addition on the Natural Numbers. Call $a\in A$ a least element of $A$ if $a\le m$ for every $m\in A$.

Existence. Suppose, for contradiction, that $A$ has no least element. For $n\in\mathbb{N}$ let $P(n)$ be the assertion: no $m\in A$ satisfies $m\le n$. We prove $P(n)$ for every $n$ by the principle of induction.

Base case. Suppose $m\in A$ and $m\le 1$. By claim 4 of Properties of the Order on the Natural Numbers we also have $1\le m$, so $m=1$ by claim 2. But then $1\in A$, and claim 4 gives $1\le m'$ for every $m'\in A$, so $1$ would be a least element of $A$, contrary to assumption. Hence $P(1)$ holds.

Inductive step. Assume $P(n)$, and suppose $m\in A$ satisfies $m\le n+1$. If $m\ne n+1$, then $m\le n$ by claim 5 of Properties of the Order on the Natural Numbers applied to $n+1=S(n)$, contradicting $P(n)$; hence $m=n+1$, so $n+1\in A$. Now let $m'\in A$ be arbitrary. By trichotomy (claim 3), exactly one of $m'<n+1$, $m'=n+1$, $n+1<m'$ holds. The first is impossible: $m'<n+1$ gives $m'\le n+1$ and $m'\ne n+1$, hence $m'\le n$ by claim 5, contradicting $P(n)$. In the remaining two cases $m'=n+1$ or $n+1<m'$, and each gives $n+1\le m'$ by claim 1. Thus $n+1$ would be a least element of $A$, contrary to assumption. Therefore no $m\in A$ satisfies $m\le n+1$, that is, $P(n+1)$ holds.

By induction, $P(n)$ holds for every $n\in\mathbb{N}$. If now $m\in A$, then $m\le m$ by claim 1, contradicting $P(m)$. Hence $A$ is empty, contrary to the hypothesis that $A$ is nonempty. This contradiction shows that $A$ has a least element.

Uniqueness. If $a$ and $a'$ are both least elements of $A$, then $a\le a'$ and $a'\le a$, so $a=a'$ by claim 2 of Properties of the Order on the Natural Numbers. Hence the notation $\min A$ is unambiguous.