Proof of Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term

Each result cited is universally quantified over the data in its own statement.

Preliminaries. The formulas below quantify over set variables only, so they are predicative (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure); they are read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading. A set variable other than $x_{1},\dots,x_{k}$ that occurs in none of finitely many given formulas, terms and variables, that is, is none of the given variables and occurs in none of the given formulas and terms, is called fresh for them; as many distinct fresh set variables as needed exist, since the set variables form an infinite list (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols) while $x_{1},\dots,x_{k}$ and the given formulas, terms and variables contain only finitely many variables.

Fixing variables at sets. Let $\varphi$ be a predicative formula, and let some of $x_{1},\dots,x_{k}$, the $x_{i}$ for $i$ in a list $I$ of indices, be fixed at sets $c_{i}$. Choose distinct set variables $y_{i}$, $i\in I$, fresh for $\varphi$, with values $c_{i}$, and let $\varphi[y/x]$ be $\varphi$ with each free occurrence of $x_{i}$ replaced by $y_{i}$; as no $y_{i}$ occurs in $\varphi$, no bound variable is renamed. Then $\varphi[y/x]$ is predicative, and under every assignment to its other free variables it holds if and only if $\varphi$ holds with $c_{i}$ assigned to $x_{i}$ for $i\in I$ (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §renaming, with the $x_{i}$ and $y_{i}$, $i\in I$, for its $v_{1},\dots,v_{k}$ and $y_{1},\dots,y_{k}$). So $\varphi$ with these $x_{i}$ fixed at sets is the predicative formula $\varphi[y/x]$, whose parameters are those of $\varphi$ and the $y_{i}$; this is how a formula below is read when sets are fixed for some of $x_{1},\dots,x_{k}$.

The guard. The formula $(\gamma\wedge u\in D)$ is predicative, since $\gamma$ is and $u\in D$ is atomic, and its free variables are among $x_{1},\dots,x_{k}$, $u$ and the parameters; so it is a guard for the variables $x_{1},\dots,x_{k},u$ (Conditions Expressed by a Predicative Formula, and Guards §guard).

By Conditions Expressed by a Predicative Formula, and Guards §expressed, the free variables of $\psi$ are among $x_{1},\dots,x_{k}$, $u$, $s$ and the parameters of $\gamma$, of $D$ and of $t$, and, under every assignment of sets to $x_{1},\dots,x_{k}$, $u$ and $s$, $\psi$ holds if and only if $\gamma$ holds, the set assigned to $u$ lies in $D$, and the set assigned to $s$ is the value of $t$. In particular $\exists u\,\psi$ is predicative, and its free variables other than $s$ are among $x_{1},\dots,x_{k}$ and the parameters, so the class abstraction $\{s:\exists u\,\psi\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction is formed with $x_{1},\dots,x_{k}$ and the parameters as its parameters.

Fix an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$ until the clause typed. For $a\in D$, the assignment of $a$ to $u$ with the same sets for $x_{1},\dots,x_{k}$ satisfies $\gamma\wedge u\in D$, since $u$ is not free in $\gamma$; so $t(a)$ is a set lying in $B$ by Terms and Typed Terms under a Guard §type-defined.

Clause members. With $x_{1},\dots,x_{k}$ fixed at the assigned sets, $\{s:\exists u\,\psi\}$ is the abstraction of the predicative formula $(\exists u\,\psi)[y/x]$, by the fixing of variables in the preliminaries. Let $b$ be a set. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and that fixing, $b\in\{s:\exists u\,\psi\}$ if and only if $\exists u\,\psi$ holds with $b$ assigned to $s$ and the assigned sets to $x_{1},\dots,x_{k}$, that is, by the reading of $\exists u$, if and only if there is a set $a$ such that $\psi$ holds with $a$ assigned to $u$ and $b$ to $s$. By the property of $\psi$, and since $\gamma$ holds, this is the case if and only if there is a set $a$ with $a\in D$ and $b=t(a)$. If $s'$ and $\psi'$ are another such choice, the class $\{s':\exists u\,\psi'\}$ has by the same argument the same elements, so the two classes are equal by Axiom of Extensionality for Classes.

Clause set. Choose a fresh set variable $p$ for $\gamma$, $t$, $\psi$, $u$, $s$ and $D$, and let $p=(u,s)$ 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 §pair-equality, with $p$, $u$ and $s$ for its $s$, $t_{1}$ and $t_{2}$; it is predicative, its free variables are among $p$, $u$ and $s$, and when sets are assigned to $p$, $u$ and $s$ it holds if and only if $p$ is the ordered pair of the sets assigned to $u$ and $s$. Let $\varphi$ be the formula $\exists u\,\exists s\,(p=(u,s)\wedge\psi)$; by the preliminaries it is predicative, with free variables among $p$, $x_{1},\dots,x_{k}$ and the parameters. Let $F=\{p:\varphi\}$ be the class of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, formed, as in the clause members, from the predicative formula $\varphi[y/x]$ with $x_{1},\dots,x_{k}$ fixed at the assigned sets, by the fixing of variables in the preliminaries. By that definition, that fixing, the reading, and the property of $\psi$, for every set $c$: $c\in F$ if and only if there are sets $a$ and $b$ with $c=(a,b)$, $a\in D$ and $b=t(a)$. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, for all sets $a$ and $b$ it follows that $(a,b)\in F$ if and only if $a\in D$ and $b=t(a)$.

So every element of $F$ is an ordered pair, and $F$ is a relation by Relations, Domain, Range, Inverse and Composition §relation. If $(a,b)\in F$ and $(a,b')\in F$, then $b=t(a)=b'$; so $F$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function. As $D$ is a set, the image $F[D]$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §image-set. By The Image and the Preimage of a Class under a Class §image and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, a set $b$ lies in $F[D]$ if and only if there is a set $a$ with $a\in D$ and $(a,b)\in F$, that is, if and only if $b=t(a)$ for some $a\in D$. By the clause members, $F[D]$ and $\{t:u\in D\}$ have the same elements, so they are equal by Axiom of Extensionality for Classes, and $\{t:u\in D\}$ is a set. Each of its elements is $t(a)$ for some $a\in D$, which lies in $B$ as shown before the clause members; so $\{t:u\in D\}$ is a subclass of $B$ by Subclasses and Subsets §subclass, and, being a set, a subset of $B$.

Clause finite. Let $D$ be finite, and let $F$ be the function of pairs $(a,t(a))$ of the clause set, so that $F[D]=\{t:u\in D\}$, a set $T$. For every $a\in D$, $(a,t(a))\in F$; and if $(a,b)\in F$, then $a\in D$ and $b=t(a)\in T$ by the clause members. So $\operatorname{dom}F=D$ and $\operatorname{ran}F\subseteq T$, and $F:D\to T$ is a map by Functions, Values of a Function, and Functions from One Class to Another §map, whose image $F(D)=F[D]$ is $T$. Hence $T$ is finite (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 §image, with $D$ and $T$ for its $A$ and $B$).

Clause typed. Term. Under each assignment satisfying $\gamma$, $\{t:u\in D\}$ is a class, and by the clause members its elements, hence by Axiom of Extensionality for Classes the class itself, are determined by the values $t(a)$ for $a\in D$, which are determined by the sets assigned to $x_{1},\dots,x_{k}$, the set $a$ and the values of the parameters, by Terms and Typed Terms under a Guard §term for $t$. The expression $\{t:u\in D\}$ is written with $x_{1},\dots,x_{k}$ and parameters, $u$ being bound in it. So it is a term under $\gamma$ by Terms and Typed Terms under a Guard §term.

Type defined. Under each assignment satisfying $\gamma$, $\{t:u\in D\}$ is a set and a subset of $B$ by the clause set, hence an element of $C$ by the hypothesis on $C$. This is Terms and Typed Terms under a Guard §type-defined.

Type expressed. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $\{t:u\in D\}$; bound occurrences counting, $z$ is neither $u$ nor $D$ and does not occur in $t$. Choose a fresh set variable $w$ for $\gamma$, $t$, $u$, $D$ and $z$. Then $w$ is none of $x_{1},\dots,x_{k}$, $u$ and $D$, is not free in $\gamma$ and does not occur in $t$, so, by Terms and Typed Terms under a Guard §type-expressed for $t$, there is a predicative formula $\psi_{w}$ expressing $\gamma\wedge u\in D\wedge w=t$ on $x_{1},\dots,x_{k},u$ and $w$; its free variables are among $x_{1},\dots,x_{k}$, $u$, $w$ and the parameters of $\gamma$, $D$ and $t$, so $z$ is not free in it. The pair $w$, $\psi_{w}$ is a choice of $s$, $\psi$ as in the statement. Let $\chi$ be the formula

$$\bigl(\gamma\wedge\forall w\,(w\in z\Leftrightarrow\exists u\,\psi_{w})\bigr).$$

By the preliminaries, $\chi$ is predicative, and its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and of $\{t:u\in D\}$. Consider an assignment of sets to $x_{1},\dots,x_{k}$ and $z$. If $\gamma$ fails, $\chi$ fails. If $\gamma$ holds, then, by the reading and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction with $w$ and $\psi_{w}$ for $s$ and $\psi$, $\chi$ holds if and only if every set $b$ satisfies $b\in z$ exactly when $b\in\{t:u\in D\}$, that is, by Axiom of Extensionality for Classes, if and only if $z=\{t:u\in D\}$. So $\chi$ expresses the condition $\gamma\wedge z=\{t:u\in D\}$, which is Terms and Typed Terms under a Guard §type-expressed. Hence $\{t:u\in D\}$ is a term of type $C$ under $\gamma$ by Terms and Typed Terms under a Guard §typed-term.

Clause symbol. Let $C$, $z$ and $\theta$ be as in the clause symbol; such a $\theta$ exists by Terms and Typed Terms under a Guard §type-expressed, $\{t:u\in D\}$ being a term of type $C$ under $\gamma$ by the clause typed. Under an assignment satisfying $\gamma$, the value of $\{t:u\in D\}$ is a set by the clause set, and $\theta$ holds exactly when the set assigned to $z$ is that set; so exactly one set $z$ satisfies $\theta$. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, $\{t:u\in D\}$ is then a defined set symbol with arguments $x_{1},\dots,x_{k}$ given by $\theta$, used properly wherever $\gamma$ holds.

Now let $x_{j}$ be taken as the $u$ of Maps and Relations Given by Formulas §map or of Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima §maps, and let the $x_{i}$, $i\neq j$, be fixed at sets $c_{i}$ such that $\gamma$ holds whenever an element of the set $a$ there is put for $x_{j}$. By the fixing of variables in the preliminaries, $\theta$ with these $x_{i}$ fixed is the predicative formula $\theta[y/x]$, whose free variables are among $x_{j}$, $z$ and the parameters, and which, under every assignment of sets to $x_{j}$ and $z$, holds if and only if $\theta$ holds with $c_{i}$ assigned to each $x_{i}$, $i\neq j$. So, for each element of $a$ put for $x_{j}$, $\gamma$ holds and exactly one set $z$ satisfies $\theta[y/x]$, namely the value of $\{t:u\in D\}$; that is, $\{t:u\in D\}$ is a defined set symbol with argument $x_{j}$ given by $\theta[y/x]$ and used properly at every element of $a$, as those clauses require. The first of them also requires the values to lie in a set $b$. When $C=\mathcal{P}(B)$ with $B$ a set, each value is an element of $C$ by the clause typed, and $\mathcal{P}(B)$ is a set (The Union Set and the Power Set of a Set §power); so $b=\mathcal{P}(B)$ serves.