ThmDex – An index of mathematical definitions, results, and conjectures.
Result R263 on D16: Countable set
Binary cartesian product of countable sets is countable

Let $X$ and $Y$ each be a D16: Countable set such that
 (i) $X \times Y$ is the D191: Binary cartesian set product of $X$ with $Y$
Then $X \times Y$ is a D16: Countable set.
Proofs
Proof 0
Let $X$ and $Y$ each be a D16: Countable set such that
 (i) $X \times Y$ is the D191: Binary cartesian set product of $X$ with $Y$
Due to results
we may assume that $X \times Y$ as well as $X$ and $Y$ are each nonempty.

Since $X$ and $Y$ are countable, then there exists surjections $f : \mathbb{N} \to X$ and $g : \mathbb{N} \to Y$. Define the map $$h : \mathbb{N} \times \mathbb{N} \to X \times Y, \quad h(n, m) : = (f(n), g(m))$$ The goal is to show that $h$ is a surjection. To this end, fix $(x, y) \in X \times Y$. Since $f$ and $g$ are surjections, then there exists $n, m \in \mathbb{N}$ such that $f(x) = n$ and $f(y) = m$. Result R3346: Characterisation of equality of ordered pairs implies that $(n, m) = (f(x), f(y)) = h(x, y)$ and hence $h$ is a surjection.

Result R511: Natural number plane is countable shows that there exists a surjection $s : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$. We can now form the composite map $$h \circ s : \mathbb{N} \to X \times Y, \quad (h \circ s)(n) = (f(n), g(m))$$ whence result R315: Composition of surjections is surjection guarantees that $h \circ s$ is a surjection. This finishes the proof. $\square$