Proof of The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons

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.

Segments. For $n\in\mathbb{N}_{0}$, $[n]=\{k\in\mathbb{N}:k\le n\}$, $[0]=\emptyset$ and $[1]=\{1\}$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, so $n\in[n]$ for $n\in\mathbb{N}$, and $[n]$ is a set by Sets and Maps: Ordinary Notation §set-builder; by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, $[n+1]=[n]\cup\{n+1\}$ with $n+1\notin[n]$.

The class of the induction. The pigeonhole claim for $n\in\mathbb{N}_{0}$ is: for every $m\in\mathbb{N}_{0}$, every injective map $f:[m]\to[n]$ satisfies $m\le n$. We prove it for every $n\in\mathbb{N}_{0}$ by induction from $0$, applied to a class formed as follows. This paragraph concerns formulas of class theory: elements of $\mathbb{N}_{0}$ are assigned to set variables and read as sets only in that sense, and in the formulas below a variable to which a number is assigned occurs only to the left of $\in$ or as a component of an ordered pair. Let $z$, $z'$, $m$, $n$ and $f$ be distinct set variables and $X$, $Y$ and $R$ distinct class variables, with $X$, $Y$ and $R$ assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §segment, applied to the variables $z$, $m$ and to $z'$, $n$, there are predicative formulas $\mathrm{seg}(z,m)$ and $\mathrm{seg}(z',n)$, with free variables among $z$, $m$, $Y$, $R$, respectively $z'$, $n$, $Y$, $R$, that hold for sets $c$ and $c'$ assigned to $z$ and $z'$ and numbers $m,n\in\mathbb{N}_{0}$ if and only if $c=[m]$, respectively $c'=[n]$. Let $\mu(f,z,z')$ and $\iota(f)$ be the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §map and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §injective with $f$, $z$ and $z'$ in place of $F$, $A$ and $B$, their bound variables chosen distinct from $m$, $n$, $z$, $z'$ and $f$; they are predicative, and for sets $g$, $c$ and $c'$ both hold if and only if $g$ is an injective map $g:c\to c'$. The formula $(m,n)\in R$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership is predicative, and for sets $m$ and $n$ it holds if and only if $(m,n)\in{\le}$, that is, $m\le n$ by The Order on Omega §order. Let $\pi(n)$ be the formula

$$\forall m\,\forall z\,\forall z'\,\forall f\,\bigl((m\in X\wedge\mathrm{seg}(z,m)\wedge\mathrm{seg}(z',n)\wedge\mu(f,z,z')\wedge\iota(f))\Rightarrow(m,n)\in R\bigr).$$

Its parts are predicative, so they apply no quantifier to a class variable, and it adds only connectives and quantifiers over set variables; so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, no quantifier being applied to a class variable. By Sets and Maps: Ordinary Notation §set-builder and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction there is the class $K=\{n:\pi(n)\}$, a set $n$ lying in $K$ if and only if $\pi(n)$. By the preceding sentences, for $n\in\mathbb{N}_{0}$, $\pi(n)$ says that $m\le n$ for every $m\in\mathbb{N}_{0}$ and every injective map $[m]\to[n]$ that is a set; as every map with domain $[m]$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set, $n\in K$ if and only if the pigeonhole claim holds for $n$. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, $\mathbb{N}_{0}$ is the set $\omega$ of The Class Omega of Natural Numbers with Zero §omega, and the successor $S(n)$ of each $n\in\mathbb{N}_{0}$ is $n+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one; so by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §induction applied to $K$, it suffices to prove the claim for $n=0$ and to show that it passes from $n$ to $n+1$ for each $n\in\mathbb{N}_{0}$.

Pigeonhole. For $n=0$: let $f:[m]\to[0]$ be injective. If $m\neq0$, then $m\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets and $m\in[m]$, while $f(m)$ would lie in $[0]=\emptyset$; hence $m=0$, and $m\le0$ 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. 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\neq0$; as $\mathbb{N}_{0}$ is the set $\omega$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §cases gives $m'\in\mathbb{N}_{0}$ with $m=S(m')$, and $S(m')=m'+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, $[m]=[m']\cup\{m\}$ and $m\notin[m']$; so $m\in[m]$, and every $k\in[m']$ lies in $[m]$ and satisfies $k\neq m$. Put $b=f(m)$. The property $f(k)=n+1$ of $k\in[m']$, with parameters $f$ and $n$, is written with abbreviations and without quantifiers, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. Let $k\in[m']$. If $f(k)\neq n+1$, then $f(k)\in[n+1]=[n]\cup\{n+1\}$ gives $f(k)\in[n]$. If $f(k)=n+1$, then $b\neq n+1$ by injectivity of $f$, as $k\neq m$; so $b\in[n]$ in the same way. Hence Maps Defined by Cases §cases, applied with $[m']$, $[n]$, the constant expression $b$ and the expression $f(k)$ in place of its $A$, $B$, $t_{1}(x)$ and $t_{2}(x)$, gives a map $g:[m']\to[n]$ with $g(k)=b$ if $f(k)=n+1$ and $g(k)=f(k)$ otherwise. It is injective: let $k,k'\in[m']$ with $g(k)=g(k')$. If $f(k)\neq n+1$ and $f(k')\neq n+1$, then $f(k)=g(k)=g(k')=f(k')$; if $f(k)=n+1=f(k')$, then $f(k)=f(k')$ as well; in both cases $k=k'$ by injectivity of $f$. If $f(k)=n+1\neq f(k')$, then $f(k')=g(k')=g(k)=b=f(m)$, so $k'=m$ by injectivity of $f$, which is impossible as $k'\in[m']$ and $m\notin[m']$; the case $f(k')=n+1\neq f(k)$ is the same with $k$ and $k'$ exchanged. So $g$ is injective by Injective, Surjective and Bijective Functions between Classes §injective, 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\in\mathbb{N}_{0}$ admits a bijection from $[n]$ onto $A$. If $g:[m]\to A$ and $h:[n]\to A$ are bijections, then $h^{-1}\circ g:[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 from $[0]$ onto $\emptyset$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity. Let $x$ be a set. As $x\in\{x\}$, there is the constant map $c:[1]\to\{x\}$, $c(u)=x$, of Sets and Maps: Ordinary Notation §maps. It is injective, since $[1]=\{1\}$ has the single element $1$, and surjective, since the only element of $\{x\}$ is $x=c(1)$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §pair; so it is a bijection by Injective, Surjective and Bijective Functions between Classes §bijective. By Finite Sets §finite this proves the clause on small sets.