Proof of Multiplication on Omega: Products Lie in Omega, Multiplication Is a Binary Operation with Value the Product, and Membership in the Multiplication

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited. 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(k)\in\omega$ for every $k\in\omega$. The ordered pair of two sets is a set by The Ordered Pair of Two Sets and Nested Tuples §pair.

Sums. Let $u,m\in\omega$. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, applied to the class $+$ of Addition on Omega §addition with the witnesses $u$ and $m$, $((u,m),u+m)\in{+}$. So $u+m$ lies in the range of $+$ by Relations, Domain, Range, Inverse and Composition §range, and this range is included in $\omega$ by Functions, Values of a Function, and Functions from One Class to Another §map, since $+$ is a map $\omega\times\omega\to\omega$ by Addition on Omega §addition. Thus $u+m\in\omega$.

The maps $\tau_{m}$. Fix $m\in\omega$ and let $\tau_{m}$ be as in Multiplication on Omega §multiplication. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, a set $p$ lies in $\tau_{m}$ if and only if $p=((n,u),u+m)$ for some $n,u\in\omega$. Each element of $\tau_{m}$ is thus an ordered pair, so $\tau_{m}$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. If $(q,v)\in\tau_{m}$, then $(q,v)=((n,u),u+m)$ for some $n,u\in\omega$, and The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic gives $q=(n,u)$ and $v=u+m$. Hence, if $(q,v)$ and $(q,v')$ lie in $\tau_{m}$, with $q=(n,u)$, $v=u+m$, $q=(n',u')$ and $v'=u'+m$, then The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic applied to $(n,u)=(n',u')$ gives $u=u'$, so $v=v'$; thus $\tau_{m}$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function. By Relations, Domain, Range, Inverse and Composition §domain, a set $q$ lies in $\operatorname{dom}\tau_{m}$ if and only if $(q,v)\in\tau_{m}$ for some set $v$; by what was just shown this forces $q=(n,u)$ with $n,u\in\omega$, and conversely such a $q$ satisfies $(q,u+m)\in\tau_{m}$. By The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, the sets of the form $(n,u)$ with $n,u\in\omega$ are exactly the elements of $\omega\times\omega$, so $\operatorname{dom}\tau_{m}=\omega\times\omega$ by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality. By Relations, Domain, Range, Inverse and Composition §range, each element $v$ of $\operatorname{ran}\tau_{m}$ satisfies $(q,v)\in\tau_{m}$ for some set $q$, so $v=u+m$ for some $u\in\omega$, and $v\in\omega$ by the paragraph on sums; so $\operatorname{ran}\tau_{m}\subseteq\omega$ by Subclasses and Subsets §subclass. Hence $\tau_{m}:\omega\times\omega\to\omega$ is a map by Functions, Values of a Function, and Functions from One Class to Another §map, and for $n,u\in\omega$ its value is $\tau_{m}((n,u))=u+m$ by Functions, Values of a Function, and Functions from One Class to Another §value, since $((n,u),u+m)\in\tau_{m}$.

The recursion. With $m$ and $\tau_{m}$ as above, The Recursion Theorem on Omega §recursion, applied with $a=\omega$, $c=0$ and $g=\tau_{m}$, gives exactly one map $f:\omega\to\omega$ with $f(0)=0$ and $f(S(k))=\tau_{m}((k,f(k)))$ for every $k\in\omega$. For every map $h:\omega\to\omega$ and every $k\in\omega$, $k\in\operatorname{dom}h$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $(k,h(k))\in h$ by Functions, Values of a Function, and Functions from One Class to Another §value, hence $h(k)\in\operatorname{ran}h$ by Relations, Domain, Range, Inverse and Composition §range, and $\operatorname{ran}h\subseteq\omega$ by Functions, Values of a Function, and Functions from One Class to Another §map; so $h(k)\in\omega$ and therefore $\tau_{m}((k,h(k)))=h(k)+m$ by the value of $\tau_{m}$ computed above. In particular $f(S(k))=f(k)+m$ for every $k\in\omega$. Since $\operatorname{dom}f=\omega$ is a set, $f$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set.

Products lie in $\omega$ (clause values). Let $m,n\in\omega$ and let $f$ be the map of the previous paragraph for this $m$. The set $f$ witnesses the formula defining $m\cdot n$ in Multiplication on Omega §multiplication with $z=f(n)$. Conversely, let $z$ be a set witnessed by a set $f'$ with $f':\omega\to\omega$, $f'(0)=0$, $f'(S(k))=f'(k)+m$ for every $k\in\omega$, and $z=f'(n)$. By the previous paragraph applied to $h=f'$, $f'(S(k))=f'(k)+m=\tau_{m}((k,f'(k)))$ for every $k\in\omega$, so $f'=f$ by the uniqueness in The Recursion Theorem on Omega §recursion, and $z=f(n)$. Hence $f(n)$ is the unique set satisfying that formula, that is, $m\cdot n=f(n)$, and $f(n)\in\omega$ by the previous paragraph applied to $h=f$. Thus $m\cdot n\in\omega$.

Membership (clause membership). Let $m$, $n$ and $z$ be sets. Then $(m,n)$ and $((m,n),z)$ are sets by The Ordered Pair of Two Sets and Nested Tuples §pair, so by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, applied to the class $\cdot$ of Multiplication on Omega §multiplication, $((m,n),z)\in{\cdot}$ if and only if there are $m',n'\in\omega$ with $((m,n),z)=((m',n'),m'\cdot n')$, where $m'\cdot n'$ is a set by the previous paragraph. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, applied first to these two pairs and then to $(m,n)=(m',n')$, this equation holds if and only if $m=m'$, $n=n'$ and $z=m'\cdot n'$. Hence $((m,n),z)\in{\cdot}$ if and only if $m\in\omega$, $n\in\omega$ and $z=m\cdot n$, the backward direction taking $m'=m$ and $n'=n$.

Binary operation (clause operation). By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, every element of $\cdot$ equals $((m',n'),m'\cdot n')$ for some $m',n'\in\omega$; so it is an ordered pair, and $\cdot$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. Moreover, if $(q,v)\in{\cdot}$, then $(q,v)=((m',n'),m'\cdot n')$ for some $m',n'\in\omega$, so $q=(m',n')$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; then $((m',n'),v)\in{\cdot}$, and $v=m'\cdot n'$ by the previous paragraph. Now let $(q,v)$ and $(q,v')$ lie in $\cdot$. Writing $q=(m',n')$ with $m',n'\in\omega$, the previous paragraph, applied to $((m',n'),v)$ and to $((m',n'),v')$, gives $v=m'\cdot n'=v'$; so $\cdot$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function. By Relations, Domain, Range, Inverse and Composition §domain, a set $q$ lies in $\operatorname{dom}{\cdot}$ if and only if $(q,v)\in{\cdot}$ for some set $v$; this forces $q=(m',n')$ with $m',n'\in\omega$, and conversely for $m,n\in\omega$ the previous paragraph gives $((m,n),m\cdot n)\in{\cdot}$. As for $\tau_{m}$, The Cartesian Product of Two Classes §product, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Class Theory NBG: the Axioms, Standing Conventions and Basic Notation §extensionality give $\operatorname{dom}{\cdot}=\omega\times\omega$. By Relations, Domain, Range, Inverse and Composition §range, each element $v$ of $\operatorname{ran}{\cdot}$ satisfies $(q,v)\in{\cdot}$ for some set $q$, so $v=m'\cdot n'$ with $m',n'\in\omega$, and $v\in\omega$ by the paragraph on products; so $\operatorname{ran}{\cdot}\subseteq\omega$ by Subclasses and Subsets §subclass. Hence $\cdot$ is a map $\omega\times\omega\to\omega$ by Functions, Values of a Function, and Functions from One Class to Another §map, that is, since $\omega$ is a set, a binary operation on $\omega$ by Binary Operations on a Set §operation. Finally, for $m,n\in\omega$ we have $(m,n)\in\operatorname{dom}{\cdot}$ and $((m,n),m\cdot n)\in{\cdot}$, so the value of $\cdot$ at $(m,n)$ is $m\cdot n$ by Functions, Values of a Function, and Functions from One Class to Another §value.