Proof of Kit for def:borel-sigma-algebra-metric

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_{5}$ are distinct also when $n<6$. The parameters $\mathbb{N}$, $\mathbb{R}$, $+$, $0$ and $\le$ are variables other than $x_{0},x_{1},\dots$ and other than the bound variables below, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). The letter $w$ denotes a further set variable, distinct from $x_{0},x_{1},\dots$ and from the parameters, and the bound variables of the formulas taken from other items are chosen other than $w$ and $x_{0},x_{1},\dots$. Where a cited item is stated for the earlier version of metric spaces, open sets or $\sigma$-algebras, the two versions agree (The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (i), The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (v), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i)).

The formula for $\mathcal{T}_{d}$. Write $X$, $d$, $T$ and $U$ for $x_{0}$, $x_{1}$, $x_{2}$ and $x_{3}$. By Kit for def:metric-space (vi) with its $n$, $i$ and $j$ equal to $2$, $0$ and $1$, there is a predicative formula $\mu_{0}$ in $x_{0},x_{1}$, with parameters among $\mathbb{R}$, $+$, $0$ and $\le$, that expresses "$d$ is a map $X\times X\to\mathbb{R}$ and $(X,d)$ is a metric space"; it is also a predicative formula in $x_{0},\dots,x_{5}$ (Renaming and Substituting Variables in Predicative Formulas (ii)). By Kit for def:open-subset-metric-space (i) with its $n$, $i$, $j$ and $k$ equal to $4$, $0$, $1$ and $3$, there is a predicative formula $\omega$ in $x_{0},\dots,x_{3}$, with the same parameters, that expresses "$(X,d)$ is a metric space, $U\subseteq X$, and $U$ is open in $(X,d)$". Let

$$\tau=\mu_{0}\wedge\forall U\,\bigl(U\in T\Leftrightarrow\omega\bigr).$$

It is predicative, being built from predicative formulas by connectives and a quantifier over the set variable $x_{3}$ (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and its free variables are among $x_{0},x_{1},x_{2}$ and the parameters.

Let sets $X$, $d$ and $T$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $d$ is not a map $X\times X\to\mathbb{R}$ or $(X,d)$ is not a metric space, then $\mu_{0}$ fails, and so do $\tau$ and the condition "$(X,d)$ is a metric space and $T=\mathcal{T}_{d}$". Suppose now that $(X,d)$ is a metric space, so that $\mu_{0}$ holds. For every set $U$ assigned to $x_{3}$, $\omega$ holds exactly when $U\subseteq X$ and $U$ is open in $(X,d)$. So $\tau$ holds if and only if, for every set $U$,

$$U\in T\iff U\subseteq X\text{ and }U\text{ is open in }(X,d).$$

By The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula (ii), $\mathcal{T}_{d}$ is the only set with this property; as $T$ is a set, $\tau$ holds if and only if $T=\mathcal{T}_{d}$. In all cases $\tau$ holds exactly when the condition does, so $\tau$ is a predicative formula in $x_{0},x_{1},x_{2}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing "$(X,d)$ is a metric space and $T=\mathcal{T}_{d}$" with $X$, $d$ and $T$ the sets assigned to $x_{0}$, $x_{1}$ and $x_{2}$.

The set of open subsets. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and its renaming map $\pi$ given by $\pi(0)=i$, $\pi(1)=j$ and $\pi(2)=k$, the formula $\tau(x_{i},x_{j},x_{k})$ 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_{i},x_{j})$ is a metric space and $x_{k}=\mathcal{T}_{x_{j}}$. This proves (i).

The formula for $\mathcal{B}(X,d)$. Now write $X$, $d$, $B$, $A$, $G$ and $T'$ for $x_{0},\dots,x_{5}$. By Kit for def:sigma-algebra-measurable-space (i), with its $n$, $i$ and $j$ equal to $6$, $0$ and $4$, there is a predicative formula $\gamma$ in $x_{0},\dots,x_{5}$, with free variables among $x_{0}$, $x_{4}$ and the parameter $\mathbb{N}$, that holds, for sets $X$ and $G$ assigned to $x_{0}$ and $x_{4}$, exactly when $G$ is a $\sigma$-algebra on $X$. By Renaming and Substituting Variables in Predicative Formulas (i) with its number of variables equal to $3$, its $n$ equal to $6$ and its renaming map $\pi$ given by $\pi(0)=0$, $\pi(1)=1$, $\pi(2)=5$, the formula $\tau'=\tau(x_{0},x_{1},x_{5})$, its bound variables renamed so as to be other than $x_{3}$ and $x_{4}$, is a predicative formula in $x_{0},\dots,x_{5}$ that holds exactly when $(X,d)$ is a metric space and $T'=\mathcal{T}_{d}$. Let

$$\beta=\mu_{0}\wedge\forall A\,\Bigl(A\in B\Leftrightarrow\Bigl(\forall w\,(w\in A\Rightarrow w\in X)\wedge\forall G\,\Bigl(\bigl(\gamma\wedge\exists T'\,\bigl(\tau'\wedge\forall w\,(w\in T'\Rightarrow w\in G)\bigr)\bigr)\Rightarrow A\in G\Bigr)\Bigr)\Bigr).$$

It is predicative, every quantifier in it being applied to a set variable (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and its free variables are among $x_{0},x_{1},x_{2}$ and the parameters.

Let sets $X$, $d$ and $B$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $d$ is not a map $X\times X\to\mathbb{R}$ or $(X,d)$ is not a metric space, then $\mu_{0}$ fails, and so do $\beta$ and the condition "$(X,d)$ is a metric space and $B=\mathcal{B}(X,d)$". Suppose now that $(X,d)$ is a metric space, and let sets $A$ and $G$ be assigned to $x_{3}$ and $x_{4}$. For a set $T'$ assigned to $x_{5}$, $\tau'$ holds exactly when $T'=\mathcal{T}_{d}$, and $\mathcal{T}_{d}$ is a set (The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula (ii)); so $\exists T'\,\bigl(\tau'\wedge\forall w\,(w\in T'\Rightarrow w\in G)\bigr)$ holds exactly when $\mathcal{T}_{d}\subseteq G$ (Subclasses and Subsets (i)). Every $\sigma$-algebra on $X$ is a set, by σ-Algebra and Measurable Space (i), so the quantifier $\forall G$ ranges over all of them, and the second conjunct of the bracket says that $A\in G$ for every $\sigma$-algebra $G$ on $X$ with $\mathcal{T}_{d}\subseteq G$; the first says $A\subseteq X$. The set $\mathcal{T}_{d}$ is a set of subsets of $X$, and $\mathcal{B}(X,d)=\sigma(\mathcal{T}_{d})$ (Borel Sigma-Algebra of a Metric Space (i)); so by The σ-Algebra Generated by a Set of Subsets (ii) the bracket holds exactly when

$$A\in\mathcal{B}(X,d).$$

Hence $\beta$ holds if and only if every set $A$ satisfies $A\in B\Leftrightarrow A\in\mathcal{B}(X,d)$. If $B=\mathcal{B}(X,d)$, this is clear; conversely, if it holds, then $B=\mathcal{B}(X,d)$ by Axiom of Extensionality for Classes. In all cases $\beta$ holds exactly when the condition does, so $\beta$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing "$(X,d)$ is a metric space and $B=\mathcal{B}(X,d)$" with $X$, $d$ and $B$ the sets assigned to $x_{0}$, $x_{1}$ and $x_{2}$.

The Borel $\sigma$-algebra. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and its renaming map $\pi$ given by $\pi(0)=i$, $\pi(1)=j$ and $\pi(2)=k$, the formula $\beta(x_{i},x_{j},x_{k})$ 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_{i},x_{j})$ is a metric space and $x_{k}=\mathcal{B}(x_{i},x_{j})$. This proves (ii).