Proof of Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms

Throughout, the parameters have their fixed values, as in Conditions Expressed by a Predicative Formula, and Guards (i). The set variables form an infinite list (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i)), so as many distinct set variables as needed can be chosen outside any finitely many given formulas, terms and variables. Every formula formed below applies no quantifier to a class variable, ordered pairs in it being 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 (iii), so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). In (i), (iii) and (v), once the map is obtained, the term is a value of a map at a term: if $F:A\times B\to C$ is a map, the value of a parameter, and $s$ and $t$ are terms of types $A$ and $B$ under $\gamma$, then $(s,t)$ is a term of type $A\times B$ under $\gamma$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), and $F(s,t)$ is a term of type $C$ under $\gamma$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), whose value is the value of $F$ at the pair of the values of $s$ and $t$. We refer to this as (V).

Proof of (i). The classes $T^{S}$, $\mathcal{P}(T)$ and $\mathcal{P}(S)$ are sets by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii) and The Union Set and the Power Set of a Set (ii). Let $f\in T^{S}$ and $V\in\mathcal{P}(T)$; then $f$ is a map $S\to T$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i). By Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i), applied to the map $f$ with a set variable $f$ for its variable $u$, the expression $f^{-1}(V)$ is a defined set symbol with the arguments $f$ and $V$, given by the formula $\pi$ there and used properly at every such $f$ and every set $V$, and $f^{-1}(V)$ is a subset of $S$, hence an element of $\mathcal{P}(S)$ by The Union Set and the Power Set of a Set (ii). So Maps and Relations Given by Formulas (ii), with $\mathcal{P}(S)$, $T^{S}$ and $\mathcal{P}(T)$ for its $b$, $c$ and $d$ and the expression $f^{-1}(V)$, gives exactly one map $\mathrm{pre}_{S,T}$ as stated. By (V), $u^{-1}(B)=\mathrm{pre}_{S,T}(u,B)$ is a term of type $\mathcal{P}(S)$ under $\gamma$, with the value $f^{-1}(V)$ for the values $f$ of $u$ and $V$ of $B$.

Proof of (ii). The guard. Let $y$ be a set variable that is none of $x_{1},\dots,x_{k}$ and $i$, is not free in $\gamma$ and does not occur in $I$. By Terms and Typed Terms under a Guard (iv) a predicative formula $\psi_{I}$ expresses $\gamma\wedge y=I$; by Conditions Expressed by a Predicative Formula, and Guards (ii) its free variables are among $x_{1},\dots,x_{k}$, $y$ and the parameters of $\gamma$ and $I$, so $i$ is not free in it. The formula $\exists y\,(\psi_{I}\wedge i\in y)$ is predicative, its free variables are among $x_{1},\dots,x_{k}$, $i$ and the parameters of $\gamma$ and $I$, and under an assignment of sets to $x_{1},\dots,x_{k}$ and $i$ it holds if and only if $\gamma$ holds and the set assigned to $i$ lies in the value of $I$, by Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i). So it is a guard expressing $\gamma\wedge i\in I$.

A formula for $t$. Let $w$ and $v$ be distinct set variables that are none of $x_{1},\dots,x_{k}$ and $i$ and occur in none of $\gamma$, $\gamma'$, $I$ and $t$. By Terms and Typed Terms under a Guard (iv), for the variables $x_{1},\dots,x_{k},i$ and the guard $\gamma'$, a predicative formula $\varphi$ expresses $\gamma'\wedge w=t$; its free variables are among $x_{1},\dots,x_{k}$, $i$, $w$ and the parameters of $\gamma'$ and $t$, by Conditions Expressed by a Predicative Formula, and Guards (ii), and the parameters of $\gamma'$ are among those of $\gamma$ and $I$. Fix an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$. For all sets $a$ and $b$, with $a$ assigned to $i$ and $b$ to $w$, and whatever further sets are assigned to variables not free in $\varphi$ (Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i)), $\varphi$ holds if and only if $\gamma'$ holds and $b=t(a)$, that is, as $\gamma'$ expresses $\gamma\wedge i\in I$, if and only if $a\in I$ and $b=t(a)$. We refer to this as (1).

Values. Under that assignment the value $I$ is a set, a subset of $Z$, by Terms and Typed Terms under a Guard (iii) and The Union Set and the Power Set of a Set (ii), and for $a\in I$ the assignment of $a$ to $i$ satisfies $\gamma'$, so $t(a)$ is a set in $\mathcal{P}(X)$, a subset of $X$. By (1), the class of the sets lying in $t(a)$ for some $a\in I$ is the class $U=\{v:\exists i\,\exists w\,(\varphi\wedge v\in w)\}$, and, when $I\neq\emptyset$, the class of the sets lying in $t(a)$ for every $a\in I$ is $N=\{v:\forall i\,\forall w\,(\varphi\Rightarrow v\in w)\}$, both formed by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) with $x_{1},\dots,x_{k}$ at their sets. These classes are determined by the sets assigned to $x_{1},\dots,x_{k}$ and the values of the parameters, so the expression $\bigcup_{i\in I}t$ with the value $U$, and, when the value of $I$ is nonempty under every assignment satisfying $\gamma$, the expression $\bigcap_{i\in I}t$ with the value $N$, are terms under $\gamma$ (Terms and Typed Terms under a Guard (i)); these are the terms of the clause. Each element of $U$ lies in some $t(a)\subseteq X$, and, if $a_{0}\in I$, each element of $N$ lies in $t(a_{0})\subseteq X$; so $U$, and $N$ when $I\neq\emptyset$, are subclasses of $X$, hence sets 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 (i), and elements of $\mathcal{P}(X)$ by The Union Set and the Power Set of a Set (ii). So Terms and Typed Terms under a Guard (iii) holds for both terms. For a family $(A_{a})_{a\in I}$ with $A_{a}=t(a)$, $U$ and $N$ have the same elements as $\bigcup_{a\in I}A_{a}$ and $\bigcap_{a\in I}A_{a}$ by Indexed Families of Sets and Their Union, Intersection and Product (ii) and Indexed Families of Sets and Their Union, Intersection and Product (iii), so they are these classes by Axiom of Extensionality for Classes.

The formulas. 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 $\bigcup_{i\in I}t$, respectively $\bigcap_{i\in I}t$; so $z$ is not $i$ and occurs neither in $I$ nor in $t$, and we may choose $w$ and $v$ above other than $z$. Then $z$ is not free in $\gamma'$, which expresses a condition whose parameters are those of $\gamma$ and $I$, nor in $\varphi$. Let $\psi_{\cup}$ be $\gamma\wedge\forall v\,\bigl(v\in z\Leftrightarrow\exists i\,\exists w\,(\varphi\wedge v\in w)\bigr)$ and $\psi_{\cap}$ be $\gamma\wedge\forall v\,\bigl(v\in z\Leftrightarrow\forall i\,\forall w\,(\varphi\Rightarrow v\in w)\bigr)$. They are predicative, and their free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$, $I$ and $t$. Under an assignment of sets to $x_{1},\dots,x_{k}$ and $z$, if $\gamma$ fails both fail; if $\gamma$ holds, then by (1) $\psi_{\cup}$ holds if and only if $z$ has the same elements as $U$, and, when $I\neq\emptyset$, $\psi_{\cap}$ holds if and only if $z$ has the same elements as $N$, that is, by Axiom of Extensionality for Classes, if and only if $z$ is the value of $\bigcup_{i\in I}t$, respectively $\bigcap_{i\in I}t$. So $\psi_{\cup}$ expresses $\gamma\wedge z=\bigcup_{i\in I}t$, and, when the value of $I$ is nonempty under every assignment satisfying $\gamma$, $\psi_{\cap}$ expresses $\gamma\wedge z=\bigcap_{i\in I}t$. By Terms and Typed Terms under a Guard (ii), both terms are of type $\mathcal{P}(X)$ under $\gamma$, the second under that hypothesis.

Proof of (iii). $\mathcal{P}(X)$ is a set by The Union Set and the Power Set of a Set (ii). For sets $v$ and $w$, $v\cup w$, $v\cap w$ and $v\setminus w$ are sets by Sets and Maps: Ordinary Notation (iv), and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ix) each is the only set $z$ satisfying the predicative formula given there; so they are defined set symbols with the arguments $v$ and $w$, used properly at all sets $v$ and $w$. For $v,w\in\mathcal{P}(X)$, $v$ and $w$ are subsets of $X$ by The Union Set and the Power Set of a Set (ii), and by The Boolean Operations on Classes, Disjointness, and the Universal Class (i) each element of $v\cup w$, $v\cap w$ or $v\setminus w$ lies in $v$ or in $w$, hence in $X$; so these sets lie in $\mathcal{P}(X)$. By Maps and Relations Given by Formulas (ii), with $\mathcal{P}(X)$ for its $b$, $c$ and $d$, there is exactly one map $\cup_{X}$, $\cap_{X}$, respectively $\setminus_{X}$, as stated. By (V), $A\cup B$, $A\cap B$ and $A\setminus B$ are terms of type $\mathcal{P}(X)$ under $\gamma$, with the values stated.

Proof of (iv). By Order and Suprema in the Extended Real Line (i), $\le$ is a total order on the set $[-\infty,\infty]$, hence a partial order by Partial and Total Orders on a Set and the Associated Strict Relation (ii). Every $e\in\mathcal{P}([-\infty,\infty])$ is a subset of $[-\infty,\infty]$ by The Union Set and the Power Set of a Set (ii), and it has a supremum and an infimum in $[-\infty,\infty]$ by Order and Suprema in the Extended Real Line (iii). So Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (iii), with $[-\infty,\infty]$ and $\le$ for its $p$ and $\preceq$, $\mathcal{P}([-\infty,\infty])$ for its $a$ and the variable $u$ itself for its expression $t(u)$, gives exactly one map $\mathrm{Sup}$ and exactly one map $\mathrm{Inf}$ as stated. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), $\mathrm{Sup}(E)$ and $\mathrm{Inf}(E)$ are terms of type $[-\infty,\infty]$ under $\gamma$. For the image: every subset of $B$ is a subset of $[-\infty,\infty]$, hence an element of $\mathcal{P}([-\infty,\infty])$ by The Union Set and the Power Set of a Set (ii), so Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term (iv) applies with $\mathcal{P}([-\infty,\infty])$ for its $C$.

Proof of (v). $C$ and $C'$ are sets 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 (i), so $C^{X}$ is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), and $\mathcal{P}(X)$ is a set. Let $X$ and $L$ also denote class variables whose values are $X$ and the order $\le$ of $[-\infty,\infty]$, a set by The Extended Real Line, Its Order, and [0,∞] (iii). By The Extended Real Line, Its Order, and [0,∞] (iii), for $p,q\in[-\infty,\infty]$: $q\ge p$ means $(p,q)\in{\le}$; $q>p$ means $(p,q)\in{\le}$ and $q\neq p$; $q\le p$ means $(q,p)\in{\le}$; and $q<p$ means $(q,p)\in{\le}$ and $q\neq p$. Let $f$, $c$, $z$, $w$ and $v$ be distinct set variables, and let $\beta(v,c)$ be the corresponding one of the formulas $(c,v)\in L\wedge\neg\,v=c$, $(c,v)\in L$, $(v,c)\in L\wedge\neg\,v=c$ and $(v,c)\in L$, for $>$, $\ge$, $<$ and $\le$ respectively; for $q,c\in[-\infty,\infty]$, $\beta(q,c)$ holds if and only if $q>c$, $q\ge c$, $q<c$, respectively $q\le c$. Let $\theta(z,f,c)$ be the formula $\forall w\,\bigl(w\in z\Leftrightarrow(w\in X\wedge\exists v\,((w,v)\in f\wedge\beta(v,c)))\bigr)$. Let $f\in C^{X}$ and $c\in C'$; $f$ is a map $X\to C$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), so $f(x)\in[-\infty,\infty]$ for $x\in X$. The class $\{x\in X:\beta(f(x),c)\}$, which is the set $\{x\in X:f(x)>c\}$, $\{x\in X:f(x)\ge c\}$, $\{x\in X:f(x)<c\}$, respectively $\{x\in X:f(x)\le c\}$, is a subset of $X$ and a set by Sets and Maps: Ordinary Notation (iii), so an element of $\mathcal{P}(X)$. For $w\in X=\operatorname{dom}f$, $\exists v\,((w,v)\in f\wedge\beta(v,c))$ holds if and only if $\beta(f(w),c)$, by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i). So $\theta(z,f,c)$ holds if and only if $z$ has the same elements as that set, that is, by Axiom of Extensionality for Classes, if and only if $z$ is that set. Hence that set is a defined set symbol with the arguments $f$ and $c$, given by $\theta$ and used properly at all $f\in C^{X}$ and $c\in C'$, and Maps and Relations Given by Formulas (ii), with $\mathcal{P}(X)$, $C^{X}$ and $C'$ for its $b$, $c$ and $d$, gives exactly one map $\Lambda_{>}$, $\Lambda_{\ge}$, $\Lambda_{<}$, respectively $\Lambda_{\le}$, as stated. By (V), each of the four terms is of type $\mathcal{P}(X)$ under $\gamma$. The last sentence of the clause holds as $[0,\infty]\subseteq[-\infty,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii), $\mathbb{Q}\subseteq\mathbb{R}$ under The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v), and $\mathbb{R}\subseteq[-\infty,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii), together with Order and Suprema in the Extended Real Line (i).

Proof of (vi). Let $w$ be a set variable that is none of $x_{1},\dots,x_{k}$ and $i$, is not free in $\gamma$ and does not occur in $t$. By Terms and Typed Terms under a Guard (iv), for the variables $x_{1},\dots,x_{k},i$ and the guard $\gamma\wedge i\in D$, a predicative formula $\varphi$ expresses $\gamma\wedge i\in D\wedge w=t$; its free variables are among $x_{1},\dots,x_{k}$, $i$, $w$, $D$ and the parameters of $\gamma$ and $t$. Fix an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$. For all sets $a$ and $b$, with $a$ assigned to $i$ and $b$ to $w$, and whatever sets are assigned to variables not free in $\varphi$ (Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i)), $\varphi$ holds if and only if $a\in D$ and $b=t(a)$. We refer to this as (2).

The map. By (2), with $x_{1},\dots,x_{k}$ taken as parameters at their sets, for every $a\in D$ exactly one set $b$ satisfies $\varphi$, namely $t(a)$, which lies in $C$ by Terms and Typed Terms under a Guard (iii). So $t(i)$ is a defined set symbol with the argument $i$, given by $\varphi$ and used properly at every $i\in D$, and Maps and Relations Given by Formulas (i), with $D$ and $C$ for its $a$ and $b$, gives exactly one map $h:D\to C$ with $h(a)=t(a)$ for every $a\in D$. It lies in $C^{D}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), so Terms and Typed Terms under a Guard (iii) holds for $(i\mapsto t)$ and $C^{D}$.

The formula. 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 $(i\mapsto t)$; so $z$ is not $i$ and does not occur in $t$, and we may choose $w$ other than $z$, so that $z$ is not free in $\varphi$. Let $\mu(z,D,C)$ 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 (vii) with $z$, $D$ and $C$ for its $F$, $A$ and $B$, its bound variables chosen outside the variables above, and let $\psi$ be

$$\gamma\wedge\mu(z,D,C)\wedge\forall i\,\bigl(i\in D\Rightarrow\exists w\,(\varphi\wedge(i,w)\in z)\bigr).$$

It is predicative, and its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $(i\mapsto t)$. Under an assignment of sets to $x_{1},\dots,x_{k}$ and $z$: if $\gamma$ fails, $\psi$ fails. If $\gamma$ holds, then 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 (vii) and (2), $\psi$ holds if and only if $z$ is a map $D\to C$ with $(a,t(a))\in z$ for every $a\in D$, that is, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), a map $D\to C$ with $z(a)=t(a)$ for every $a\in D$; by the uniqueness of $h$, if and only if $z=h$. So $\psi$ expresses $\gamma\wedge z=(i\mapsto t)$, Terms and Typed Terms under a Guard (iv) holds, and $(i\mapsto t)$ is a term of type $C^{D}$ under $\gamma$ by Terms and Typed Terms under a Guard (ii).