Proof of Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples

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.

Removing an element. Let $B$ be a finite set and $x\in B$. The singleton $\{x\}$ is a set by The Empty Set, the Unordered Pair and the Singleton §singleton, with $x$ as its only element, and it is finite by 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 §small; $B\setminus\{x\}$ is a subset of $B$, hence finite by 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 §subset. For a set $u$: if $u\in B$, then either $u=x$, so $u\in\{x\}$, or $u\neq x$, so $u\in B\setminus\{x\}$; conversely $B\setminus\{x\}\subseteq B$ and $\{x\}\subseteq B$ as $x\in B$. Hence $B=(B\setminus\{x\})\cup\{x\}$ by extensionality, and $(B\setminus\{x\})\cap\{x\}=\emptyset$, since an element of $\{x\}$ equals $x$ and so does not lie in $B\setminus\{x\}$. By Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §union, applied to the disjoint finite sets $B\setminus\{x\}$ and $\{x\}$, and by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty, which gives $\#\{x\}=1$,

$$\#B=\#\big((B\setminus\{x\})\cup\{x\}\big)=\#(B\setminus\{x\})+\#\{x\}=\#(B\setminus\{x\})+1.$$

Injective self-maps. Let $A$ be a finite set and $f:A\to A$ injective. By Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §image, applied with $C=A$, $\#f(A)=\#A$. The image $f(A)$ is $f[A]$ by Sets and Maps: Ordinary Notation §images, and by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §injective-inverse it equals $\operatorname{ran}f$, and $\operatorname{ran}f\subseteq A$ by Functions, Values of a Function, and Functions from One Class to Another §map; so $f(A)$ is a subset of $A$ with $\#f(A)=\#A$, and Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §subset, applied to $f(A)\subseteq A$, gives $f(A)=A$. Now let $v\in A$. Then $v\in\operatorname{ran}f$, so by Relations, Domain, Range, Inverse and Composition §range there is a set $u$ with $(u,v)\in f$; then $u\in\operatorname{dom}f=A$ by Relations, Domain, Range, Inverse and Composition §domain and Functions, Values of a Function, and Functions from One Class to Another §map, and $f(u)=v$ by Functions, Values of a Function, and Functions from One Class to Another §value. Thus $f$ is surjective, and being injective it is a bijection by Injective, Surjective and Bijective Functions between Classes §bijective.

Infinite sets. First let $X$ be a set and $g:\mathbb{N}\to X$ an injective map, and suppose that $X$ is finite. By Finite Sets §finite there are $n\in\mathbb{N}_{0}$ and a bijection $\varphi$ from $[n]$ onto $X$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, $\varphi^{-1}:X\to[n]$ is bijective, in particular injective by Injective, Surjective and Bijective Functions between Classes §bijective. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[n+1]=\{k\in\mathbb{N}:k\le n+1\}$, so $[n+1]\subseteq\mathbb{N}$, and $\varphi^{-1}(g(k))\in[n]$ for every $k\in[n+1]$. Let $h:[n+1]\to[n]$ be the map $k\mapsto\varphi^{-1}(g(k))$. If $k,k'\in[n+1]$ and $h(k)=h(k')$, then $g(k)=g(k')$ as $\varphi^{-1}$ is injective, and then $k=k'$ as $g$ is injective; so $h$ is injective. By 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 §pigeonhole, applied with $m=n+1$ and the injective map $h$ from $[n+1]$ to $[n]$, we get $n+1\le n$. Since $n+1$ is the successor of $n$ 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, The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor-below, applied with $m=n$, turns $n+1\le n$ into $n<n$, and by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §strict this would give $n\neq n$, which is absurd. Hence $X$ is not finite, that is, $X$ is infinite by Finite Sets §finite.

Now $\mathbb{N}$ is a set by the setting, and the identity $\mathrm{id}_{\mathbb{N}}:\mathbb{N}\to\mathbb{N}$ is bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, hence injective by Injective, Surjective and Bijective Functions between Classes §bijective. By what was just shown, with $X=\mathbb{N}$ and $g=\mathrm{id}_{\mathbb{N}}$, $\mathbb{N}$ is infinite.

Permutations. Let $n\in\mathbb{N}_{0}$. The set $[n]$ is finite by 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 §naturals, as $[n]=\{1,\dots,n\}$ is an interval by Intervals of Natural Numbers §segment. Hence the set $[n]^{[n]}$ of maps from $[n]$ to $[n]$ is finite by 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 §maps, applied with $A=B=[n]$. By Permutations of a Set and the Set of Permutations of [n] §permutations, $S_{n}=\{\sigma\in[n]^{[n]}:\sigma\text{ is bijective}\}$ is a subset of $[n]^{[n]}$, so it is finite by 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 §subset. The identity $\mathrm{id}_{[n]}$ is a bijective map $[n]\to[n]$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity; so $\mathrm{id}_{[n]}\in[n]^{[n]}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, and therefore $\mathrm{id}_{[n]}\in S_{n}$. Thus $S_{n}$ is nonempty.

Pairs. Let $a$ and $B$ be sets. The singleton $\{a\}$ is a set whose only element is $a$, by The Empty Set, the Unordered Pair and the Singleton §singleton, and $\{a\}\times B$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. For $b\in B$, $(a,b)\in\{a\}\times B$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, as $a\in\{a\}$ and $b\in B$; let $p:B\to\{a\}\times B$ be the map $b\mapsto(a,b)$. If $b,b'\in B$ and $(a,b)=(a,b')$, then $b=b'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; so $p$ is injective. Let $q\in\{a\}\times B$. By The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction there are sets $u\in\{a\}$ and $v\in B$ with $q=(u,v)$; then $u=a$, so $q=(a,v)=p(v)$. Thus $p$ is surjective, hence a bijection from $B$ onto $\{a\}\times B$ by Injective, Surjective and Bijective Functions between Classes §bijective.

Extended tuples. Let $Y$ be a set and $n\in\mathbb{N}_{0}$. By Tuples in a Set: the Set of n-Tuples and Their Components §tuples, $Y^{n}=Y^{[n]}$ and $Y^{n+1}=Y^{[n+1]}$, and by Tuples in a Set: the Set of n-Tuples and Their Components §components the components of a tuple are its values, $v_{k}=v(k)$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, $[n+1]=[n]\cup\{n+1\}$ and $n+1\notin[n]$; in particular $[n]\subseteq[n+1]$ and $n+1\in[n+1]$. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, the elements of $Y^{[m]}$, for $m\in\mathbb{N}_{0}$, are exactly the maps $[m]\to Y$.

Existence. Let $t\in Y^{n}$ and $y\in Y$. For $k\in[n+1]$ with $k\in[n]$ the value $t(k)$ is defined and lies in $Y$, as $t:[n]\to Y$; and $y\in Y$. By Maps Defined by Cases §cases, applied with $A=[n+1]$, $B=Y$, the property $k\in[n]$, $t_{1}(k)=t(k)$ and $t_{2}(k)=y$, there is a map $u:[n+1]\to Y$ with $u(k)=t(k)$ for $k\in[n]$ and $u(k)=y$ for $k\in[n+1]\setminus[n]$. Then $u\in Y^{n+1}$, $u_{k}=t_{k}$ for $k\in[n]$, and $u_{n+1}=y$ as $n+1\in[n+1]\setminus[n]$.

Uniqueness. If $u,u'\in Y^{n+1}$ both satisfy $u_{k}=u'_{k}=t_{k}$ for $k\in[n]$ and $u_{n+1}=u'_{n+1}=y$, then $u(k)=u'(k)$ for every $k\in[n]\cup\{n+1\}=[n+1]$, and both have domain $[n+1]$; so $u=u'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Write $E(t,y)$ for this unique $u$.

The inverse map. For $v\in Y^{n+1}$, the restriction $v|_{[n]}$ is a function with domain $[n]\cap[n+1]=[n]$ and values $(v|_{[n]})(k)=v(k)$ for $k\in[n]$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction. Every element of $v|_{[n]}$ is an element of $v$ by The Restriction of a Function or Relation to a Class §restriction, so $\operatorname{ran}(v|_{[n]})\subseteq\operatorname{ran}v\subseteq Y$ by Relations, Domain, Range, Inverse and Composition §range and Functions, Values of a Function, and Functions from One Class to Another §map. Hence $v|_{[n]}:[n]\to Y$ by Functions, Values of a Function, and Functions from One Class to Another §map, that is $v|_{[n]}\in Y^{n}$; and $v(n+1)\in Y$, as $n+1\in[n+1]=\operatorname{dom}v$ and $v$ maps into $Y$. So $(v|_{[n]},v(n+1))\in Y^{n}\times Y$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, and we let $G:Y^{n+1}\to Y^{n}\times Y$ be the map $v\mapsto(v|_{[n]},v(n+1))$.

$G$ is injective: if $v,v'\in Y^{n+1}$ and $G(v)=G(v')$, then $v|_{[n]}=v'|_{[n]}$ and $v(n+1)=v'(n+1)$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; for $k\in[n]$ this gives $v(k)=(v|_{[n]})(k)=(v'|_{[n]})(k)=v'(k)$, so $v$ and $v'$ agree on $[n]\cup\{n+1\}=[n+1]$, their common domain, and $v=v'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality.

$G$ is surjective: an element of $Y^{n}\times Y$ is of the form $(t,y)$ with $t\in Y^{n}$ and $y\in Y$, by The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction. For $u=E(t,y)$, the function $u|_{[n]}$ has domain $[n]=\operatorname{dom}t$ and values $(u|_{[n]})(k)=u(k)=t(k)$ for $k\in[n]$, so $u|_{[n]}=t$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality; and $u(n+1)=y$. Thus $G(u)=(t,y)$.

So $G$ is bijective by Injective, Surjective and Bijective Functions between Classes §bijective, and by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse its inverse $H=G^{-1}:Y^{n}\times Y\to Y^{n+1}$ is bijective with $G\circ H=\mathrm{id}_{Y^{n}\times Y}$. For $t\in Y^{n}$ and $y\in Y$, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity give $G(H(t,y))=(t,y)$, that is, $H(t,y)|_{[n]}=t$ and $H(t,y)(n+1)=y$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic. Hence $H(t,y)\in Y^{n+1}$ has components $H(t,y)_{k}=(H(t,y)|_{[n]})(k)=t_{k}$ for $k\in[n]$ and $H(t,y)_{n+1}=y$, so $H(t,y)=E(t,y)$ by uniqueness. Therefore the map $(t,y)\mapsto E(t,y)$ is $H$, the only map on $Y^{n}\times Y$ with these values by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, and it is a bijection from $Y^{n}\times Y$ onto $Y^{n+1}$.