Theorem NBFPS

There exist no bijections from $\text{Fin}(n)$ to a proper subset of itself.

Proof: Do induction on $n\in\mathbb{N}$:

1. $\text{Fin}(0)=\emptyset$ has no proper subsets. So, trivially, $\text{Fin}(0)$ has no proper subsets bijective to it.
2. Now suppose there are no bijections from $\text{Fin}(n)$ to a proper subset of it. Then, by the contrapositive of the previous lemma, $\text{Fin}(S(n))$ has no bijections to a strict subset of it.

Rephrasing the above theorem a little bit, one gets the following: if there is a bijection from $\text{Fin}(n)$ to a subset of itself, then that subset is the whole of $\text{Fin}(n)$.

Corollary NoBijFnFk

There exist no bijections from $\text{Fin}(n)$ to $\text{Fin}(k)$ where $k<n$.

Corollary ifInjthenBij

If $f:\text{Fin}(n) \to Y\subseteq\text{Fin}(n)$ is injective, then it is also surjective and, in fact, $Y=\text{Fin}(n)$.

Proof: By Lemma RSIS, restricting $f$'s codomain to $f(\text{Fin}(n))$ produces a bijection. So, by the previous theorem, it must be that $f(\text{Fin}(n))=\text{Fin}(n)$. But then, by Lemma ISSI, $\text{Fin}(n)=f(\text{Fin}(n)) \subseteq Y$. Hence, $Y=\text{Fin}(n)$ (as $Y\subseteq\text{Fin}(n)$ by hypothesis), so that $f(\text{Fin}(n))=Y$. But this means precisely that $f$ is surjective.

Corollary FnFkInjthenSurj

If there is an injection from $\text{Fin}(n)$ to $\text{Fin}(k)$ where $k \leq n$, then it also a surjection and, in fact, $k=n$.

There is also a surjective analog of Corollary ifInjthenBij.

Lemma SurjInvBij

Surjection produces Inverted Bijection: If $f:\text{Fin}(n)\to\text{Fin}(n)$ is an surjection, then there exists a bijection $f':\text{Fin}(n)\to\text{Fin}(n)$ such that $f(f'(y))=y$ for $y\in\text{Fin}(n)$.

Proof: By theorem's hypothesis, $f^{-1}(y)\neq\emptyset$ and $f^{-1}(y)\subseteq\text{Fin}(n)\subseteq\mathbb{N}$ for any $y\in\text{Fin}(n)$. Thus by well-ordering, for every $y\in\text{Fin}(n)$, there is a unique element $\text{min}(f^{-1}(y)) \in f^{-1}(y)$. So, the following function is automatically well-defined: $f':\text{Fin}(n) \ni y\mapsto\text{min}(f^{-1}(y)) \in f^{-1}(y)\subseteq\text{Fin}(n)$

Next, for any $y\in\text{Fin}(n)$, $f'(y)=\text{min}(f^{-1}(y)) \in f^{-1}(y)$. Hence, by definition of the set $f^{-1}(y)$, $f(f'(y))=y$.

Finally, to show this function's bijectivity, I will instead show its injectivity. That it is surjective will then follow from Corollary ifInjthenBij. So, suppose for $y,y'\in\text{Fin}(n)$ that $f'(y)=f'(y')$. Then, by the definition of $f'$, $\text{min}(f^{-1}(y))=\text{min}(f^{-1}(y'))$. So, $y=f(\text{min}(f^{-1}(y)))=f(\text{min}(f^{-1}(y')))=y'$ since $f$, being a function, maps values to unique values.

Corollary ifSurjthenBij

If $f:\text{Fin}(n)\to\text{Fin}(n)$ is a surjection, then it is also a bijection.

This result is a straightforward application of the previous lemma and Lemma LInvBijThenBij. I leave it for the readers to fill in the relevant details.

Lemma BFxSABFSxSS

Bijection from $\text{Fin}(n)$ to Set Ascends to Bijection from $\text{Fin}(S(n))$ to Superset: Fix an $n\in\mathbb{N}$. If for an arbitrary set $X$ one has a bijection $f:\text{Fin}(n) \to X$, then for arbitrary $y\in\mathcal{U}$ such that $y \notin X$, one has a bijection $\tilde{f}:\text{Fin}(S(n)) \to X\cup\{y\}$.

Proof Sketch: Define $\tilde{f}:\text{Fin}(S(n)) \to X\cup\{y\}$ thus: $\tilde{f}(x)=\begin{cases} f(x) &\text{if } x<n \\ y &\text{if } x=n \end{cases}$ Now, every $x\in\text{Fin}(S(n))$ is either less that $n$ or is $n$. If $x<n$, $\tilde{f}(x)$ refers to the unique value $f(x)$ in $X$ since $f$ is a well-defined by hypothesis. If $x=n$, $\tilde{f}(x)$ obviously refers to the unique value $y \in X\cup\{y\}$. In both cases, $\tilde{f}$ maps each value in its domain to a unique value in its codomain, making the function well-defined. A proof of bijectivity is left to the reader.

Theorem SFnBSFk

Subset of $\text{Fin}(n)$ is Bijective to Some $\text{Fin}(k)$: Fix an $n\in\mathbb{N}$. For every $U\subseteq\text{Fin}(n)$, there is a $k \leq n$ with some bijection from $\text{Fin}(k)$ to $U$.

Proof: Do induction on $n\in\mathbb{N}$:

1. If $U\subseteq\text{Fin}(0)=\emptyset$, then $U=\emptyset$. So, there is a $k$, namely $0$, and a bijection, namely $\text{id}_\emptyset:\emptyset=\text{Fin}(k)=\text{Fin}(0) \ni x\mapsto x \in U=\emptyset$ This function is vacuously well-defined and vacuously bijective.
2. Now suppose the claim is true for $\text{Fin}(n)$. Consider any $U\subseteq\text{Fin}(S(n))$. If $n \notin U$, then certainly $U\subseteq\text{Fin}(n)$. So immediately, the inductive hypothesis gives a $k \leq n<S(n)$ and a bijection $\text{Fin}(k) \to U$. Now, suppose $n \in U$. Here, $U\setminus\{n\}\subseteq\text{Fin}(n)$ and the inductive hypothesis gives a $k \leq n<S(n)$ and a bijection $f:\text{Fin}(k) \to U\setminus\{n\}$. Lift this smaller bijection to a bigger bijection from $f^U:\text{Fin}(S(k))$ to $U$ as per the lemma above. Note furthermore that as $k<S(n)$, $S(k) \leq S(n)$. Hence, this bijection satisfies the theorem's requirements as applied to $\text{Fin}(S(n))$.

Corollary SFnBSUFk

Subset of $\text{Fin}(n)$ is Bijective to Some Unique $\text{Fin}(k)$: Fix an $n\in\mathbb{N}$. For every $U\subseteq\text{Fin}(n)$, there is exactly one $k \leq n$ with some bijection from $\text{Fin}(k)$ to $U$.

Proof: Continuing from the end of the previous proof, only the uniqueness part remains to be shown. For this, the reader should keep in their minds results about functions shown earlier. So, suppose there is some other $\tilde{k}\in\mathbb{N}$ with a bijection $\text{Fin}(\tilde{k}) \to U$. Now, totality gives either $\tilde{k} \leq k$ or $k\leq\tilde{k}$. Assume w.l.o.g. that $\tilde{k} \leq k$; the other case is handled similarly. Continuing, the bijection associated with $\tilde{k}$ induces a left inverse $\phi:U\to\text{Fin}(\tilde{k})$ that is also a bijection. Composing, one gets a bijectiion $(\phi \circ f):\text{Fin}(k)\to\text{Fin}(\tilde{k})$. Since $\tilde{k} \leq k$, it must be that $\text{Fin}(\tilde{k})\subseteq\text{Fin}(k)$. But $\text{Fin}(k)$ is not bijective to any of its proper subsets. Hence, $\text{Fin}(\tilde{k})=\text{Fin}(k)$, so that $\tilde{k}=k$.