Proof of Unions and Intersections over a Countable Index Term of Terms with Values in a σ-Algebra Are Again Such Terms

We prove (i) and (ii) together; let $W$ be $U$, respectively $V$, and let $\bigodot$ stand for $\bigcup$, respectively $\bigcap$. In the case of (ii) the value of $I$ is nonempty under every assignment satisfying $\gamma$, as supposed there. By Terms and Typed Terms under a Guard (ii), we must show Terms and Typed Terms under a Guard (iii) and Terms and Typed Terms under a Guard (iv) for $W$ and the class $\mathcal{F}$.

The term $t$ has type $\mathcal{P}(X)$. By σ-Algebra and Measurable Space (i), $\mathcal{F}\subseteq\mathcal{P}(X)$. So the value of $t$ under every assignment satisfying $\gamma'$, a set lying in $\mathcal{F}$, lies in $\mathcal{P}(X)$; and Terms and Typed Terms under a Guard (iv) for $t$ does not involve the class. Hence $t$ is a term of type $\mathcal{P}(X)$ under $\gamma'$, and Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii) applies to $X$, $Z$, $I$, $i$, $\gamma'$ and $t$: the term $\bigodot_{i\in I}t$ under $\gamma$, written with $I$, $i$ and $t$, $i$ bound in it, is a term of type $\mathcal{P}(X)$ under $\gamma$, and under each assignment satisfying $\gamma$ its value is the class described in (i), respectively (ii), that is, the value of $W$.

The defining condition is predicative. 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 $W$. Let $z'$ be a set variable distinct from $z$, $i$, $x_{1},\dots,x_{k}$ and occurring in none of $\gamma$, $I$, $t$, $W$. By the preceding paragraph and Terms and Typed Terms under a Guard (iv) for $\bigodot_{i\in I}t$, there is a predicative formula $\psi'$ expressing the condition $\gamma\wedge z'=\bigodot_{i\in I}t$; its free variables are among $x_{1},\dots,x_{k}$, $z'$ and the parameters of $\gamma$, $I$ and $t$. The variable $z$ is not free in $\psi'$: it is none of $x_{1},\dots,x_{k}$ and not $z'$, it is not free in $\gamma$, and it is no parameter of $I$ or of $t$, since every such parameter is a parameter of $W$ and $z$ does not occur in $W$. Let $\psi$ be the formula $\exists z'\,(z'=z\wedge\psi')$. It is predicative, its quantifier binding a set variable (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $W$, and under every assignment it holds if and only if $\gamma$ holds and $z$ is the value of $\bigodot_{i\in I}t$, that is, the value of $W$. So $\psi$ expresses the condition $\gamma\wedge z=W$, which is Terms and Typed Terms under a Guard (iv) for $W$.

A map from $Z$ to $\mathcal{F}$. Let $\gamma''$ be the formula $\gamma\wedge i\in Z$, with $Z$ a parameter; it is a guard for $x_{1},\dots,x_{k},i$. Let $t^{*}$ be the term under $\gamma''$, written with $\gamma'$, $t$ and $Z$, whose value under an assignment satisfying $\gamma''$ is the value of $t$ if the assignment satisfies $\gamma'$, and $\emptyset$ otherwise. Under every assignment satisfying $\gamma''$ this value lies in $\mathcal{F}$, by Terms and Typed Terms under a Guard (iii) for $t$ and since $\emptyset\in\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi). Let $y$ be a set variable that is none of $x_{1},\dots,x_{k},i$, is not free in $\gamma''$ and does not occur in $t^{*}$, and let $\psi_{t}$ be a predicative formula expressing $\gamma'\wedge y=t$, by Terms and Typed Terms under a Guard (iv) for $t$. Under an assignment satisfying $\gamma'$, the value of $I$ is a subset of $Z$, so the assignment satisfies $\gamma''$. Hence the predicative formula

$$(\gamma''\wedge\psi_{t})\vee(\gamma''\wedge\neg\gamma'\wedge\forall s\,\neg(s\in y)),$$

with $s$ a set variable distinct from the others, holds exactly when $\gamma''$ holds and $y$ is the value of $t^{*}$; so $t^{*}$ is a term of type $\mathcal{F}$ under $\gamma''$. By Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (vi), with class variables $D$ and $C$ whose values are $Z$ and $\mathcal{F}$, under each assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$ there is exactly one map $h^{*}:Z\to\mathcal{F}$ whose value at each $a\in Z$ is the value of $t^{*}$ when $a$ is assigned to $i$.

The value lies in $\mathcal{F}$. Fix an assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, and let $I_{0}$ be the value of $I$, a set with $I_{0}\subseteq Z$. As $Z$ is countable, $I_{0}$ is countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (iv). Let $a\in I_{0}$. Assigning $a$ to $i$ changes neither the truth of $\gamma$, by Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i), $\gamma$ being predicative and $i$ not free in it, nor the value of $I$, since $i$ does not occur in $I$; so the extended assignment satisfies $\gamma'$, and $h^{*}(a)=t(a)\in\mathcal{F}$. Hence the restriction $h=h^{*}|_{I_{0}}$ is a map $h:I_{0}\to\mathcal{F}$ with $h(a)=t(a)$ for every $a\in I_{0}$, a family $(t(a))_{a\in I_{0}}$. By Unions and Intersections over a Countable Index Set in a σ-Algebra (i), $\bigcup_{a\in I_{0}}h(a)\in\mathcal{F}$, and in the case of (ii), $I_{0}$ being nonempty, $\bigcap_{a\in I_{0}}h(a)\in\mathcal{F}$ by Unions and Intersections over a Countable Index Set in a σ-Algebra (ii). By Indexed Families of Sets and Their Union, Intersection and Product (ii) and Indexed Families of Sets and Their Union, Intersection and Product (iii), this union is the class of the sets lying in $t(a)$ for some $a\in I_{0}$ and this intersection the class of the sets lying in $t(a)$ for every $a\in I_{0}$; so the value of $W$ is a set lying in $\mathcal{F}$. This is Terms and Typed Terms under a Guard (iii) for $W$, and $W$ is a term of type $\mathcal{F}$ under $\gamma$.