Sets of the form $\text{Fin}(n)$ have special properties that are not satisfied by arbitrary sets. In this section, a few intermediate results are developed to warm up to these peculiar properties.

Lemma SFSxWSFx

Subset of $\text{Fin}(S(n))$ Without $n$ is Subset of $\text{Fin}(n)$: $U\subseteq\text{Fin}(n)$ if $U\subseteq\text{Fin}(S(n))$ and $n \notin U$.

Proof: Fix any $u \in U$; I show that $u\in\text{Fin}(n)$. Well, since $n \notin U$, $u \neq n$. At the same time, since $U\subseteq\text{Fin}(S(n))$, $u\in\text{Fin}(S(n))$ i.e. $u\in\mathbb{N}$ and $u<S(n)$; thus, by a lemma from the previous chapter, $u \leq n$. So, altogether, $u \leq n$ and $u \neq n$ i.e. $u<n$. Hence, $u\in\text{Fin}(n)$.

Lemma BFSxSDBFxSS

Bijection from $\text{Fin}(S(n))$ to Set Descends to Bijection from $\text{Fin}(n)$ to Subset: Fix an $n\in\mathbb{N}$. If for an arbitrary set $X$ one has a bijection $f:\text{Fin}(S(n)) \to X$, then for any $x \in X$, one has a bijection $f':\text{Fin}(n) \to X'=X\setminus\{x\}$.

Proof: Since $f$ is surjective, there is a natural $k\in\text{Fin}(S(n))$ such that $f(k)=x$. There are two cases to consider:

Suppose first that $k=n$: Restrict $f$ to the domain $\text{Fin}(n)$ and the codomain $f(\text{Fin}(n))$ as described in Lemma RSIS. By the lemma, this restriction is bijective. It remains to be seen that $f(\text{Fin}(n))=X\setminus\{x\}=X'$

To see this, one first shows that $f(\text{Fin}(n)) \subseteq X'$. Well, notice that by Lemma ISSI and the fact that $\text{Fin}(n)\subseteq\text{Fin}(S(n))$, one has $f(\text{Fin}(n)) \subseteq X$. Also, $x=f(n) \notin f(\text{Fin}(n))$ for if it were, there would be some $k'\in\text{Fin}(n)$ such that $f(k')=x$. So by the injectivity of $f$, one would have $n=k'\in\text{Fin}(n)$, which is a contradiction.

Next, one shows that $X' \subseteq f(\text{Fin}(n))$. So let $y \in X'$. Then certainly $y \in X$. So by the surjectivity of $f$, there is some $k'\in\text{Fin}(S(n))$ such that $f(k')=y$. But as $y$ is in $X'$ which does not contain $x$, $f(k')=y \neq x=f(n)$ Hence, $k' \neq n$ because $f$, being a function, cannot map a single value to two different values. Altogether, one then has $k'\in\text{Fin}(n)$ so that $y \in f(\text{Fin}(n))$ as there is the element $k'$ in $\text{Fin}(n)$ mapping to $y$.

Thus, the restriction mentioned in the first paragraph is the required bijection from $\text{Fin}(n)$ to $X'$.

Suppose next that $k \neq n$: In this case, $k\in\text{Fin}(n)$. Define $f':\text{Fin}(n) \to X'$ thus: $f'(\nu)=\begin{cases} f(\nu) &\text{if } \nu \neq k \\ f(n) &\text{if } \nu=k \end{cases}$

• Now, firstly, this function does indeed map values into $X'$ as advertised. To see this, fix any $\nu\in\text{Fin}(n)$. If $\nu \neq k$, then by the injectivity of $f$ $X \ni f'(\nu)=f(\nu) \neq f(k)=x$ If $\nu=k$, then by injectivity again, $x=f(k) \neq f(n)=f'(\nu) \in X$ In both cases, $f'(\nu) \neq x$ and $f'(\nu) \in X$. Hence, $f'(\nu) \in X'$.

• Secondly, $f'$ is injective. For, suppose $\nu \neq \tilde{\nu}$ for $\nu,\tilde{\nu}\in\text{Fin}(n)$. If neither $\nu$ nor $\tilde{\nu}$ is $k$, then by injectivity $f'(\nu)=f(\nu) \neq f(\tilde{\nu})=f'(\tilde{\nu})$ Otherwise w.l.o.g. assume that $\tilde{\nu}=k$. Then, $\nu \neq k$ (so $f'(\nu)=f(\nu)$). Hence, by injectivity applied to $\nu \neq n$ (which happens because $\nu\in\text{Fin}(n)$) $f'(\nu)=f(\nu) \neq f(n)=f'(k)=f'(\tilde{\nu})$ Thus, in both cases, $\nu \neq \tilde{\nu}$ implies $f'(\nu) \neq f'(\tilde{\nu})$ i.e. $f'$ is injective.

• Thirdly, $f'$ is surjective. Indeed, take any $y\in X'$. Since $f$ is bijective, $f(\nu)=y$ for some $\nu\in\text{Fin}(S(n))$. Now, since $f(\nu)=y \neq x=f(k)$ (because $y\in X\setminus\{x\}$) one must have $\nu \neq k$, lest $f$ map one value to multiple values. Now, $\text{Fin}(S(n))=\text{Fin}(n)\cup\{n\}$. So, either $\nu=n$ or $\nu\in\text{Fin}(n)$. For the former, note that $k \neq \nu=n$ so that $k\in\text{Fin}(n)$. But then, one has $k\in\text{Fin}(n)$ such that $f'(k)=f(n)=f(\nu)=y$. Otherwise, for the latter, since $\nu \neq k$ by before, $f'(\nu)=f(\nu)=y$; thus, again, one has $\nu\in\text{Fin}(n)$ such that $f'(\nu)=y$.

Lemma BFSxRBFx

Bijection from $\text{Fin}(S(n))$ to Subset Restricts to Bijection from $\text{Fin}(n)$ to Subset: Fix an $n\in\mathbb{N}$. If one has a bijection $f:\text{Fin}(S(n)) \to X$ for some $X\subset\text{Fin}(S(n))$, then one has a bijection $f':\text{Fin}(n) \to X'$ for some $X'\subset\text{Fin}(n)$.

Proof: There are two cases to consider:

Suppose first that $n \notin X$: Thus, $X\subseteq\text{Fin}(n)$ by Lemma SFSxWSFx. Now choose any $x \in X$; if at a loss, choose $x=f(n)$. Then, the above lemma gives a bijection from $\text{Fin}(n)$ to $X'=X\setminus\{x\}$. Now, $X'$ is certainly a subset of $X$. Moreover, it is a strict subset of the same because $X'$ does not contain an element of $X$. Thus, it must also be a strict subset of $\text{Fin}(n)$.

Suppose next that $n \in X$: Then, the above lemma gives a bijection from $\text{Fin}(n)$ to $X'=X\setminus\{n\}$. Note that $X'$, as a subset of $X\subset\text{Fin}(S(n))$, must also be a subset of $F(S(n))$. But, as $X'$ does not contain $n$, Lemma SFSxWSFx implies that $X'\subseteq\text{Fin}(n)$. Finally, as $X$ is a strict subset of $\text{Fin}(S(n))$, some $\nu\in\text{Fin}(S(n))$ is not in $X$. This $\nu$ cannot be $n$ as it is being supposed that $n$ is in $X$. Thus, $\nu\in\text{Fin}(n)$. Also, $\nu$ cannot be in $X'$ since the latter is a subset of a set not containing $\nu$. In other words, $X'$ is missing an element $\nu$ of $\text{Fin}(n)$ despite being a subset of $\text{Fin}(n)$ i.e. $X'\subset\text{Fin}(n)$.