Predicative Formulas for σ-Algebras, π-Systems and λ-Systems, and the Sets of Them Containing a Given Family

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; this helper is in part a statement of the metatheory. Conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards (ii), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). Let $X$ be a set, let $\mathcal{P}(X)$ be its power set and $\mathcal{P}(\mathcal{P}(X))$ the power set of $\mathcal{P}(X)$, and let $\mathcal{C}$ be a subset of $\mathcal{P}(X)$. In each clause, $G$ is a set variable, and $X$ and $\mathbb{N}$ are parameters with the fixed values $X$ and the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii).

(i) The condition on $G$ that $G$ is a $\sigma$-algebra on $X$ is expressed by a predicative formula with parameters $X$ and $\mathbb{N}$. There is exactly one set $\mathcal{S}$ such that, for every set $G$, $G\in\mathcal{S}$ if and only if $G$ is a $\sigma$-algebra on $X$ and $\mathcal{C}\subseteq G$; and $\mathcal{S}\subseteq\mathcal{P}(\mathcal{P}(X))$.

(ii) The condition on $G$ that $G$ is a $\pi$-system on $X$ is expressed by a predicative formula with parameter $X$. There is exactly one set $\mathcal{S}$ such that, for every set $G$, $G\in\mathcal{S}$ if and only if $G$ is a $\pi$-system on $X$ and $\mathcal{C}\subseteq G$; and $\mathcal{S}\subseteq\mathcal{P}(\mathcal{P}(X))$.

(iii) The condition on $G$ that $G$ is a $\lambda$-system on $X$ is expressed by a predicative formula with parameters $X$ and $\mathbb{N}$. There is exactly one set $\mathcal{S}$ such that, for every set $G$, $G\in\mathcal{S}$ if and only if $G$ is a $\lambda$-system on $X$ and $\mathcal{C}\subseteq G$; and $\mathcal{S}\subseteq\mathcal{P}(\mathcal{P}(X))$.