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

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Inductions. Several claims below are proved for every $n\in\mathbb{N}_{0}$ by induction from $0$ on $\mathbb{N}_{0}$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction: we check the claim for $n=0$ and show that it passes from $n$ to $n+1$ for each $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\}$; this map is obtained by applying Maps Defined by Cases §cases twice, first to get $\sigma:Y\to Y$ with $\sigma(u)=y$ for $u=z$ and $\sigma(u)=u$ for the other $u\in Y$, then to get $\tau$ with $\tau(u)=z$ for $u=y$ and $\tau(u)=\sigma(u)$ for the other $u\in Y$, all these values lying in $Y$ because $y,z\in Y$ (if $y=z$, then $\tau(z)=z=y$). Then $\tau(\tau(y))=\tau(z)=y$, $\tau(\tau(z))=\tau(y)=z$, and $\tau(\tau(u))=\tau(u)=u$ for every $u\in Y\setminus\{y,z\}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $\tau\circ\tau$ is a map $Y\to Y$ with $(\tau\circ\tau)(u)=\tau(\tau(u))$, so $(\tau\circ\tau)(u)=u=\mathrm{id}_{Y}(u)$ for every $u\in Y$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity; both maps have domain $Y$, so $\tau\circ\tau=\mathrm{id}_{Y}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Hence $\tau$ is bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion, applied with $\tau$ in place of both $F$ and $G$.

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$; its hypothesis $1\le k+1$ holds, as $0\le k$ gives $1=0+1\le k+1$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws) 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 $\{1+k,\dots,l+k\}$, which is $\{k+1,\dots,k+l\}$ by commutativity of addition; let $\theta$ be its inverse, a bijection from $\{k+1,\dots,k+l\}$ onto $[l]$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse. Define $\chi:[k+l]\to C\cup D$ by $\chi(j)=\varphi(j)$ for $j\le k$ and $\chi(j)=\psi(\theta(j))$ for the other $j\in[k+l]$, a map by Maps Defined by Cases §cases with $P(j)$ the property $j\le k$: if $j\le k$, then $j\in[k]$ and $\varphi(j)\in C$; otherwise $j\notin[k]$, so $j\in\{k+1,\dots,k+l\}$ and $\psi(\theta(j))\in D$. On $[k]$ it is $\varphi$, a bijection onto $C$, and on $\{k+1,\dots,k+l\}$ it is $\psi\circ\theta$, a bijection onto $D$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation; 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 from $1$ on $n\in\mathbb{N}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §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 The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §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; let $f:A\to B$ be the map with $f(x)=g(x)$ for $x\in A'$ and $f(x)=b$ for the other $x\in A$, given by Maps Defined by Cases §cases with $P(x)$ the property $x\in A'$, both values lying in $B$; as $A=A'\cup\{a\}$ and $a\notin A'$, $f(a)=b$. 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. Here and in the paragraph on finite choice, for every set $J$ and every family $(C_{i})_{i\in J}$ of sets, in particular for the restricted families below, the union $\bigcup_{i\in J}C_{i}$ is a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets §union. We prove by induction on $n$, as in the paragraph on inductions (so by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §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, the set $\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 The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §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}$ into the set $\bigcup_{i\in I}C_{i}$ of The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets §union 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'$ from $I'$ to the set $\bigcup_{i\in I'}C_{i}$, a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets §union, 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. Let $f:I\to\bigcup_{i\in I}C_{i}$ be the map with $f(i)=f'(i)$ for $i\in I'$ and $f(i)=c$ for the other $i\in I$, given by Maps Defined by Cases §cases with $P(i)$ the property $i\in I'$: both values lie in $\bigcup_{i\in I}C_{i}$ by Indexed Families of Sets and Their Union, Intersection and Product §union, since $f'(i)\in C_{i}$ for $i\in I'$ and $c\in C_{a}$. As $I=I'\cup\{a\}$ and $a\notin I'$, $f(a)=c$. Then $f(i)\in C_{i}$ for every $i\in I$, 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.