ThmDex – An index of mathematical definitions, results, and conjectures.
Result R508 on D16: Countable set
Finite cartesian product of countable sets is countable
Formulation 0
Let $X_1, \ldots, X_N$ each be a D16: Countable set such that
(i) $\prod_{n = 1}^N X_n$ is a D326: Cartesian product of $X_1, \ldots, X_N$
Then $\prod_{n = 1}^N X_n$ is a D16: Countable set.
Proofs
Proof 0
Let $X_1, \ldots, X_N$ each be a D16: Countable set such that
(i) $\prod_{n = 1}^N X_n$ is a D326: Cartesian product of $X_1, \ldots, X_N$
Let $X_1, X_2, X_3, \ldots$ be countable sets. Due to results
(i) R4262: Finite cartesian product with empty set is empty
(ii) R507: Empty set is countable

we may assume that all of $X_1, X_2, X_3, \ldots$ are nonempty. Consider the sets $Y_1, Y_2, Y_3, \ldots$ defined by \begin{equation} Y_N : = \prod_{n = 1}^N X_n \end{equation} We proceed by induction on $N$. The base case of $N = 1$ is immediate since $X_1$ is assumed to be countable. As an induction hypothesis, assume then that $Y_N$ is countable for some $N \geq 1$. We must show that this implies that $Y_{N + 1}$ is countable. Since $Y_N$ and $X_{N + 1}$ are countable, result R263: Binary cartesian product of countable sets is countable guarantees that the cartesian product \begin{equation} Y_N \times X_{N + 1} = \left( \prod_{n = 1}^N X_n \right) \times X_{N + 1} \end{equation} is countable. Further, result R1848: Bijection between parenthesis-sliced cartesian products shows that \begin{equation} |Y_N \times X_{N + 1}| = |Y_{N + 1}| \end{equation} That is, $Y_{N + 1}$ is countable. The claim is now a consequence of R800: Proof by principle of weak mathematical induction. $\square$