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

In the setting of Measure Spaces, Borel Sets and Lebesgue Measure on the Real Line: Standing Notation; this helper is a statement of the metatheory about expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, and terms of type $A$ under $\gamma$ for a class $A$, be as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii). Let $X$ be a set, $\mathcal{F}$ a $\sigma$-algebra on $X$ and $Z$ a countable set, all three values of parameters; let $\mathcal{P}(Z)$ be the power set of $Z$. Let $I$ be a term of type $\mathcal{P}(Z)$ under $\gamma$, let $i$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $I$, and let $\gamma'$ be a guard for the variables $x_{1},\dots,x_{k},i$ that expresses the condition $\gamma\wedge i\in I$, as in Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii). Let $t$ be a term of type $\mathcal{F}$ under $\gamma'$, and, under an assignment satisfying $\gamma$ and for $a$ in the value of $I$, let $t(a)$ be the value of $t$ when $a$ is assigned to $i$ and $x_{1},\dots,x_{k}$ keep their sets.

(i) Let $U$ be a term under $\gamma$, of which every parameter of $I$ and of $t$ is a parameter, whose value under each assignment satisfying $\gamma$ is the class of the sets lying in $t(a)$ for some $a$ in the value of $I$; for instance the term $\bigcup_{i\in I}t$ of Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii). Then $U$ is a term of type $\mathcal{F}$ under $\gamma$.

(ii) Suppose that the value of $I$ is nonempty under every assignment satisfying $\gamma$. Let $V$ be a term under $\gamma$, of which every parameter of $I$ and of $t$ is a parameter, whose value under each assignment satisfying $\gamma$ is the class of the sets lying in $t(a)$ for every $a$ in the value of $I$; for instance the term $\bigcap_{i\in I}t$ of Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (ii). Then $V$ is a term of type $\mathcal{F}$ under $\gamma$.