Proof of Borel Sets of a Variable Metric Space as a Predicative Condition, and the Families of σ-Algebras Generated by Random Elements and of Their Composites

Throughout, formulas are written with abbreviations; each formula below quantifies over set variables only and is therefore predicative, its bound variables being renamed apart from the other variables in play where needed (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i)). For a function $F$ and a set $u$ in its domain, $(u,v)\in F$ holds exactly for $v=F(u)$ (Functions, Values of a Function, and Functions from One Class to Another (ii)), and $\mu(F,A,B)$ is the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), which holds exactly when $F$ is a map $F:A\to B$.

Proof of (i). Let $a,b,c,e,f,p,s,x,y,z$ be further set variables. Let $\delta(S,d)$ be

$$\exists c\,\Bigl(\forall p\,\bigl(p\in c\Leftrightarrow\exists x\,\exists y\,(x\in S\wedge y\in S\wedge p=(x,y))\bigr)\wedge\mu(d,c,\mathbb{R})\Bigr).$$

The only $c$ satisfying its first conjunct is the Cartesian product $S\times S$, so $\delta(S,d)$ holds exactly when $d$ is a map $S\times S\to\mathbb{R}$. Let $\kappa(S,d)$ be

$$\forall x\,\forall y\,\forall z\,\forall a\,\forall b\,\forall e\,\forall f\,\forall s\,\Bigl(\bigl(x\in S\wedge y\in S\wedge z\in S\wedge((x,y),a)\in d\wedge((y,x),b)\in d\wedge((x,z),e)\in d\wedge((y,z),f)\in d\wedge((a,f),s)\in{+}\bigr)\Rightarrow\bigl((0,a)\in{\le}\wedge(a=0\Leftrightarrow x=y)\wedge a=b\wedge(e,s)\in{\le}\bigr)\Bigr).$$

When $\delta(S,d)$ holds and $x,y,z\in S$, its premises single out $a=d(x,y)$, $b=d(y,x)$, $e=d(x,z)$, $f=d(y,z)$ and $s=d(x,y)+d(y,z)$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi) for the sum), so $\kappa(S,d)$ states the four conditions of Metric Space (i). Hence

$$\chi(S,d)=\delta(S,d)\wedge\kappa(S,d)$$

expresses that $(S,d)$ is a metric space (Metric Space (vi)); its parameters are $\mathbb{R}$, $\le$, $+$ and $0$.

Proof of (ii). Let $z$ be a further set variable. By Open Ball in a Metric Space (ii), $y\in B_{d}(x,r)$ means $y\in S$ and $d(x,y)<r$, so the condition is expressed by

$$\chi(S,d)\wedge x\in S\wedge r\in\mathbb{R}\wedge(0,r)\in{<}\wedge y\in S\wedge\exists z\,\bigl(((x,y),z)\in d\wedge(z,r)\in{<}\bigr),$$

whose parameters are $\mathbb{R}$, $\le$, $<$, $+$ and $0$.

Proof of (iii). Let $\omega(U,S,d)$ be the formula $\omega(U)$ of The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula (i) with $S$ in place of $X$. That clause holds for every metric space $(X,d)$, a statement about parameters holding for all their values satisfying its hypotheses (Conditions Expressed by a Predicative Formula, and Guards (i)). So under every assignment for which $(S,d)$ is a metric space, $\omega(U,S,d)$ holds if and only if $U\subseteq S$ and $U$ is open in $(S,d)$, that is, $U\in\mathcal{T}_{d}$ (The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula (ii)). Hence $\chi(S,d)\wedge\omega(U,S,d)$ expresses the condition, with parameters $\mathbb{R}$, $\le$, $<$, $+$ and $0$.

Proof of (iv). Let $A,c,f,n,w$ be further set variables, and let $\varsigma(G,Y)$ be the conjunction of the four formulas

$$\forall A\,\bigl(A\in G\Rightarrow\forall w\,(w\in A\Rightarrow w\in Y)\bigr),\qquad Y\in G,$$ $$\forall A\,\Bigl(A\in G\Rightarrow\exists c\,\bigl(\forall w\,(w\in c\Leftrightarrow(w\in Y\wedge w\notin A))\wedge c\in G\bigr)\Bigr),$$ $$\forall f\,\Bigl(\mu(f,\mathbb{N},G)\Rightarrow\exists c\,\bigl(\forall w\,(w\in c\Leftrightarrow\exists n\,\exists A\,(n\in\mathbb{N}\wedge(n,A)\in f\wedge w\in A))\wedge c\in G\bigr)\Bigr).$$

The first says $G\subseteq\mathcal{P}(Y)$ (The Union Set and the Power Set of a Set (ii)). In the third, the only $c$ with the stated elements is the difference $Y\setminus A$. In the fourth, the sets $f$ with $\mu(f,\mathbb{N},G)$ are the sequences $(A_{n})$ in $G$, and the only $c$ with the stated elements is the union $\bigcup_{n\in\mathbb{N}}A_{n}$, a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets (i). So $\varsigma(G,Y)$, whose only parameter is $\mathbb{N}$, holds if and only if $G$ is a $\sigma$-algebra on $Y$ (σ-Algebra and Measurable Space (i)).

Proof of (v). Let $G,U,w$ be further set variables and let $\beta(B,S,d)$ be

$$\chi(S,d)\wedge\forall w\,(w\in B\Rightarrow w\in S)\wedge\forall G\,\Bigl(\bigl(\varsigma(G,S)\wedge\forall U\,(\omega(U,S,d)\Rightarrow U\in G)\bigr)\Rightarrow B\in G\Bigr).$$

If $(S,d)$ is not a metric space, $\beta(B,S,d)$ and the condition both fail. Let $(S,d)$ be a metric space. Then $\mathcal{B}(S,d)=\sigma(\mathcal{T}_{d})$ (Borel Sigma-Algebra of a Metric Space (i)), and by The σ-Algebra Generated by a Set of Subsets (ii), $B\in\sigma(\mathcal{T}_{d})$ if and only if $B\subseteq S$ and $B\in G$ for every $\sigma$-algebra $G$ on $S$ with $\mathcal{T}_{d}\subseteq G$. By (iv), as proved above, $\varsigma(G,S)$ says that $G$ is a $\sigma$-algebra on $S$; and by the property of $\omega$ shown in the proof of (iii), $\forall U\,(\omega(U,S,d)\Rightarrow U\in G)$ says $\mathcal{T}_{d}\subseteq G$. So $\beta(B,S,d)$ expresses the condition, with parameters $\mathbb{R}$, $\le$, $<$, $+$, $0$ and $\mathbb{N}$.

Proof of (vi). Let $\Omega$, and $\Sigma$, $D$ and $\Xi$, be parameters whose values are $\Omega$ and the functions giving the families $(S_{j})_{j\in J}$, $(d_{j})_{j\in J}$ and $(X_{j})_{j\in J}$, and let $j,z,s,e,x,A,G,B,c,w,y$ be set variables. Let $\pi(c,B)$ be $\forall w\,(w\in c\Leftrightarrow\exists y\,(y\in B\wedge(w,y)\in x))$, the formula of Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i) with $c$, $B$ and $x$ for its $z$, $V$ and $u$, and let $\theta(z,j)$ be

$$\exists s\,\exists e\,\exists x\,\Bigl((j,s)\in\Sigma\wedge(j,e)\in D\wedge(j,x)\in\Xi\wedge\forall A\,\Bigl(A\in z\Leftrightarrow\bigl(\forall w\,(w\in A\Rightarrow w\in\Omega)\wedge\forall G\,\bigl((\varsigma(G,\Omega)\wedge\forall B\,(\beta(B,s,e)\Rightarrow\exists c\,(\pi(c,B)\wedge c\in G)))\Rightarrow A\in G\bigr)\bigr)\Bigr)\Bigr).$$

Let $j\in J$. The only sets $s$, $e$ and $x$ satisfying the first three conjuncts are $S_{j}$, $d_{j}$ and $X_{j}$, and $X_{j}$ is a map $\Omega\to S_{j}$ (Probability Spaces, Events and Random Elements (iii)). For every set $B$, the only $c$ with $\pi(c,B)$ is $X_{j}^{-1}(B)$ (Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i)), and $\beta(B,S_{j},d_{j})$ holds if and only if $B\in\mathcal{B}(S_{j})$, by (v) as proved above. So, with $\mathcal{C}_{j}=\{X_{j}^{-1}(B):B\in\mathcal{B}(S_{j})\}$, the subset of $\mathcal{P}(\Omega)$ of σ-Algebras Generated by Random Elements (i), the inner formula says that $A\subseteq\Omega$ and $A\in G$ for every $\sigma$-algebra $G$ on $\Omega$ with $\mathcal{C}_{j}\subseteq G$, which by The σ-Algebra Generated by a Set of Subsets (ii) means $A\in\sigma(\mathcal{C}_{j})=\sigma(X_{j})$. Thus $\theta(z,j)$ holds exactly when $z$ and $\sigma(X_{j})$ have the same elements, that is, when $z=\sigma(X_{j})$. So $\sigma(X_{j})$ is a defined set symbol with argument $j$, given by $\theta$ and used properly at every $j\in J$. As $\sigma(X_{j})$ is a $\sigma$-algebra on $\Omega$ (σ-Algebras Generated by Random Elements (i)), $\sigma(X_{j})\subseteq\mathcal{P}(\Omega)$, that is, $\sigma(X_{j})\in\mathcal{P}(\mathcal{P}(\Omega))$ (σ-Algebra and Measurable Space (i), The Union Set and the Power Set of a Set (ii)). By Maps and Relations Given by Formulas (i), with $J$ for $a$, $\mathcal{P}(\mathcal{P}(\Omega))$ for $b$ and $\sigma(X_{j})$ for $t(j)$, exactly one map $\mathcal{G}:J\to\mathcal{P}(\mathcal{P}(\Omega))$ has $\mathcal{G}(j)=\sigma(X_{j})$ for every $j\in J$; it is a family indexed by $J$. Any family $(\mathcal{G}'_{j})_{j\in J}$ with $\mathcal{G}'_{j}=\sigma(X_{j})$ for every $j\in J$ is a function with domain $J$ and range contained in $\mathcal{P}(\mathcal{P}(\Omega))$, hence a map $J\to\mathcal{P}(\mathcal{P}(\Omega))$ (Functions, Values of a Function, and Functions from One Class to Another (iii)), and so it is $\mathcal{G}$.

Proof of (vii). Let $\Xi$ and $\Gamma$ be parameters whose values are the functions giving $(X_{j})_{j\in J}$ and $(g_{j})_{j\in J}$, let $j,z,x,h,p,u,v,w$ be set variables, and let $\theta'(z,j)$ be

$$\exists x\,\exists h\,\Bigl((j,x)\in\Xi\wedge(j,h)\in\Gamma\wedge\forall p\,\bigl(p\in z\Leftrightarrow\exists u\,\exists v\,\exists w\,((u,v)\in x\wedge(v,w)\in h\wedge p=(u,w))\bigr)\Bigr).$$

Let $j\in J$. The only $x$ and $h$ satisfying the first two conjuncts are $X_{j}$ and $g_{j}$, so by Relations, Domain, Range, Inverse and Composition (v) the only set $z$ with $\theta'(z,j)$ is the composite $g_{j}\circ X_{j}=g_{j}(X_{j})$, which is a map $\Omega\to T_{j}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii). Thus $g_{j}(X_{j})$ is a defined set symbol with argument $j$, given by $\theta'$ and used properly at every $j\in J$. Let $\mathcal{U}=\bigcup_{j\in J}T_{j}$, a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets (i). Every element of $g_{j}(X_{j})$ is an ordered pair $(u,w)$ with $u\in\Omega$ and $w\in T_{j}\subseteq\mathcal{U}$ (Functions, Values of a Function, and Functions from One Class to Another (iii), Indexed Families of Sets and Their Union, Intersection and Product (ii)), so $g_{j}(X_{j})\in\mathcal{P}(\Omega\times\mathcal{U})$. As in the proof of (vi), Maps and Relations Given by Formulas (i) with $J$ for $a$, $\mathcal{P}(\Omega\times\mathcal{U})$ for $b$ and $g_{j}(X_{j})$ for $t(j)$ gives exactly one map $J\to\mathcal{P}(\Omega\times\mathcal{U})$ with value $g_{j}(X_{j})$ at every $j\in J$, and every family with these values is such a map, hence equal to it.