Proof of The Maps from a Finite Set to a Nonempty Finite Set Form a Nonempty Finite Set

Each result cited is universally quantified over the data in its own statement.

Since $T$ is nonempty and finite, it has $q$ elements for some $q\in\mathbb{N}$, and we may fix $t_{0}\in T$.

Nonemptiness. For every set $Y$ the constant map $Y\to T$ with value $t_{0}$ belongs to $\mathrm{Map}(Y,T)$, so $\mathrm{Map}(Y,T)$ is nonempty.

A preliminary remark. The initial segment $[1]$ is $\{1\}$ by claim 2 of Basic Properties of Initial Segments of the Natural Numbers. Hence a set $Y$ with $1$ element is $\{a\}$ for $a=\beta(1)$, where $\beta:[1]\to Y$ is a bijection.

Finiteness, by induction. Let $A$ be the set of those $p\in\mathbb{N}$ such that $\mathrm{Map}(Y,T)$ is finite for every set $Y$ with $p$ elements. We show $A=\mathbb{N}$ by the principle of induction Principle of Induction for the Natural Numbers.

$1\in A$. Let $Y$ have $1$ element; by the remark $Y=\{a\}$. For $t\in T$ let $c(t)\in\mathrm{Map}(Y,T)$ be the map sending $a$ to $t$. The map $c:T\to\mathrm{Map}(Y,T)$ is surjective, because every $f\in\mathrm{Map}(Y,T)$ equals $c(f(a))$, the two maps having the same value at the only point $a$ of $Y$. Since $T$ has $q$ elements, claim 4 of Basic Properties of Finite Sets shows that $\mathrm{Map}(Y,T)$ has $m$ elements for some $m\in\mathbb{N}$, so it is finite by Finite Set.

If $p\in A$ then $S(p)\in A$. Let $Y$ have $S(p)$ elements. By claim 2 of Peeling an Element off a Finite Set, and Unions of Finite Sets there are a subset $Y'\subseteq Y$ with $p$ elements and $x\in Y$ with $x\notin Y'$ and $Y=Y'\cup\{x\}$. Since $p\in A$, the set $\mathrm{Map}(Y',T)$ is finite, and it is nonempty by the first paragraph. By claim 1 of Finiteness of Cartesian Products, Tuple Sets, and Permutation Sets the Cartesian product $\mathrm{Map}(Y',T)\times T$ is finite; it contains the pair of the constant map with value $t_{0}$ and $t_{0}$, so it is nonempty and has $m'$ elements for some $m'\in\mathbb{N}$. For $g\in\mathrm{Map}(Y',T)$ and $t\in T$ let $E((g,t))\in\mathrm{Map}(Y,T)$ be the map whose value at $y\in Y'$ is $g(y)$ and whose value at $x$ is $t$; this is well defined because $Y=Y'\cup\{x\}$ and $x\notin Y'$. The map $E:\mathrm{Map}(Y',T)\times T\to\mathrm{Map}(Y,T)$ is surjective: for $f\in\mathrm{Map}(Y,T)$, let $f'$ be the restriction of $f$ to $Y'$; then $E((f',f(x)))$ and $f$ agree at every point of $Y'$ and at $x$, so they are equal. By claim 4 of Basic Properties of Finite Sets, $\mathrm{Map}(Y,T)$ has $m$ elements for some $m\in\mathbb{N}$, so it is finite by Finite Set. Thus $S(p)\in A$.

By Principle of Induction for the Natural Numbers, $A=\mathbb{N}$.

Conclusion. The given $Y$ is nonempty and finite, so by Finite Set it has $p$ elements for some $p\in\mathbb{N}$. Since $p\in A$, $\mathrm{Map}(Y,T)$ is finite, and it is nonempty by the first paragraph. This proves (Finiteness).