Proof of The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor

Throughout, every element of a class is a set by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §objects. Membership in a class formed by class abstraction is unfolded by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted; class abstractions are unfolded without further mention. Every class formed below has a formula that quantifies over set variables only, with $0$, $S(u)$ and the ordered pair as defined set symbols (by The Empty Set, the Unordered Pair and the Singleton §empty, The Successor of a Set §successor and The Ordered Pair of Two Sets and Nested Tuples §pair), so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. By The Successor of a Set §successor, for all sets $u$ and $x$,

$$u\in S(x)\quad\text{if and only if}\quad u\in x\ \text{or}\ u=x.\qquad(\mathrm{S})$$

Reading the order. Let $m$ and $n$ be sets. By The Order on Omega §order, $(m,n)\in{\le}$ if and only if there are sets $m',n'$ with $(m,n)=(m',n')$, $m',n'\in\omega$ and $m'\in n'$ or $m'=n'$; by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, $m'=m$ and $n'=n$. Arguing in the same way with The Order on Omega §strict,

$$m\le n\iff m,n\in\omega\ \text{and}\ (m\in n\ \text{or}\ m=n),\qquad m<n\iff m,n\in\omega\ \text{and}\ m\in n.\qquad(\mathrm{O})$$

Every element of $\le$ has the form $(m,n)$ with $m,n\in\omega$, so ${\le}$ is a relation by Relations, Domain, Range, Inverse and Composition §relation, and each element lies in $\omega\times\omega$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. Hence ${\le}\subseteq\omega\times\omega$ by Subclasses and Subsets §subclass, so ${\le}$ is a relation on $\omega$ by Relations, Domain, Range, Inverse and Composition §on. Also, $\omega$ is a set by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §set.

(a) No set is an element of itself. Let $x$ be a set and suppose $x\in x$. By The Empty Set, the Unordered Pair and the Singleton §singleton, the singleton $\{x\}$ has exactly one element, namely $x$. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §foundation, $\{x\}$ has an element $u$ such that no set $s$ satisfies $s\in u$ and $s\in\{x\}$. Then $u=x$, and $s=x$ satisfies $s\in u$ and $s\in\{x\}$, a contradiction. So $x\notin x$.

(b) No two-cycles. Let $m,n\in\omega$ with $m\in n$ and $n\in m$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §element-transitive, applied to $m\in\omega$ with $m\in n$ and $n\in m$, we get $m\in m$, contrary to (a). So $m\in n$ and $n\in m$ never both hold.

(c) Transitivity of membership. Let $k\in\omega$ and let $m,n$ be sets with $m\in n$ and $n\in k$. Then $m\in k$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §element-transitive.

(d) Zero. Let $A=\{n\in\omega:0\in n\vee0=n\}$. Then $0\in A$, because $0\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive and $0=0$. Let $n\in\omega$ with $n\in A$. Then $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, and $0\in n$ or $0=n$, so $0\in S(n)$ by $(\mathrm{S})$; thus $S(n)\in A$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, $\omega\subseteq A$: for every $n\in\omega$, $0\in n$ or $0=n$.

(e) Successors stay below. Let $B=\{n\in\omega:\forall m\,(m\in n\Rightarrow(S(m)\in n\vee S(m)=n))\}$. Since $0\in\omega$ and $0$ has no element by The Empty Set, the Unordered Pair and the Singleton §empty, $0\in B$. Let $n\in\omega$ with $n\in B$; then $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive. Let $m\in S(n)$; by $(\mathrm{S})$, $m\in n$ or $m=n$. If $m\in n$, then $S(m)\in n$ or $S(m)=n$ because $n\in B$, and in either case $S(m)\in S(n)$ by $(\mathrm{S})$. If $m=n$, then $S(m)=S(n)$. Thus $S(n)\in B$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, $\omega\subseteq B$: for every $n\in\omega$ and every set $m\in n$, $S(m)\in n$ or $S(m)=n$.

(f) Comparability. Let $C=\{n\in\omega:\forall m\,(m\in\omega\Rightarrow(m\in n\vee m=n\vee n\in m))\}$. By (d), every $m\in\omega$ satisfies $0\in m$ or $0=m$, so $0\in C$. Let $n\in\omega$ with $n\in C$, and let $m\in\omega$. If $m\in n$ or $m=n$, then $m\in S(n)$ by $(\mathrm{S})$. Otherwise $n\in m$, and (e), applied to $m\in\omega$ and $n\in m$, gives $S(n)\in m$ or $S(n)=m$. In all cases $m\in S(n)$, $m=S(n)$ or $S(n)\in m$, and $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, so $S(n)\in C$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction, $\omega\subseteq C$: for all $m,n\in\omega$, $m\in n$, $m=n$ or $n\in m$.

Well-order. The relation $\le$ on $\omega$ is reflexive, since $u\le u$ for $u\in\omega$ by $(\mathrm{O})$. It is antisymmetric: if $u,v\in\omega$, $u\le v$, $v\le u$ and $u\neq v$, then $u\in v$ and $v\in u$ by $(\mathrm{O})$, contrary to (b). It is transitive: let $u,v,w\in\omega$ with $u\le v$ and $v\le w$; if $u=v$ or $v=w$, then $u\le w$ is one of the hypotheses, and otherwise $u\in v$ and $v\in w$ by $(\mathrm{O})$, so $u\in w$ by (c) and $u\le w$ by $(\mathrm{O})$. Hence $\le$ is a partial order on $\omega$ by Partial and Total Orders on a Set and the Associated Strict Relation §partial. It is total, since for $u,v\in\omega$, (f) gives $u\in v$, $u=v$ or $v\in u$, that is, $u\le v$ or $v\le u$ by $(\mathrm{O})$. Now let $s$ be a subset of $\omega$ with at least one element. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §foundation, $s$ has an element $u$ such that no set lies in both $u$ and $s$. Let $v\in s$. Then $u,v\in\omega$, and $v\notin u$ because $v\in s$; so (f) gives $u=v$ or $u\in v$, that is, $u\le v$ by $(\mathrm{O})$. Hence $u$ is a least element of $s$ by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least, and $\le$ is a well-order on $\omega$ by Well-Orders on a Set §well-order.

Strict. Let ${<_{\le}}$ be the strict relation associated with $\le$, as in Partial and Total Orders on a Set and the Associated Strict Relation §strict. Let $p\in{<}$. By The Order on Omega §strict, $p=(m,n)$ with $m,n\in\omega$ and $m\in n$. Then $m\le n$ by $(\mathrm{O})$, and $m\neq n$, since $m=n$ would give $n\in n$, contrary to (a); so $p\in{<_{\le}}$. Conversely let $p\in{<_{\le}}$; then $p=(u,v)$ with $u\le v$ and $u\neq v$. By $(\mathrm{O})$, $u,v\in\omega$ and $u\in v$ or $u=v$; as $u\neq v$, $u\in v$, so $p\in{<}$ by The Order on Omega §strict. By Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, ${<}={<_{\le}}$. The characterization of $m<n$ then follows from Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization.

Zero-least. For $n\in\omega$, (d) gives $0\in n$ or $0=n$, and $0\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, so $0\le n$ by $(\mathrm{O})$.

Successor. Let $m,n\in\omega$. Then $S(n)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, so by $(\mathrm{O})$, $m<S(n)$ holds if and only if $m\in S(n)$, by $(\mathrm{S})$ if and only if $m\in n$ or $m=n$, and by $(\mathrm{O})$ if and only if $m\le n$. Since $n\le n$ by reflexivity, $n<S(n)$.

Successor-adjacent. Let $n\in\omega$ and suppose $m\in\omega$ satisfies $n<m$ and $m<S(n)$. By $(\mathrm{O})$, $n\in m$ and $m\in S(n)$, so $m\in n$ or $m=n$ by $(\mathrm{S})$. If $m\in n$, this contradicts (b); if $m=n$, then $n\in n$, contrary to (a). So no such $m$ exists.

Successor-below. Let $m,n\in\omega$; then $S(m)\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive. If $m<n$, then $m\in n$ by $(\mathrm{O})$, so $S(m)\in n$ or $S(m)=n$ by (e), that is, $S(m)\le n$ by $(\mathrm{O})$. Conversely let $S(m)\le n$, so $S(m)\in n$ or $S(m)=n$ by $(\mathrm{O})$. Since $m\in S(m)$ by $(\mathrm{S})$, in the first case $m\in n$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §element-transitive, and in the second case $m\in n$ directly. So $m<n$ by $(\mathrm{O})$.

Segment. Let $n\in\omega$ and $T=\{m\in\omega:m<n\}$, formed with the parameters $\omega$, $<$ and $n$. For a set $m$, $m\in T$ if and only if $m\in\omega$ and $m<n$, by $(\mathrm{O})$ if and only if $m\in\omega$ and $m\in n$. If $m\in n$, then $m\in\omega$ by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §omega-transitive. So $m\in T$ if and only if $m\in n$, and $n=T$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality.