Addition on Omega

In the setting of Class Theory NBG: the Axioms, Standing Conventions and Basic Notation, let $\omega$ and $0$ be as in The Class Omega of Natural Numbers with Zero §omega and The Class Omega of Natural Numbers with Zero §zero, and let $S(x)$ denote the successor of a set $x$. By Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §set, $\omega$ is a set, and by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §inductive, $0\in\omega$ and $S(u)\in\omega$ for every $u\in\omega$. Below, $m,n,k,u,z,f,p$ are set variables, and each class is formed by class abstraction from a formula quantifying over set variables only, in which the ordered pair, $S(u)$, the values of functions and the sums $m+n$ introduced below are defined set symbols; so it is predicative as Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §comprehension requires.

¶ Let $\sigma=\{p:\exists n\,\exists u\,(n\in\omega\wedge u\in\omega\wedge p=((n,u),S(u)))\}$. It is a map $\sigma:\omega\times\omega\to\omega$ with $\sigma((n,u))=S(u)$: it is a relation, and two of its elements with the same first coordinate $(n,u)$ have the same second coordinate $S(u)$, by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, so it is a function; its domain is the Cartesian product $\omega\times\omega$ by The Cartesian Product of Two Classes §product and Relations, Domain, Range, Inverse and Composition §domain; its range is included in $\omega$ because $S(u)\in\omega$; and its value is given by Functions, Values of a Function, and Functions from One Class to Another §value. For $m\in\omega$, The Recursion Theorem on Omega §recursion, applied with $a=\omega$, $c=m$ and $g=\sigma$, gives exactly one map $f:\omega\to\omega$ with $f(0)=m$ and $f(S(k))=\sigma((k,f(k)))=S(f(k))$ for every $k\in\omega$, the last equality by the value of $\sigma$ just computed; it is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set, its domain $\omega$ being a set. For $m,n\in\omega$, the sum $m+n$ is the unique set $z$ satisfying

$$\exists f\,\bigl(f:\omega\to\omega\wedge f(0)=m\wedge\forall k\,(k\in\omega\Rightarrow f(S(k))=S(f(k)))\wedge z=f(n)\bigr):$$

the map just described is a set witnessing this formula, and every set $f$ witnessing it satisfies $f(S(k))=S(f(k))=\sigma((k,f(k)))$ for every $k\in\omega$, hence equals that map by the uniqueness in The Recursion Theorem on Omega §recursion; so $m+n$ is a defined set symbol, used only for $m,n\in\omega$, and $m+n=f(n)\in\omega$, since $f(n)$ lies in the range of $f$, which is included in $\omega$ by Functions, Values of a Function, and Functions from One Class to Another §map. The addition on $\omega$ is the class

$${+}=\{p:\exists m\,\exists n\,(m\in\omega\wedge n\in\omega\wedge p=((m,n),m+n))\}.$$

By the argument given above for $\sigma$, with $m+n\in\omega$ in place of $S(u)\in\omega$, it is a map ${+}:\omega\times\omega\to\omega$, that is, a binary operation on $\omega$, whose value at $(m,n)$, written as in Binary Operations on a Set §notation, is $m+n$ by Functions, Values of a Function, and Functions from One Class to Another §value, since $((m,n),m+n)\in{+}$.