axiomatic sets 17 (arithmetic in natural numbers)

The set of all natural numbers is closed under addition (and multiplication).

We have already defined one equation of addition.
\[ n+1=n\cup\left\{ n \right\} \qquad (n\in\mathbb{N}, 0\in\mathbb{N},1=\left\{ 0 \right\})  \]

Since, for any natural number $n$ , there must be an $n\cup\left\{ n \right\}$ by axiom of infinity,
and for any natural number $m\ne 0$ , there must be an $n$ such that $n\cup\left\{ n \right\}=m$ ,
this equation is true.

We want to extend this to the definition of "$a+b$".

For this purpose the function "$f$" is needed.

A collection of a pair of two natural numbers is a set.
(i.e. Cartesian Product of two $\mathbb{N}$s is a set. )
\[ \mathbb{N}\times\mathbb{N}=\left\{\left\{ a,b \right\}: a\in\mathbb{N},b\in\mathbb{N} \right\}  \]

In axiomatic set theory,  as the function $f$ is also a set,
\[ f:\mathbb{N}\times\mathbb{N}\rightarrow \mathbb{N} , \]
and
\[ \forall a\forall b\exists f[f(\left\{a,b  \right\})\in\mathbb{N}] ,  \]
and $f$  has to be satisfied the following two conditions;

(1)$f(\left\{a,0\right\})=a$
(2)$f(\left\{a,b^+\right\})=(f(\left\{a,b\right\}))^+$

,where $b^+$ is the successor set of $b$ . Namely, $b^+=b\cup\left\{ b \right\} $ .

You may see it is not easy to understand. However, its mean, simply,
(1)$a+0=a$ ,
(2)$a+(b+1)=(a+b)+1$ .

If $b$ is not $0$, there exists a $c$ such that $c^+=c+1=b$ .
Thus,
\[ a+(b+1)=(a+b)+1=(a+c^+)+1=(a+(c+1))+1=((a+c)+1)+1 . \]

Same operations take us to
\[ a+b=(\cdots(a+0)+1)+1)\cdots )+1 . \]

,where $(\cdots (0+1)+1)\cdots )+1=b$ .

This is the definition of an arithmetic of addition in axiomatic set theory.