Proof of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets

Throughout we use claim 4 of Basic Properties of Finite Sets: if a set having a number of elements admits a surjection onto a set $Z$, then $Z$ is finite and nonempty.

Claim 1. If $A=\emptyset$ or $B=\emptyset$ then $A\times B=\emptyset$ by Cartesian Product of Two Sets, via Ordered Pairs, which is finite. So assume both are nonempty, and let $B$ have $l$ elements. We argue by induction on the number of elements of $A$, using the induction principle for the natural numbers; let $\mathcal{P}$ be the set of natural numbers $k$ such that $A\times B$ is finite whenever $A$ has $k$ elements.

For any object $a$, let $\beta_{a}:B\to\{a\}\times B$ send $b$ to the ordered pair $(a,b)$. It is surjective: by Cartesian Product of Two Sets, via Ordered Pairs every element of $\{a\}\times B$ is $(a',b)$ with $a'\in\{a\}$ and $b\in B$, so $a'=a$. It is injective: if $(a,b)=(a,b')$ then $b=b'$ by Characteristic Property of the Ordered Pair. Hence $\beta_{a}$ is a bijection, which is the first assertion of claim 1, and $\{a\}\times B$ is finite by claim 4 of Basic Properties of Finite Sets. If $A$ has $1$ element, let $\psi:[1]\to A$ be a bijection; since $[1]$ consists of $1$ alone, $A=\{\psi(1)\}$, so $A\times B$ is finite by the previous sentence and $1\in\mathcal{P}$.

Suppose $k\in\mathcal{P}$ and let $A$ have $S(k)$ elements. By claim 2 of Peeling an Element off a Finite Set, and Unions of Finite Sets there are $A'$ with $k$ elements and $a\in A$ with $A=A'\cup\{a\}$. By Cartesian Product of Two Sets, via Ordered Pairs, $A\times B=(A'\times B)\cup(\{a\}\times B)$, since every element of $A\times B$ is $(a'',b)$ with $a''\in A$ and $b\in B$, and $a''$ lies in $A'$ or equals $a$. The first set is finite by the induction hypothesis and the second by the previous paragraph, so their union is finite by claim 3 of Peeling an Element off a Finite Set, and Unions of Finite Sets. Hence $S(k)\in\mathcal{P}$.

Claim 2. By Cartesian Product of Two Sets, via Ordered Pairs every element $p$ of $Y^{n}\times Y$ is $(t,x)$ for some $t\in Y^{n}$ and some $x\in Y$, and by Characteristic Property of the Ordered Pair those $t$ and $x$ are determined by $p$. Hence the prescription in the statement assigns to each such $p$ exactly one value, so there is exactly one map $q$ with the stated property: the map sending $p=(t,x)$ to the tuple $u$ with $u_{k}=t_{k}$ for $k\in[n]$ and $u_{S(n)}=x$. This $u$ is a well-defined element of $Y^{S(n)}$, because every $k\in[S(n)]$ satisfies exactly one of $k\in[n]$ and $k=S(n)$, by the order facts of Properties of the Order on the Natural Numbers.

The map $q$ is surjective: given $u\in Y^{S(n)}$, let $t$ be the restriction of $u$ to $[n]$ and let $x=u_{S(n)}$; then $q\bigl((t,x)\bigr)=u$. It is injective: if $q\bigl((t,x)\bigr)=q\bigl((t',x')\bigr)$, then comparing components at each $k\in[n]$ gives $t_{k}=t'_{k}$, so $t=t'$, and comparing components at $S(n)$ gives $x=x'$; hence $(t,x)=(t',x')$ by Characteristic Property of the Ordered Pair. So $q$ is a bijection.

Claim 3. We argue by induction on $n$. Let $\mathcal{Q}$ be the set of natural numbers $n$ such that $X^{n}$ is nonempty and finite.

For $n=1$, the set $[1]$ consists of $1$ alone, so the map $X\to X^{1}$ sending $x$ to the tuple $t$ with $t_{1}=x$ is surjective; since $X$ is nonempty and finite it has some number of elements, so claim 4 of Basic Properties of Finite Sets gives that $X^{1}$ is nonempty and finite.

Suppose $n\in\mathcal{Q}$. By claim 1 the set $X^{n}\times X$ is finite, and it is nonempty because $X^{n}$ and $X$ are, so it has some number of elements. By claim 2 applied with $Y=X$ there is a bijection $q:X^{n}\times X\to X^{S(n)}$, which is in particular surjective, so claim 4 of Basic Properties of Finite Sets gives that $X^{S(n)}$ is nonempty and finite. Hence $S(n)\in\mathcal{Q}$.

Claim 4. By claim 1 of Basic Properties of Finite Sets the set $[n]$ has $n$ elements, and it is nonempty since $1\in[n]$; so $[n]^{n}$ is finite by claim 3. Every element of $S_{n}$ is in particular a map from $[n]$ to $[n]$, by Permutation of the Set $\{1,\dots,r\}$, so $S_{n}\subseteq[n]^{n}$ by Tuples in a Set, and claim 3 of Basic Properties of Finite Sets gives that $S_{n}$ is finite. It is nonempty because the identity map of $[n]$ is a bijection and hence belongs to $S_{n}$.