Proof of Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity

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; class abstractions are unfolded without further mention. In particular, by The Class Omega of Natural Numbers with Zero §omega, a set $n$ lies in $\omega$ if and only if $n\in y$ for every inductive set $y$. By The Successor of a Set §successor, for all sets $x$ and $u$, $S(x)$ is a set and $u\in S(x)$ if and only if $u\in x$ or $u=x$. By The Class Omega of Natural Numbers with Zero §zero and The Empty Set, the Unordered Pair and the Singleton §empty, $0=\emptyset$ is a set with no element.

Set. By the axiom of infinity Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §infinity, that is Axiom of Infinity, there is a set $x_{0}$ with $\emptyset\in x_{0}$ such that for every $u\in x_{0}$ there is a set $w\in x_{0}$ with $s\in w$ if and only if $s\in u$ or $s=u$, for every set $s$. For such $u$ and $w$, the same condition characterizes $s\in S(u)$, so $w=S(u)$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality, and hence $S(u)\in x_{0}$. Thus $x_{0}$ is inductive by Inductive Classes §inductive. Every $n\in\omega$ therefore satisfies $n\in x_{0}$, so $\omega\subseteq x_{0}$ by Subclasses and Subsets §subclass, and $\omega$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass.

Inductive. Let $y$ be an inductive set. Then $\emptyset\in y$ by Inductive Classes §inductive; as $y$ was arbitrary, $0=\emptyset\in\omega$. Let $n\in\omega$, and let $y$ be an inductive set. Then $n\in y$, so $S(n)\in y$ by Inductive Classes §inductive; as $y$ was arbitrary and $S(n)$ is a set, $S(n)\in\omega$. Hence $\omega$ is inductive by Inductive Classes §inductive.

Least. Let $A$ be an inductive class. By the clause set above and Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass, the intersection $\omega\cap A$ is a set, and by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations a set $u$ lies in $\omega\cap A$ if and only if $u\in\omega$ and $u\in A$. Now $\emptyset\in\omega$ by the clause inductive above and $\emptyset\in A$ by Inductive Classes §inductive, so $\emptyset\in\omega\cap A$. If $u\in\omega\cap A$, then $S(u)\in\omega$ by the clause inductive above and $S(u)\in A$ by Inductive Classes §inductive, so $S(u)\in\omega\cap A$. Thus $\omega\cap A$ is an inductive set by Inductive Classes §inductive, and every $n\in\omega$ satisfies $n\in\omega\cap A$, hence $n\in A$. So $\omega\subseteq A$ by Subclasses and Subsets §subclass.

Induction. Let $A$ be as in the clause induction above, and let $B=\omega\cap A$, the intersection, so that a set $n$ lies in $B$ if and only if $n\in\omega$ and $n\in A$, by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations. Then $0\in\omega$ by the clause inductive above and $0\in A$ by hypothesis, so $0\in B$. If $n\in B$, then $n\in\omega$ and $n\in A$, so $S(n)\in A$ by hypothesis and $S(n)\in\omega$ by the clause inductive above; hence $S(n)\in B$. Thus $B$ is inductive by Inductive Classes §inductive, and $\omega\subseteq B$ by the clause least above. Every $n\in\omega$ therefore lies in $A$, and $\omega\subseteq A$ by Subclasses and Subsets §subclass.

Successor-nonzero. Let $x$ be a set. Then $x\in S(x)$, since $x=x$. If $S(x)=0$, then $x\in0=\emptyset$, which is impossible since $\emptyset$ has no element. Hence $S(x)\neq0$.

Successor-injective. Let $x$ and $y$ be sets with $S(x)=S(y)$, and suppose $x\neq y$. Since $x\in S(x)=S(y)$, we have $x\in y$ or $x=y$, so $x\in y$; symmetrically, $y\in S(y)=S(x)$ gives $y\in x$. By The Empty Set, the Unordered Pair and the Singleton §pair, the unordered pair $\{x,y\}$ is a set whose elements are exactly $x$ and $y$; in particular it has the element $x$. By the axiom of foundation Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §foundation, that is Axiom of Foundation for Classes, it has an element $u$ such that no set $s$ satisfies both $s\in u$ and $s\in\{x,y\}$. Either $u=x$ or $u=y$. If $u=x$, then $s=y$ satisfies $y\in x$ and $y\in\{x,y\}$; if $u=y$, then $s=x$ satisfies $x\in y$ and $x\in\{x,y\}$. Both cases contradict the choice of $u$, so $x=y$.

Cases. Let

$$B=\{n\in\omega:n=0\vee\exists m\,(m\in\omega\wedge n=S(m))\},$$

formed by class abstraction with the parameter $\omega$; its formula quantifies over the set variable $m$ only, $0$ and $S(m)$ being defined set symbols by The Empty Set, the Unordered Pair and the Singleton §empty and The Successor of a Set §successor, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. Since $0\in\omega$ by the clause inductive above and $0=0$, $0\in B$. Let $n\in\omega$. Then $S(n)\in\omega$ by the clause inductive above, and $S(n)=S(m)$ for $m=n\in\omega$, so $S(n)\in B$; in particular $n\in B$ implies $S(n)\in B$. By the clause induction above, $\omega\subseteq B$, which is the claim.

Omega-transitive. Let

$$B=\{n\in\omega:\forall u\,(u\in n\Rightarrow u\in\omega)\},$$

formed by class abstraction with the parameter $\omega$; its formula quantifies over the set variable $u$ only, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. Since $0\in\omega$ by the clause inductive above and $0$ has no element, $0\in B$. Let $n\in\omega$ with $n\in B$, and let $u\in S(n)$. Then $u\in n$, in which case $u\in\omega$ because $n\in B$, or $u=n$, in which case $u\in\omega$ because $n\in\omega$. Since also $S(n)\in\omega$ by the clause inductive above, $S(n)\in B$. By the clause induction above, $\omega\subseteq B$, which is the claim.

Element-transitive. Let

$$B=\{n\in\omega:\forall u\,\forall v\,((v\in u\wedge u\in n)\Rightarrow v\in n)\},$$

formed by class abstraction with the parameter $\omega$; its formula quantifies over the set variables $u$ and $v$ only, so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires. Since $0\in\omega$ by the clause inductive above and $0$ has no element, $0\in B$. Let $n\in\omega$ with $n\in B$, and let $u$ and $v$ be sets with $v\in u$ and $u\in S(n)$. Then $u\in n$ or $u=n$. If $u\in n$, then $v\in n$ because $n\in B$; if $u=n$, then $v\in n$ directly. In both cases $v\in S(n)$. Since also $S(n)\in\omega$ by the clause inductive above, $S(n)\in B$. By the clause induction above, $\omega\subseteq B$, which is the claim.