Proof of Kit for def:sigma-algebra-measurable-space

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{3}$ are distinct also when $n<4$. The parameter $\mathbb{N}$ is a variable of either kind (its kind plays no role below), other than $x_{0},x_{1},\dots$ and other than the bound variables below, at its fixed value as in Conditions Expressed by a Predicative Formula, and Guards (i). The letters $B$, $a$ and $m$ denote further set variables, distinct from one another, from $x_{0},x_{1},\dots$ and from $\mathbb{N}$.

The formula for $\sigma$-algebras. Write $X$ and $\mathcal{F}$ for $x_{0}$ and $x_{1}$, and let

$$\sigma=\mathcal{F}\subseteq\mathcal{P}(X)\wedge X\in\mathcal{F}\wedge\forall B\,\bigl(B\in\mathcal{F}\Rightarrow X\setminus B\in\mathcal{F}\bigr)\wedge\forall a\,\Bigl(a\in\mathcal{F}^{\mathbb{N}}\Rightarrow\bigcup_{m\in\mathbb{N}}a(m)\in\mathcal{F}\Bigr).$$

Here $\subseteq$ is the defined predicate of Subclasses and Subsets (i); the power set $\mathcal{P}(X)$ and the value $a(m)$ are defined set symbols; and the difference $X\setminus B$, the class $\mathcal{F}^{\mathbb{N}}$ of functions from $\mathbb{N}$ to $\mathcal{F}$ and the union $\bigcup_{m\in\mathbb{N}}a(m)$ are class terms given by class abstraction with predicative formulas. Every quantifier of $\sigma$, including those inside these class terms, is over a set variable, and each defined set symbol is used as Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (viii) permits ($\mathcal{P}(X)$ exists for every set $X$, and $a(m)$ occurs only under the hypotheses $a\in\mathcal{F}^{\mathbb{N}}$, which makes $a$ a function with domain $\mathbb{N}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and $m\in\mathbb{N}$); so $\sigma$ is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), with free variables among $x_{0}$, $x_{1}$ and $\mathbb{N}$.

Let sets $X$ and $\mathcal{F}$ be assigned to $x_{0}$ and $x_{1}$. The first three conjuncts of $\sigma$ say that $\mathcal{F}\subseteq\mathcal{P}(X)$, that $X\in\mathcal{F}$, and that $X\setminus B\in\mathcal{F}$ for every $B\in\mathcal{F}$, every element of $\mathcal{F}$ being a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)). A sequence $(A_{m})$ in $\mathcal{F}$ is a map $\mathbb{N}\to\mathcal{F}$ (Sequences (i)), that is, an element of $\mathcal{F}^{\mathbb{N}}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), and so a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)); hence the quantifier $\forall a$ ranges over all sequences in $\mathcal{F}$, and the last conjunct says that

$$\bigcup_{m\in\mathbb{N}}A_{m}\in\mathcal{F}$$

for every sequence $(A_{m})$ in $\mathcal{F}$, the union being that of $(A_{m})$ as a family indexed by $\mathbb{N}$. As $\mathcal{F}$ is a set, these are exactly the requirements of σ-Algebra and Measurable Space (i): $\sigma$ holds if and only if $\mathcal{F}$ is a $\sigma$-algebra on $X$. So $\sigma$ is a predicative formula in $x_{0},x_{1}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing "$x_{1}$ is a $\sigma$-algebra on $x_{0}$".

$\sigma$-algebras. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $2$ and its renaming map $\pi$ given by $\pi(0)=i$ and $\pi(1)=j$, the formula $\sigma(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{j}$ is a $\sigma$-algebra on $x_{i}$. This proves (i).

The formula for measurable spaces. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $2$, its $n$ equal to $3$ and $\pi(0)=1$, $\pi(1)=2$, the formula $\sigma(x_{1},x_{2})$ is a predicative formula in $x_{0},x_{1},x_{2}$ that holds exactly when $x_{2}$ is a $\sigma$-algebra on $x_{1}$. Let

$$\mu=\exists x_{1}\,\exists x_{2}\,\bigl(x_{0}=(x_{1},x_{2})\wedge\sigma(x_{1},x_{2})\bigr).$$

The ordered pair is a defined set symbol, used properly since it exists for all sets (The Ordered Pair of Two Sets and Nested Tuples (i)), so $\mu$ is predicative, being built from predicative formulas by connectives and quantifiers over set variables (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)); its free variables are among $x_{0}$ and $\mathbb{N}$. For a set $M$ assigned to $x_{0}$, $\mu$ holds if and only if there are sets $X$ and $\mathcal{F}$ with $M=(X,\mathcal{F})$ and $\mathcal{F}$ a $\sigma$-algebra on $X$, that is, by σ-Algebra and Measurable Space (ii), if and only if $M$ is a measurable space. So $\mu$ is a predicative formula in $x_{0}$ expressing "$x_{0}$ is a measurable space".

Measurable spaces. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $1$ and $\pi(0)=i$, the formula $\mu(x_{i})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}$ is a measurable space. This proves (ii).

The formula for measurable sets. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $1$, its $n$ equal to $4$ and $\pi(0)=3$, the formula $\mu(x_{3})$ is a predicative formula in $x_{0},\dots,x_{3}$ that holds exactly when $x_{3}$ is a measurable space; its bound variables are renamed so as to be other than $x_{0}$, $x_{1}$ and $x_{2}$. Let

$$\rho=\exists x_{3}\,\bigl(x_{3}=(x_{0},x_{1})\wedge\mu(x_{3})\bigr)\wedge x_{2}\in x_{1}.$$

As above, $\rho$ is predicative, and its free variables are among $x_{0},x_{1},x_{2}$ and $\mathbb{N}$. Let sets $X$, $\mathcal{F}$ and $A$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. The first conjunct of $\rho$ holds exactly when the set $(X,\mathcal{F})$ is a measurable space, and the second exactly when $A\in\mathcal{F}$, that is, by σ-Algebra and Measurable Space (ii), when $A$ is a measurable set of $(X,\mathcal{F})$. So $\rho$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing "$(x_{0},x_{1})$ is a measurable space and $x_{2}$ is a measurable set of it".

Measurable sets. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\pi(0)=i$, $\pi(1)=j$, $\pi(2)=k$, the formula $\rho(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $(x_{i},x_{j})$ is a measurable space and $x_{k}$ is a measurable set of it. This proves (iii).

The set of $\sigma$-algebras on a set. Let $X$ be a set, and let $y$ be a parameter, a set variable other than those above, with value $X$. By Renaming and Substituting Variables in Predicative Formulas (iii), with its number of variables equal to $2$ and its $n$ equal to $1$, $\tau_{0}=y$ and $\tau_{1}=x_{0}$, the formula $\sigma(y,x_{0})$ is a predicative formula in $x_{0}$ that holds, for a set $\mathcal{F}$ assigned to $x_{0}$, exactly when $\mathcal{F}$ is a $\sigma$-algebra on $X$. By The Class Comprehension Theorem for Predicative Formulas (i), with one set variable $x_{0}$ and parameters $y$ and $\mathbb{N}$, there is a class $\mathcal{S}$ such that, for every set $\mathcal{F}$, $\mathcal{F}\in\mathcal{S}$ if and only if $\mathcal{F}$ is a $\sigma$-algebra on $X$. This extends to every class $\mathcal{F}$: an element of $\mathcal{S}$ is a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)), and a $\sigma$-algebra on $X$ is a set by σ-Algebra and Measurable Space (i). Every $\mathcal{F}\in\mathcal{S}$ satisfies $\mathcal{F}\subseteq\mathcal{P}(X)$, so $\mathcal{F}\in\mathcal{P}(\mathcal{P}(X))$ (The Union Set and the Power Set of a Set (ii)); hence $\mathcal{S}\subseteq\mathcal{P}(\mathcal{P}(X))$, and $\mathcal{S}$ is a set 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). This proves (iv).

The class of measurable spaces. By The Class Comprehension Theorem for Predicative Formulas (i), with one set variable $x_{0}$, the parameter $\mathbb{N}$ and the formula $\mu$, there is a class $\mathcal{M}$ such that, for every set $M$, $M\in\mathcal{M}$ if and only if $M$ is a measurable space. This extends to every class $M$: an element of $\mathcal{M}$ is a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)), and a measurable space is an ordered pair, which is a set (The Ordered Pair of Two Sets and Nested Tuples (i)). This proves (v).

The class of measurable sets. Let $X$ and $\mathcal{F}$ be sets such that $(X,\mathcal{F})$ is a measurable space. By σ-Algebra and Measurable Space (ii), the measurable sets of $(X,\mathcal{F})$ are the elements of $\mathcal{F}$, so for every class $A$, $A\in\mathcal{F}$ if and only if $A$ is a measurable set of $(X,\mathcal{F})$, and $C=\mathcal{F}$ has the required property. This proves (vi).