Kit for def:sigma-algebra-measurable-space

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k<n$, not necessarily distinct. In the first three clauses, a condition on $x_{0},\dots,x_{n-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ as the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) as a parameter, which may be a set variable or a class variable.

(i) $\sigma$-algebras. With $X=x_{i}$ and $\mathcal{F}=x_{j}$, the condition "$\mathcal{F}$ is a $\sigma$-algebra on $X$" is predicative.

(ii) Measurable spaces. With $M=x_{i}$, the condition "$M$ is a measurable space" is predicative.

(iii) Measurable sets. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $A=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space and $A$ is a measurable set of $(X,\mathcal{F})$" is predicative.

(iv) The set of $\sigma$-algebras on a set. For every set $X$ there is a class $\mathcal{S}$ such that, for every class $\mathcal{F}$, $\mathcal{F}\in\mathcal{S}$ if and only if $\mathcal{F}$ is a $\sigma$-algebra on $X$; and $\mathcal{S}$ is a set and a subset of $\mathcal{P}(\mathcal{P}(X))$, where $\mathcal{P}$ denotes the power set.

(v) The class of measurable spaces. There is a class $\mathcal{M}$ such that, for every class $M$, $M\in\mathcal{M}$ if and only if $M$ is a measurable space.

(vi) The class of measurable sets. For all sets $X$ and $\mathcal{F}$ such that $(X,\mathcal{F})$ is a measurable space, there is a class $C$ such that, for every class $A$, $A\in C$ if and only if $A$ is a measurable set of $(X,\mathcal{F})$; and $C$ is $\mathcal{F}$.