Proof of Sets of Maps between Finite Sets, Finite Unions of Finite Sets, 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.

Conventions for the inductions. All three clauses are proved by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction. In the formulas below, $A$, $z$ and the other lower-case letters are set variables, and $B$, $I$, $C$, $U$, $X$, $Y$ and $R$ are distinct class variables; the sets of the same names are assigned to $B$, $I$, $C$ and $U$, and $X$, $Y$ and $R$ are assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and the order $\le$ of $\mathbb{N}_{0}$; bound variables are chosen distinct from all of these. The variable $A$ is the variable of the induction: for a set $J$, $\varphi(J)$ means that $\varphi$ holds when $J$ is assigned to $A$. Let $\mathrm{fin}(z)$ be the formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §predicative for the set variable $z$; it is predicative, its free variables are among $z$, $X$, $Y$ and $R$, and it holds for a set assigned to $z$ if and only if that set is finite. A formula built from predicative formulas by connectives and by quantifiers over set variables is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative.

Adjoining a value. Let $D$ and $E$ be sets, $g:D\to E$ a map, $x\notin D$ a set and $e\in E$, and let $h=g\cup\{(x,e)\}$; it is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set and Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §binary-union, and its elements are those of $g$ and $(x,e)$, by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations and The Empty Set, the Unordered Pair and the Singleton §singleton. They are ordered pairs, $g$ being a relation by Functions, Values of a Function, and Functions from One Class to Another §function, so $h$ is a relation. Let $(u,v),(u,v')\in h$. If both lie in $g$, then $v=v'$. If $(u,v)=(x,e)$, then $u=x$ and $v=e$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; $(u,v')\in g$ would give $x\in\operatorname{dom}g=D$ by Relations, Domain, Range, Inverse and Composition §domain, so $(u,v')=(x,e)$ and $v'=e=v$; likewise if $(u,v')=(x,e)$. So $h$ is a function. By Relations, Domain, Range, Inverse and Composition §domain, Relations, Domain, Range, Inverse and Composition §range and The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, $\operatorname{dom}h=D\cup\{x\}$ and $\operatorname{ran}h=\operatorname{ran}g\cup\{e\}\subseteq E$, so $h:D\cup\{x\}\to E$ by Functions, Values of a Function, and Functions from One Class to Another §map. As $(u,g(u))\in g\subseteq h$ for $u\in D$ and $(x,e)\in h$, Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value gives $h(u)=g(u)$ for $u\in D$ and $h(x)=e$.

Maps with empty domain. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, $\mathrm{id}_{\emptyset}$ is a map $\emptyset\to\emptyset$, so $\operatorname{ran}\mathrm{id}_{\emptyset}\subseteq\emptyset\subseteq E$ and $\mathrm{id}_{\emptyset}:\emptyset\to E$ for every set $E$, by Functions, Values of a Function, and Functions from One Class to Another §map. Every map $f:\emptyset\to E$ has the domain of $\mathrm{id}_{\emptyset}$ and, vacuously, the same values, so $f=\mathrm{id}_{\emptyset}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, $E^{\emptyset}=\{\mathrm{id}_{\emptyset}\}$.

Sets of maps. Let $B$ be finite. Let $\mu(w,A,B)$ be the formula 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 with $w$, $A$, $B$ in place of $F$, $A$, $B$, and let $\theta(z,A)$ be $\forall w\,(w\in z\Leftrightarrow\mu(w,A,B))$, predicative by that clause. For every set $J$, $B^{J}$ is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §set whose elements are the maps $J\to B$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, so by 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 exactly one set $z$ satisfies $\theta(z,J)$, namely $B^{J}$. Let $\psi(z)$ be $\mathrm{fin}(z)\wedge(\neg\forall w\,(w\notin B)\Rightarrow\neg\forall w\,(w\notin z))$, predicative, and let $\varphi(A)$ be $A=A\wedge\exists z\,(\theta(z,A)\wedge\psi(z))$, with parameters $B$, $X$, $Y$ and $R$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination (with $k=1$, $A$ for $v_{1}$ and $\gamma$ the formula $A=A$), $\varphi$ is predicative and $\varphi(J)$ holds if and only if $\psi(B^{J})$, which by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §empty says: $B^{J}$ is finite, and $B^{J}\neq\emptyset$ if $B\neq\emptyset$.

Base: $B^{\emptyset}=\{\mathrm{id}_{\emptyset}\}$ by the preceding paragraph; it is nonempty, and finite by The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons §small. Step: let $D$ be finite with $\varphi(D)$, let $a\notin D$, and put $A'=D\cup\{a\}$. For $g\in B^{D}$ and $y\in B$, $g$ is a map $D\to B$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, so $g\cup\{(a,y)\}$ is a map $A'\to B$ by the paragraph on adjoining a value, that is, an element of $B^{A'}$. The union of two sets, the singleton and the ordered pair are used here as defined set symbols, properly, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-operations, Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §binary-union and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §pair; so Maps and Relations Given by Formulas §binary gives the map $\sigma:B^{D}\times B\to B^{A'}$, $\sigma(g,y)=g\cup\{(a,y)\}$. It is surjective: let $f\in B^{A'}$ and $g=f|_{D}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $g$ is a function with domain $D\cap A'=D$ and $g(u)=f(u)\in B$ for $u\in D$, so $g\in B^{D}$; also $f(a)\in B$, so $(g,f(a))\in B^{D}\times B$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. The map $h=\sigma(g,f(a))$ has domain $A'$, $h(u)=g(u)=f(u)$ for $u\in D$ and $h(a)=f(a)$, so $h=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Hence $B^{A'}$ is the image $\sigma(B^{D}\times B)$, by The Image and the Preimage of a Class under a Class §image. Since $B^{D}$ is finite by $\varphi(D)$ and $B$ is finite, $B^{D}\times B$ is finite by Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite §union, so $B^{A'}$ is finite by Images of Finite Sets Are Finite, Bounded Sets of Natural Numbers Are Finite, and Nonempty Finite Totally Ordered Sets Have Extreme Elements §image. If $B\neq\emptyset$, then $\varphi(D)$ gives some $g\in B^{D}$; with $y\in B$, $\sigma(g,y)\in B^{A'}$. So $\varphi(A')$ holds, and by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, $\varphi(J)$ holds for every finite set $J$, in particular for the set $A$ of the statement; that is, $B^{A}$ is finite, and nonempty if $B\neq\emptyset$. This proves the clause on maps.

Finite unions. Assume $C_{i}$ is finite for every $i\in I$. The family is the function $C$ with domain $I$ and values $C_{i}=C(i)$ (Indexed Families of Sets and Their Union, Intersection and Product §family); so, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, for sets $i$ and $c$, $(i,c)\in C$ if and only if $i\in I$ and $c=C_{i}$. Let $\theta'(z,A)$ be $\forall w\,(w\in z\Leftrightarrow\exists i\,(i\in A\wedge\exists c\,((i,c)\in C\wedge w\in c)))$, predicative by 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. For a set $J$, the class $U_{J}=\{w:\exists i\,(i\in J\wedge\exists c\,((i,c)\in C\wedge w\in c))\}$ consists of the elements of the sets $C_{i}$ with $i\in J\cap I$; it is a subclass of $\bigcup_{i\in I}C_{i}$ by Indexed Families of Sets and Their Union, Intersection and Product §union, 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, so $U_{J}$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass, and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms a set $z$ satisfies $\theta'(z,J)$ if and only if $z=U_{J}$. Let $\varphi'(A)$ be $A=A\wedge\exists z\,(\theta'(z,A)\wedge(A\subseteq I\Rightarrow\mathrm{fin}(z)))$, with parameters $I$, $C$, $X$, $Y$ and $R$; $A\subseteq I$ abbreviates a predicative formula by Subclasses and Subsets §subclass. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, as for $\varphi$, $\varphi'$ is predicative and $\varphi'(J)$ holds if and only if $U_{J}$ is finite or $J\not\subseteq I$.

Base: $U_{\emptyset}$ has no element, so it is $\emptyset$, finite by The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons §small. Step: let $J$ be finite with $\varphi'(J)$, let $x\notin J$, and let $J\cup\{x\}\subseteq I$. Then $J\subseteq I$, so $U_{J}$ is finite. An element lies in $U_{J\cup\{x\}}$ exactly when it lies in some $C_{i}$ with $i\in J$, that is in $U_{J}$, or in $C_{x}$; so $U_{J\cup\{x\}}=U_{J}\cup C_{x}$ by The Boolean Operations on Classes, Disjointness, and the Universal Class §operations. As $x\in I$, $C_{x}$ is finite by this assumption, and $U_{J\cup\{x\}}$ is finite by Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite §union. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, $\varphi'(I)$ holds; as $I\subseteq I$, $U_{I}$ is finite, and $U_{I}=\bigcup_{i\in I}C_{i}$ by Indexed Families of Sets and Their Union, Intersection and Product §union. This proves the clause on finite unions.

Finite choice. Assume $C_{i}\neq\emptyset$ for every $i\in I$. No choice axiom is used: each induction step picks one element of one nonempty set. Let $U=\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, and let $\varphi''(A)$ be

$$A\subseteq I\Rightarrow\exists f\,\bigl(\mu(f,A,U)\wedge\forall i\,(i\in A\Rightarrow\exists c\,((i,c)\in C\wedge\exists v\,((i,v)\in f\wedge v\in c)))\bigr),$$

with $\mu(f,A,U)$ as in 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 ($f$, $A$, $U$ in place of $F$, $A$, $B$) and parameters $I$, $C$ and $U$; it is predicative by that clause 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 §pair-membership. For a set $J\subseteq I$, $\varphi''(J)$ holds if and only if there is a map $f:J\to U$ with $f(i)\in C_{i}$ for every $i\in J$: the variable $f$ ranges over sets, which loses nothing since every map with domain $J$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §function-set; $\mu(f,J,U)$ says $f:J\to U$ by 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 for $i\in J$, $(i,c)\in C$ says $c=C_{i}$ and $(i,v)\in f$ says $v=f(i)$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value.

Base: $\mathrm{id}_{\emptyset}:\emptyset\to U$ by the paragraph on maps with empty domain, the condition on values being vacuous. Step: let $J$ be finite with $\varphi''(J)$, let $x\notin J$, and let $J\cup\{x\}\subseteq I$. Then $J\subseteq I$, so there is a map $f':J\to U$ with $f'(i)\in C_{i}$ for $i\in J$. As $x\in I$, $C_{x}\neq\emptyset$ by this assumption; let $c\in C_{x}$. Then $c\in U$ by Indexed Families of Sets and Their Union, Intersection and Product §union, and by the paragraph on adjoining a value, $f=f'\cup\{(x,c)\}$ is a map $J\cup\{x\}\to U$ with $f(i)=f'(i)\in C_{i}$ for $i\in J$ and $f(x)=c\in C_{x}$; so $\varphi''(J\cup\{x\})$ holds. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, $\varphi''(I)$ holds, and as $I\subseteq I$ it gives the required map $f:I\to\bigcup_{i\in I}C_{i}$. This proves the clause on finite choice.