$\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 \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 \ne 0$ for every $m$: by induction, $2^0 = \sigma(0) \ne 0$; and if $2^m \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) \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 \ne 0$ by step 2.1 and $\sigma(n+n) \ne 0$ by [L2], so $J(m,n) \ne 0$ by [L5]. Thus $J$ maps into $\mathbb{N} \setminus \{0\}$.

$J$ is injective. Suppose $2^m \sigma(n+n) = 2^{m'} \sigma(n'+n')$; by [L4] we may assume $m \le m'$, the other case being symmetric, and write $m' = m + d$. By step 2.2 the right side is $2^m (2^d \sigma(n'+n'))$, so cancelling the nonzero factor $2^m$ with [L5] and [L3] gives $\sigma(n+n) = 2^d \cdot \sigma(n'+n')$. If $d \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'+n')$, by [L3]; that would make $\sigma(n+n)$ both odd and even, contradicting step 1.3. Hence $d = 0$ and $m' = m$, and then $\sigma(n+n) = \sigma(n'+n')$ gives $n + n = n' + n'$ by injectivity of $\sigma$, whence $n = n'$ because $n < n'$ would force $n + n < n' + n = n + n' < n' + n'$ by [L4] and [L3], and symmetrically for $n' < 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 \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 \ne 0$, since $j = 0$ would give $k = 0$; also $j < j + j = k$ by [L4], because $j + j = k$ with $j \ne 0$; so the hypothesis at $j$ and $j \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.