Proof of Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice

Inductions. Several claims below are proved for every $n\in\mathbb{N}_{0}$ in the following way: we check the claim for $n=0$ and show that it passes from $n$ to $n+1$ for each $n\in\mathbb{N}_{0}$. The class of $n\in\mathbb{N}$ for which the claim holds then contains $1=0+1$ and is closed under $n\mapsto n+1$, so it is $\mathbb{N}$ by Arithmetic and Order of the Natural Numbers §induction. Because $\mathbb{N}_{0}=\mathbb{N}\cup\{0\}$ by The Natural Numbers with Zero and Their Embedding into the Integers §naturals, the claim then holds for every $n\in\mathbb{N}_{0}$. Recall from Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment that $[n]=\{k\in\mathbb{N}:k\le n\}$ and $[0]=\emptyset$, so $n\in[n]$ for $n\in\mathbb{N}$, and from Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor that $[n+1]=[n]\cup\{n+1\}$ with $n+1\notin[n]$.

Transpositions. For a set $Y$ and $y,z\in Y$, let $\tau:Y\to Y$ be given by $\tau(y)=z$, $\tau(z)=y$ and $\tau(u)=u$ for $u\in Y\setminus\{y,z\}$. Then $\tau\circ\tau=\mathrm{id}_{Y}$, so $\tau$ is bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion.

Pigeonhole. We prove by induction on $n$ the claim: for every $m\in\mathbb{N}_{0}$, every injective map $f:[m]\to[n]$ satisfies $m\le n$. For $n=0$: if $m\neq0$, then $m\in\mathbb{N}$ and $m\in[m]$, while $f(m)$ would lie in $[0]=\emptyset$; hence $m=0$. Now assume the claim for $n$ and let $f:[m]\to[n+1]$ be injective. If $m=0$, then $m\le n+1$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §zero-least. Otherwise $m\in\mathbb{N}$, and $m=m'+1$ with $m'\in\mathbb{N}_{0}$: take $m'=0$ if $m=1$, and $m'$ from Arithmetic and Order of the Natural Numbers §predecessor if $m\neq1$. Let $\tau$ be the transposition of $[n+1]$ exchanging $f(m)$ and $n+1$, and $g=\tau\circ f$, which is injective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation and satisfies $g(m)=n+1$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, $[m]=[m']\cup\{m\}$ and $m\notin[m']$; so for $k\in[m']$ we have $k\neq m$, hence $g(k)\neq n+1$, hence $g(k)\in[n]$. Thus $k\mapsto g(k)$ is an injective map $[m']\to[n]$, the induction hypothesis gives $m'\le n$, and $m=m'+1\le n+1$. This proves the first assertion of the pigeonhole clause. If $h:[m]\to[n]$ is a bijection, then $m\le n$ because $h$ is injective, and $n\le m$ because $h^{-1}:[n]\to[m]$ is bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse; so $m=n$.

Uniqueness. Let $A$ be finite. By Finite Sets §finite some $n$ admits a bijection $[n]\to A$. If $\varphi:[m]\to A$ and $\psi:[n]\to A$ are bijections, then $\psi^{-1}\circ\varphi:[m]\to[n]$ is bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation, so $m=n$ by the pigeonhole clause. This proves the uniqueness clause.

Small sets. Since $[0]=\emptyset$, the identity $\mathrm{id}_{\emptyset}$ is a bijection $[0]\to\emptyset$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity. Since $[1]=\{1\}$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, the map $1\mapsto x$ is a bijection $[1]\to\{x\}$. By Finite Sets §finite this proves the clause on small sets.

Concatenation. Let $k,l\in\mathbb{N}_{0}$, let $C$ and $D$ be disjoint sets, and let $\varphi:[k]\to C$ and $\psi:[l]\to D$ be bijections. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split (with $1$, $k$, $l$ in place of $m$, $n$, $p$) and Intervals of Natural Numbers §segment, $[k+l]$ is the union of the disjoint sets $[k]$ and $\{k+1,\dots,k+l\}$, and by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift the map $j\mapsto j+k$ is a bijection from $[l]$ onto $\{k+1,\dots,k+l\}$, with inverse $j\mapsto j-k$. Define $\chi:[k+l]\to C\cup D$ by $\chi(j)=\varphi(j)$ for $j\le k$ and $\chi(j)=\psi(j-k)$ for $j>k$. On $[k]$ it is a bijection onto $C$, on $\{k+1,\dots,k+l\}$ a bijection onto $D$; as both the two pieces of $[k+l]$ and the sets $C$ and $D$ are disjoint, $\chi$ is a bijection onto $C\cup D$. Hence the union of two disjoint finite sets is finite.

Subsets. We prove by induction on $n$ that every subset of $[n]$ is finite. For $n=0$ the only subset of $[0]=\emptyset$ is $\emptyset$, which is finite by the clause on small sets. Assume the claim for $n$ and let $T\subseteq[n+1]$. Then $T'=T\setminus\{n+1\}\subseteq[n]$, so $T'$ is finite. If $n+1\notin T$, then $T=T'$; otherwise $T$ is the union of the disjoint finite sets $T'$ and $\{n+1\}$, finite by concatenation. Now let $A$ be finite, $\varphi:[n]\to A$ a bijection and $S\subseteq A$. The set $\varphi^{-1}(S)\subseteq[n]$ is finite; let $\chi:[k]\to\varphi^{-1}(S)$ be a bijection. The map $j\mapsto\varphi(\chi(j))$ from $[k]$ to $S$ is injective, and it is surjective because each $s\in S$ equals $\varphi(\varphi^{-1}(s))$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, with $\varphi^{-1}(s)\in\varphi^{-1}(S)$. So $S$ is finite, proving the subset clause.

Unions and products. Let $A$ and $B$ be finite. $B\setminus A$ is finite by the subset clause, and $A\cup B$ is the union of the disjoint finite sets $A$ and $B\setminus A$, so it is finite by concatenation. For the product, fix $A$ and prove by induction on $n$: for every set $B$ admitting a bijection $\psi:[n]\to B$, $A\times B$ is finite. For $n=0$, $B=\psi(\emptyset)=\emptyset$ and $A\times B=\emptyset$ is finite. Assume the claim for $n$ and let $\psi:[n+1]\to B$ be a bijection. Put $b=\psi(n+1)$ and $B'=\psi([n])$; the restriction $\psi|_{[n]}$ is a bijection $[n]\to B'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, and $B=B'\cup\{b\}$ because $[n+1]=[n]\cup\{n+1\}$. Hence $A\times B=(A\times B')\cup(A\times\{b\})$. The set $A\times B'$ is finite by the induction hypothesis; if $\varphi:[k]\to A$ is a bijection, then $j\mapsto(\varphi(j),b)$ is a bijection $[k]\to A\times\{b\}$. So $A\times B$ is finite by the first part. This proves the union clause.

Images. Let $\varphi:[n]\to A$ be a bijection and $f:A\to B$ a map. For $y\in f(A)$ the set $K_{y}=\{k\in[n]:f(\varphi(k))=y\}$ is a nonempty subset of $\mathbb{N}$, since $y=f(\varphi(k))$ for some $k$; let $g(y)$ be its least element, given by Arithmetic and Order of the Natural Numbers §well-order. Then $g:f(A)\to[n]$ satisfies $f(\varphi(g(y)))=y$, so $g$ is injective. Its image $T=g(f(A))$ is a subset of $[n]$, which is finite via $\mathrm{id}_{[n]}$, so $T$ is finite by the subset clause; let $\chi:[p]\to T$ be a bijection. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §injective-inverse, $g^{-1}:T\to f(A)$ is bijective, so $g^{-1}\circ\chi:[p]\to f(A)$ is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation. This proves the image clause.

Extreme elements. Let $\le$ be a total order on $X$. We prove by induction on $n\in\mathbb{N}$ (Arithmetic and Order of the Natural Numbers §induction) that every $S\subseteq X$ admitting a bijection $\varphi:[n]\to S$ has a greatest and a least element in the sense of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least. For $n=1$, $S=\{\varphi(1)\}$ and $\varphi(1)$ is both, by reflexivity. Assume the claim for $n\in\mathbb{N}$ and let $\varphi:[n+1]\to S$ be a bijection. As in the product step, $S=S'\cup\{s\}$ with $s=\varphi(n+1)$ and $S'=\varphi([n])$, and $\varphi|_{[n]}$ is a bijection $[n]\to S'$; so $S'$ has a greatest element $M'$ and a least element $m'$. By totality, $M'\le s$ or $s\le M'$; let $M=s$ in the first case and $M=M'$ in the second. Then $M\in S$, and $v\le M$ for $v\in S'$ by $v\le M'$ and transitivity, and for $v=s$ by the choice of $M$. So $M$ is the greatest element of $S$; the least element is obtained in the same way from $m'$. Finally, a nonempty finite $S$ admits a bijection $[n]\to S$ by Finite Sets §finite, and $n\neq0$ since $[0]=\emptyset$; so $n\in\mathbb{N}$, proving the clause on extreme elements.

Bounded sets of natural numbers. Let $S\subseteq\mathbb{N}_{0}$ and $b\in\mathbb{N}_{0}$ with $k\le b$ for every $k\in S$. By The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §zero-least, $S\subseteq\{0,\dots,b\}$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift, $k\mapsto k+1$ is a bijection from $\{0,\dots,b\}$ onto $\{1,\dots,b+1\}=[b+1]$, so its inverse is a bijection $[b+1]\to\{0,\dots,b\}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse. Thus $\{0,\dots,b\}$ is finite, and so is $S$ by the subset clause. Conversely let $S$ be finite. If $S=\emptyset$, $b=0$ serves. Otherwise, since the order of $\mathbb{N}_{0}$ is a well-order, hence total, by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §well-order and Well-Orders on a Set §well-order, $S$ has a greatest element by the clause on extreme elements, and $b=\max S$ serves. In particular an interval $\{m,\dots,n\}$ is a subset of $\mathbb{N}_{0}$ all of whose elements are at most $n$ by Intervals of Natural Numbers §interval, so it is finite. This proves the clause on bounded sets of natural numbers.

Removing one element. The three remaining clauses are proved by induction on the length of an enumeration, and their induction steps use the following. Let $n\in\mathbb{N}_{0}$, let $\psi:[n+1]\to D$ be a bijection onto a set $D$, and put $a=\psi(n+1)$ and $D'=\psi([n])$. As in the product step, $\psi|_{[n]}$ is a bijection $[n]\to D'$ and $D=D'\cup\{a\}$; moreover $a\notin D'$, since $\psi$ is injective and $n+1\notin[n]$. Also, a map with domain $\emptyset$ has no values, so by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality every map with domain $\emptyset$ equals $\mathrm{id}_{\emptyset}$, which is a map $\emptyset\to\emptyset$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity and hence a map from $\emptyset$ to any set.

Sets of maps. Fix a finite set $B$. We prove by induction on $n$, as in the paragraph on inductions (so by Arithmetic and Order of the Natural Numbers §induction), the claim: for every set $A$ admitting a bijection $\psi:[n]\to A$, the set $B^{A}$ is finite, and $B^{A}\neq\emptyset$ if $B\neq\emptyset$. For $n=0$, $A=\psi(\emptyset)=\emptyset$, so $B^{\emptyset}=\{\mathrm{id}_{\emptyset}\}$ by the preceding paragraph; it is nonempty, and finite by the clause on small sets. Assume the claim for $n$, let $\psi:[n+1]\to A$ be a bijection, and let $a=\psi(n+1)$ and $A'=\psi([n])$ as in the preceding paragraph, so that $A=A'\cup\{a\}$, $a\notin A'$, and $\psi|_{[n]}$ is a bijection $[n]\to A'$. Define $\rho:B^{A}\to B^{A'}\times B$ by $\rho(f)=(f|_{A'},f(a))$; here $f|_{A'}$ is a map $A'\to B$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction. If $\rho(f)=\rho(g)$, then $f(x)=f|_{A'}(x)=g|_{A'}(x)=g(x)$ for $x\in A'$ and $f(a)=g(a)$, so $f=g$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, as $A=A'\cup\{a\}$; thus $\rho$ is injective. By the induction hypothesis $B^{A'}$ is finite, so $B^{A'}\times B$ is finite by the union clause, and its subset $\rho(B^{A})$ is finite by the subset clause. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §injective-inverse, $\rho^{-1}$ is a bijection from $\rho(B^{A})$ onto $B^{A}$, so $B^{A}$ is finite by the image clause. If $B\neq\emptyset$, let $b\in B$, and let $g\in B^{A'}$, which exists by the induction hypothesis; the map $f:A\to B$ with $f(x)=g(x)$ for $x\in A'$ and $f(a)=b$ is well defined because $a\notin A'$, so $B^{A}\neq\emptyset$. Finally, a finite set $A$ admits a bijection from some $[n]$ onto $A$ by Finite Sets §finite. This proves the clause on sets of maps.

Finite unions. We prove by induction on $n$, as in the paragraph on inductions (so by Arithmetic and Order of the Natural Numbers §induction), the claim: for every set $I$ admitting a bijection $\psi:[n]\to I$ and every family $(C_{i})_{i\in I}$ of finite sets, $\bigcup_{i\in I}C_{i}$ is finite. For $n=0$, $I=\emptyset$, so by Indexed Families of Sets and Their Union, Intersection and Product §union the union has no element; it is $\emptyset$, which is finite by the clause on small sets. Assume the claim for $n$, let $\psi:[n+1]\to I$ be a bijection, and let $a=\psi(n+1)$ and $I'=\psi([n])$ as in the paragraph on removing one element, so that $I=I'\cup\{a\}$ and $\psi|_{[n]}$ is a bijection $[n]\to I'$. By Indexed Families of Sets and Their Union, Intersection and Product §union, an element lies in some $C_{i}$ with $i\in I$ exactly when it lies in some $C_{i}$ with $i\in I'$ or in $C_{a}$, so

$$\bigcup_{i\in I}C_{i}=\Big(\bigcup_{i\in I'}C_{i}\Big)\cup C_{a},$$

where $(C_{i})_{i\in I'}$ is the restricted family. The first set is finite by the induction hypothesis and $C_{a}$ is finite, so the union is finite by the union clause. As $I$ is finite, it admits a bijection from some $[n]$ onto $I$ by Finite Sets §finite. This proves the clause on finite unions.

Finite choice. No choice axiom is used: the map is built by induction, and each induction step fixes a single element of a single nonempty set, which is an instance of existential instantiation. We prove by induction on $n$, as in the paragraph on inductions (so by Arithmetic and Order of the Natural Numbers §induction), the claim: for every set $I$ admitting a bijection $\psi:[n]\to I$ and every family $(C_{i})_{i\in I}$ of nonempty sets, there is a map $f:I\to\bigcup_{i\in I}C_{i}$ with $f(i)\in C_{i}$ for every $i\in I$. For $n=0$, $I=\emptyset$, and $f=\mathrm{id}_{\emptyset}$ is a map from $\emptyset$ to $\bigcup_{i\in I}C_{i}$ by the paragraph on removing one element; the condition on its values is vacuous. Assume the claim for $n$, let $\psi:[n+1]\to I$ be a bijection, and let $a=\psi(n+1)$ and $I'=\psi([n])$ as in that paragraph, so that $I=I'\cup\{a\}$, $a\notin I'$, and $\psi|_{[n]}$ is a bijection $[n]\to I'$. The induction hypothesis, applied to the restricted family $(C_{i})_{i\in I'}$, gives a map $f':I'\to\bigcup_{i\in I'}C_{i}$ with $f'(i)\in C_{i}$ for every $i\in I'$. Since $C_{a}\neq\emptyset$, there is an element of $C_{a}$; let $c$ be one. Define $f$ on $I$ by $f(i)=f'(i)$ for $i\in I'$ and $f(a)=c$; this is well defined because $a\notin I'$. Then $f(i)\in C_{i}$ for every $i\in I$, so each value of $f$ lies in $\bigcup_{i\in I}C_{i}$ by Indexed Families of Sets and Their Union, Intersection and Product §union, and $f:I\to\bigcup_{i\in I}C_{i}$ is as required. As $I$ is finite, it admits a bijection from some $[n]$ onto $I$ by Finite Sets §finite. This proves the clause on finite choice.