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

This helper adopts the setting of Sets and Maps: Ordinary Notation; it is a statement of the metatheory about formulas and expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters and assignments be as in Conditions Expressed by a Predicative Formula, and Guards §data, terms under a guard and their values as in Terms and Typed Terms under a Guard §term, terms of a type, and conditions expressed by a predicative formula.

Let $\gamma$ be a guard, let $u$ be a set variable that is none of $x_{1},\dots,x_{k}$ and is not free in $\gamma$, and let $D$ be a variable other than $x_{1},\dots,x_{k}$ and $u$ whose value is a set. Let $B$ be a class and let $t$ be a term of type $B$ under the guard $\gamma\wedge u\in D$, for the variables $x_{1},\dots,x_{k},u$. Under an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$ and for $a\in D$, $t(a)$ denotes the value of $t$ when $a$ is assigned to $u$ and $x_{1},\dots,x_{k}$ keep their sets.

Let $s$ be a set variable that is none of $x_{1},\dots,x_{k}$, $u$ and $D$, is not free in $\gamma$ and does not occur in $t$, and let $\psi$ be a predicative formula expressing the condition $\gamma\wedge u\in D\wedge s=t$ on $x_{1},\dots,x_{k},u$ and the displayed set variable $s$, as Terms and Typed Terms under a Guard §type-expressed provides.

¶ Under each assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, the image $\{t:u\in D\}$ is the class $\{s:\exists u\,\psi\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, in which $x_{1},\dots,x_{k}$ have the assigned sets as values. For every set $b$: $b\in\{t:u\in D\}$ if and only if $b=t(a)$ for some $a\in D$. In particular, the class $\{t:u\in D\}$ does not depend on the choice of $s$ and $\psi$.

¶ Under each assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, $\{t:u\in D\}$ is a set and a subset of $B$.

¶ If the value of $D$ is a finite set, then under each assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, $\{t:u\in D\}$ is finite.

¶ Let $C$ be a class of which every subset of $B$ is an element; for instance, when $B$ is a set, its power set $\mathcal{P}(B)$. Then $\{t:u\in D\}$, the term under $\gamma$ whose value under each assignment satisfying $\gamma$ is the class above, is a term of type $C$ under $\gamma$. Here bound occurrences count: a set variable $z$ does not occur in $\{t:u\in D\}$ when $z$ is not $u$, is not $D$, and does not occur in $t$, bound or free.

¶ Let $C$ be as in the clause typed, 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, and let $\theta$ be a predicative formula expressing the condition $\gamma\wedge z=\{t:u\in D\}$. Under every assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, exactly one set $z$ satisfies $\theta$; so $\{t:u\in D\}$ is a defined set symbol with arguments $x_{1},\dots,x_{k}$, given by $\theta$ and used properly where $\gamma$ holds. It may stand as the expression written $t(u)$ in Maps and Relations Given by Formulas §map and in Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima §maps in the following way. One of $x_{1},\dots,x_{k}$, say $x_{j}$, is taken as the $u$ there; the other variables $x_{i}$, $i\neq j$, are parameters fixed at sets for which $\gamma$ holds whenever an element of the set $a$ there is put for $x_{j}$; and, for the first of the two clauses, this is provided the values lie in a set $b$, which holds for $C=\mathcal{P}(B)$ when $B$ is a set, with $b=\mathcal{P}(B)$.