Proof of Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite

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.

Inserting an element. Let $A$ be finite and $x$ a set. If $x\in A$, then $A\cup\{x\}=A$ is finite. Otherwise, by Finite Sets §finite there are $n\in\mathbb{N}_{0}$ and a bijection $g:[n]\to A$, and 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]$. By Maps Defined by Cases §cases, with $P(k)$ the property $k\in[n]$ (a predicative formula with the set $[n]$ as parameter), there is a map $h:[n+1]\to A\cup\{x\}$ with $h(k)=g(k)$ for $k\in[n]$ and $h(k)=x$ for the other $k\in[n+1]$, that is, for $k=n+1$; both values lie in $A\cup\{x\}$, as $g(k)\in A$. The map $h$ is injective: distinct $k,l\in[n]$ have $g(k)\neq g(l)$ as $g$ is injective, and $h(k)\in A$ differs from $h(n+1)=x\notin A$ for $k\in[n]$. It is surjective: an element of $A$ is $g(k)=h(k)$ for some $k\in[n]\subseteq[n+1]$, and $x=h(n+1)$. So $h$ is a bijection from $[n+1]$ onto $A\cup\{x\}$, which is therefore finite by Finite Sets §finite. This proves the clause insert.

Formulas. The other clauses are proved by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, applied to predicative formulas $\varphi$ in which its set variable $A$ is free. Inside formulas, $A$ is that variable; the sets $A$ and $B$ of the statement enter only as values, outside formulas. The letters $d$, $s$, $u$, $v$, $w$ and $z$ denote set variables, distinct from each other and from $A$, and $X$, $Y$ and $R$ distinct class variables, assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$ throughout. For $t$ equal to $s$ or $z$, $\mathrm{fin}(t)$ is the formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §predicative with $t$ as its set variable; it is predicative, its free variables are among $t$, $X$, $Y$ and $R$, and it holds if and only if the value of $t$ is finite. If $\theta(z,A,d)$ is predicative and, for all sets $A$ and $d$, exactly one set $z$ satisfies it, call that set $\tau(A,d)$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination with $k=1$, $v_{1}=A$, $\gamma$ the formula $A=A$ and $\mathrm{fin}(z)$ as the formula there called $\varphi$, the formula $A=A\wedge\exists z\,(\theta\wedge\mathrm{fin}(z))$ is predicative, and for every set $C$ and every value of $d$ it holds at $C$ if and only if $\tau(C,d)$ is finite.

Subsets. Let $\varphi(A)$ be $\forall s\,(s\subseteq A\Rightarrow\mathrm{fin}(s))$, where $s\subseteq A$ abbreviates the formula $\forall u\,(u\in s\Rightarrow u\in A)$ of Subclasses and Subsets §subclass. It is predicative, since $\mathrm{fin}(s)$ is and the quantifiers added bind set variables; for a set $C$, $\varphi(C)$ says that every subset of $C$ is finite. A subset of $\emptyset$ has no element, so it is $\emptyset$, which is finite by The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons §small; so $\varphi(\emptyset)$ holds. Let $C$ be finite with $\varphi(C)$, let $x\notin C$, and let $S\subseteq C\cup\{x\}$. Then $S\setminus\{x\}\subseteq C$ is finite by $\varphi(C)$. If $x\notin S$, then $S=S\setminus\{x\}$; otherwise $S=(S\setminus\{x\})\cup\{x\}$, finite by the clause insert. So $\varphi(C\cup\{x\})$ holds, and Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction gives $\varphi(C)$ for every finite set $C$. Taking $C$ to be the finite set $A$ of the clause, this proves the clause subset.

Unions. Let $\theta(z,A,d)$ be $\forall w\,(w\in z\Leftrightarrow(w\in A\vee w\in d))$; it is predicative, as it quantifies a set variable only, and for all sets $A$ and $d$ the set $A\cup d$ is the only set $z$ satisfying it, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-operations. Let $\varphi(A)$ be the formula $A=A\wedge\exists z\,(\theta\wedge\mathrm{fin}(z))$ of the paragraph on formulas, and let $B$ be finite, assigned to $d$; so $\varphi(C)$ holds if and only if $C\cup B$ is finite. Then $\varphi(\emptyset)$ holds, as $\emptyset\cup B=B$. If $C$ is finite with $\varphi(C)$ and $x\notin C$, then $(C\cup\{x\})\cup B=(C\cup B)\cup\{x\}$ is finite by the clause insert. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, $C\cup B$ is finite for every finite set $C$; taking $C$ to be the finite set $A$ of the clause, $A\cup B$ is finite.

Products. Let $B$ be finite, with $n\in\mathbb{N}_{0}$ and a bijection $g:[n]\to B$ as in Finite Sets §finite, and let $x$ be a set. For $k\in[n]$, $(x,g(k))\in\{x\}\times B$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, so by Sets and Maps: Ordinary Notation §maps there is the map $h:[n]\to\{x\}\times B$, $k\mapsto(x,g(k))$. It is injective: if $(x,g(k))=(x,g(l))$, then $g(k)=g(l)$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, so $k=l$ as $g$ is injective. It is surjective: by The Cartesian Product of Two Classes §product, an element of $\{x\}\times B$ is a pair $(u,v)$ with $u\in\{x\}$, so $u=x$, and $v\in B$, so $v=g(k)$ for some $k\in[n]$. Hence $\{x\}\times B$ is finite by Finite Sets §finite. Now let $\theta'(z,A,d)$ be $\forall w\,(w\in z\Leftrightarrow\exists u\,\exists v\,(u\in A\wedge v\in d\wedge w=(u,v)))$, predicative since $w=(u,v)$ is 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-equality and only set variables are quantified. For all sets $A$ and $d$, $A\times d$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms, applied to the class abstraction of The Cartesian Product of Two Classes §product, it is the only set $z$ satisfying $\theta'$. Let $\chi(A)$ be the formula $A=A\wedge\exists z\,(\theta'\wedge\mathrm{fin}(z))$ of the paragraph on formulas, with $B$ assigned to $d$; so $\chi(C)$ holds if and only if $C\times B$ is finite. The set $\emptyset\times B$ has no element by The Cartesian Product of Two Classes §product, 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. If $C$ is finite with $\chi(C)$ and $x\notin C$, then by The Cartesian Product of Two Classes §product and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership both $(C\cup\{x\})\times B$ and $(C\times B)\cup(\{x\}\times B)$ consist of the pairs $(u,v)$ with $u\in C$ or $u=x$, and $v\in B$; so they are equal, and finite by the paragraph on unions, as $\{x\}\times B$ is finite. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, $C\times B$ is finite for every finite set $C$; taking $C$ to be the finite set $A$ of the clause, $A\times B$ is finite. With the paragraph on unions, this proves the clause union.