$\mathbb{N}\times \mathbb{N}\approx \mathbb{N}$

Apply [L1] with $X=\mathbb{N}$, $x_0=1$ and $F(x)=x+x$: this defines $m\mapsto 2^m$ with $2^0=1$ and $2^{\sigma (m)}=2^m+2^m$ for all $m$.

Every natural is even or odd: by induction, $0=0+0$ is even; and if $k=j+j$ is even then $\sigma (k)=\sigma (j+j)$ is odd, while if $k=\sigma (j+j)$ is odd then $\sigma (k)=\sigma (\sigma (j+j))=\sigma (\sigma (j)+j)=\sigma (j)+\sigma (j)$ is even, using $\sigma (j)+j=\sigma (j+j)$ and $x+\sigma (y)=\sigma (x+y)$.

No natural is both even and odd, that is $j+j\mathrm{\ne }\sigma (i+i)$ for all $i,j$: if $j\le i$ then $j+j\le i+j=j+i\le i+i<\sigma (i+i)$; if $i<j$ then $\sigma (i)\le j$, so $\sigma (i+i)<\sigma (\sigma (i+i))=\sigma (\sigma (i)+i)=\sigma (i)+\sigma (i)\le j+j$; in both cases the two sides differ by irreflexivity of $<$.

$\sigma$ is a bijection from $\mathbb{N}$ onto $\mathbb{N}\setminus \{0\}$: it is injective by [L2], its values are nonzero by [L2], and every nonzero natural is a value of $\sigma$ by [L2].

$2^m\mathrm{\ne }0$ for every $m$: by induction, $2^0=\sigma (0)\mathrm{\ne }0$; and if $2^m\mathrm{\ne }0$ then $2^m=\sigma (a)$ for some $a$ by [L2], so $2^{\sigma (m)}=2^m+2^m=2^m+\sigma (a)=\sigma (2^m+a)\mathrm{\ne }0$.

$2^{m+d}=2^m\cdot 2^d$ for all $m,d$: by induction on $d$, at $d=0$ both sides are $2^m$ since $m+0=m$ and $2^m\cdot 1=2^m$; and if $2^{m+d}=2^m\cdot 2^d$ then $2^{m+\sigma (d)}=2^{\sigma (m+d)}=2^{m+d}+2^{m+d}=2^m{2}^d+2^m{2}^d=2^m(2^d+2^d)=2^m\cdot 2^{\sigma (d)}$.

Define $J:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$ by $J(m,n)=2^m\cdot \sigma (n+n)$. Its values are nonzero: $2^m\mathrm{\ne }0$ by step 2.1 and $\sigma (n+n)\mathrm{\ne }0$ by [L2], so $J(m,n)\mathrm{\ne }0$ by [L5]. Thus $J$ maps into $\mathbb{N}\setminus \{0\}$.

$J$ is injective. Suppose $2^m\sigma (n+n)=2^{m^{\mathrm{\prime }}}\sigma (n^{\mathrm{\prime }}+n^{\mathrm{\prime }})$; by [L4] we may assume $m\le m^{\mathrm{\prime }}$, the other case being symmetric, and write $m^{\mathrm{\prime }}=m+d$. By step 2.2 the right side is $2^m(2^d\sigma (n^{\mathrm{\prime }}+n^{\mathrm{\prime }}))$, so cancelling the nonzero factor $2^m$ with [L5] and [L3] gives $\sigma (n+n)=2^d\cdot \sigma (n^{\mathrm{\prime }}+n^{\mathrm{\prime }})$. If $d\mathrm{\ne }0$ then $d=\sigma (e)$ by [L2] and $2^d=2^e+2^e$, so the right side equals $w+w$ with $w=2^e\sigma (n^{\mathrm{\prime }}+n^{\mathrm{\prime }})$, by [L3]; that would make $\sigma (n+n)$ both odd and even, contradicting step 1.3. Hence $d=0$ and $m^{\mathrm{\prime }}=m$, and then $\sigma (n+n)=\sigma (n^{\mathrm{\prime }}+n^{\mathrm{\prime }})$ gives $n+n=n^{\mathrm{\prime }}+n^{\mathrm{\prime }}$ by injectivity of $\sigma$, whence $n=n^{\mathrm{\prime }}$ because $n<n^{\mathrm{\prime }}$ would force $n+n<n^{\mathrm{\prime }}+n=n+n^{\mathrm{\prime }}<n^{\mathrm{\prime }}+n^{\mathrm{\prime }}$ by [L4] and [L3], and symmetrically for $n^{\mathrm{\prime }}<n$.

$J$ is surjective onto $\mathbb{N}\setminus \{0\}$: by strong induction [L6] we show every $k$ is $0$ or a value of $J$. Let $k\mathrm{\ne }0$ and assume the claim for all $j<k$. By step 1.2, $k$ is odd or even. If $k=\sigma (j+j)$ then $k=1\cdot \sigma (j+j)=2^0\sigma (j+j)=J(0,j)$ by [L3]. If $k=j+j$ then $j\mathrm{\ne }0$, since $j=0$ would give $k=0$; also $j<j+j=k$ by [L4], because $j+j=k$ with $j\mathrm{\ne }0$; so the hypothesis at $j$ and $j\mathrm{\ne }0$ give $j=2^m\sigma (n+n)$ for some $m,n$, and then $k=j+j=2^m\sigma (n+n)+2^m\sigma (n+n)=(2^m+2^m)\sigma (n+n)=2^{\sigma (m)}\sigma (n+n)=J(\sigma (m),n)$ by [L3] and step 1.1.

Therefore $J$ is a bijection from $\mathbb{N}\times \mathbb{N}$ onto $\mathbb{N}\setminus \{0\}$, and composing with the inverse of the bijection $\sigma$ of step 1.4 yields the bijection ${\sigma }^{-1}\circ J:\mathbb{N}\times \mathbb{N}\to \mathbb{N}$; hence $\mathbb{N}\times \mathbb{N}\approx \mathbb{N}$ and $\mathbb{N}\times \mathbb{N}$ is countably infinite.