Proof of Kit for def:measurable-function

Throughout, formulas are written with the abbreviations $\vee$, $\Rightarrow$, $\Leftrightarrow$ and $\forall$ of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (ii); 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_{6}$ are distinct also when $N<7$; and the parameters are at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). The letters $A$, $B$, $H$, $a$, $b$, $c$, $e$, $s$, $s'$, $w$, $y$, $z$ and $z'$ denote further set variables, pairwise distinct and other than $x_{0},x_{1},\dots$ and the parameters; formulas taken from other items are used at the variables named, their bound variables chosen other than all of these. Set bookkeeping is used without comment, as carried by Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (i) and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii): elements of classes are sets, subclasses of sets (preimages under maps between sets, subsets of $\mathbb{R}^{n}$) and the segments $[n]$ are sets, and two classes with the same elements are equal. Where a cited item is stated for the earlier version of $\sigma$-algebras or of the Borel $\sigma$-algebras, the two versions agree (The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (i), The Earlier and the New Versions of the Definitions of σ-Algebras, Measures, Measurable Functions and Integrals Agree (ii)). Finally, for $n,p,q\in\mathbb{N}$, the pairs $(\mathbb{R},\mathcal{B}(\mathbb{R}))$, $(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$, $(\mathbb{R}^{p\times q},\mathcal{B}(\mathbb{R}^{p\times q}))$ and $([0,\infty],\mathcal{B}([0,\infty]))$ are measurable spaces, as recorded in Measurable Map, and the Set of Measurable Maps.

Three formulas from other items. For any two distinct set variables, here written $Y'$ and $G'$, Kit for def:sigma-algebra-measurable-space (i), with its $n$, $x_{0}$, $x_{1}$, $i$ and $j$ equal to $2$, $Y'$, $G'$, $0$ and $1$ and its parameter the class variable $\mathbb{N}$, gives a predicative formula $\mathrm{sa}(Y',G')$, with free variables among $Y'$, $G'$ and $\mathbb{N}$, that holds, for sets assigned to $Y'$ and $G'$, exactly when the set assigned to $G'$ is a $\sigma$-algebra on the set assigned to $Y'$. By 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), for distinct variables $F'$, $A'$ and $B'$ of either kind, the formula $\mathrm{mp}(F',A',B')$ is predicative, with free variables $F'$, $A'$ and $B'$, and holds for classes exactly when $F'$ is a map $F':A'\to B'$. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), with the class variables $\mathbb{N}$ and $R$ as its $Y$ and $R$, for any two distinct set variables, here written $z''$ and $n'$, there is a predicative formula $\mathrm{seg}(z'',n')$, with free variables among $z''$, $n'$, $\mathbb{N}$ and $R$, that holds for a set assigned to $z''$ and an element $n'$ of $\mathbb{N}_{0}$ exactly when that set is the segment $[n']$ of Intervals of Natural Numbers (ii). Finally, the formulas $e=(s,s')$, $(a,y)\in f$ and $((s,s'),y)\in a$ used below, for set variables, are predicative and mean what they say when sets are assigned, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv).

The formula for measurable maps. Write $X$, $\mathcal{F}$, $Y$, $\mathcal{G}$ and $f$ for $x_{0},\dots,x_{4}$, and let

$$\varphi=\mathrm{sa}(X,\mathcal{F})\wedge\mathrm{sa}(Y,\mathcal{G})\wedge\mathrm{mp}(f,X,Y)\wedge\forall B\,\Bigl(B\in\mathcal{G}\Rightarrow\exists w\,\bigl(\forall a\,\bigl(a\in w\Leftrightarrow(a\in X\wedge\exists y\,(y\in B\wedge(a,y)\in f))\bigr)\wedge w\in\mathcal{F}\bigr)\Bigr).$$

It is built from predicative formulas and atomic formulas by connectives and quantifiers over set variables only, so it is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), with free variables among $x_{0},\dots,x_{4}$ and $\mathbb{N}$.

Let sets $X$, $\mathcal{F}$, $Y$, $\mathcal{G}$ and $f$ be assigned to $x_{0},\dots,x_{4}$. By σ-Algebra and Measurable Space (ii), the first two conjuncts of $\varphi$ hold exactly when $(X,\mathcal{F})$ and $(Y,\mathcal{G})$ are measurable spaces, and the third exactly when $f$ is a map $f:X\to Y$; if one of them fails, so do $\varphi$ and the condition of (i). Assume all three hold, and let $B$ be a set. The elements of the preimage $f^{-1}[B]$ are the sets $a$ with $(a,y)\in f$ for some $y\in B$, as carried by Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii), and each of them lies in $X$, as $f:X\to Y$. So $f^{-1}[B]\subseteq X$ is a set, and a set $w$ satisfies the formula $\forall a\,(\dots)$ exactly when $w$ and $f^{-1}[B]$ have the same elements, that is, exactly when $w=f^{-1}[B]$. Hence the part $\exists w\,(\dots)$ holds exactly when $f^{-1}[B]\in\mathcal{F}$, and the last conjunct of $\varphi$ holds if and only if

$$f^{-1}[B]\in\mathcal{F}\qquad\text{for every }B\in\mathcal{G},$$

that is, by Measurable Map, and the Set of Measurable Maps (i), if and only if $f$ is $\mathcal{F}/\mathcal{G}$-measurable. So $\varphi$ is a predicative formula in $x_{0},\dots,x_{4}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing "$(x_{0},x_{1})$ and $(x_{2},x_{3})$ are measurable spaces and $x_{4}$ is an $x_{1}/x_{3}$-measurable map $x_{0}\to x_{2}$".

Measurable maps. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $5$ and its renaming map given by $0,1,2,3,4\mapsto i,j,k,l,m$, the formula $\varphi(x_{i},x_{j},x_{k},x_{l},x_{m})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ that holds, under every assignment of sets, exactly when $(x_{i},x_{j})$ and $(x_{k},x_{l})$ are measurable spaces and $x_{m}$ is an $x_{j}/x_{l}$-measurable map $x_{i}\to x_{k}$. This proves (i).

Maps into $\mathbb{R}$ and into $[0,\infty]$. The values of the parameters $\mathbb{R}$ and $\mathcal{B}(\mathbb{R})$ are sets (The Real Numbers (i), Borel Sigma-Algebra of a Metric Space (ii)). By Renaming and Substituting Variables in Predicative Formulas (iii), with its number of variables equal to $5$, its $n$ equal to $N$, and $\tau_{0},\dots,\tau_{4}$ equal to $x_{i}$, $x_{j}$, $\mathbb{R}$, $\mathcal{B}(\mathbb{R})$ and $x_{k}$, the formula $\varphi(x_{i},x_{j},\mathbb{R},\mathcal{B}(\mathbb{R}),x_{k})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ that holds exactly when $(x_{i},x_{j})$ and $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ are measurable spaces and $x_{k}$ is an $x_{j}/\mathcal{B}(\mathbb{R})$-measurable map $x_{i}\to\mathbb{R}$. Here $(\mathbb{R},\mathcal{B}(\mathbb{R}))$ is always a measurable space, as noted at the start; and by Measurable Map, and the Set of Measurable Maps (iii) the rest is the condition of (ii). Likewise the values of $[0,\infty]$ and $\mathcal{B}([0,\infty])$ are sets (The Extended Real Line, Its Order, and [0,∞] (ii), The Borel σ-Algebra of [0,∞] (ii)), $([0,\infty],\mathcal{B}([0,\infty]))$ is a measurable space, and the same substitution, with $[0,\infty]$ and $\mathcal{B}([0,\infty])$ for $\tau_{2}$ and $\tau_{3}$, gives a predicative formula $\varphi(x_{i},x_{j},[0,\infty],\mathcal{B}([0,\infty]),x_{k})$ in $x_{0},\dots,x_{N-1}$ expressing, by Measurable Map, and the Set of Measurable Maps (vi), the condition of (v). This proves (ii) and (v).

The formula for $\mathbb{R}^{n}$ and its Borel sets. Write $n$, $Y$ and $\mathcal{G}$ for $x_{0}$, $x_{1}$ and $x_{2}$, and let

$$\kappa=\forall s\,\forall B\,\Bigl(\bigl(s\in z\wedge B\in\mathcal{B}(\mathbb{R})\bigr)\Rightarrow\exists w\,\bigl(\forall a\,\bigl(a\in w\Leftrightarrow(a\in Y\wedge\exists y\,(y\in B\wedge(s,y)\in a))\bigr)\wedge w\in H\bigr)\Bigr),$$ $$\varepsilon=n\in\mathbb{N}\wedge\exists z\,\Bigl(\mathrm{seg}(z,n)\wedge\forall e\,\bigl(e\in Y\Leftrightarrow\mathrm{mp}(e,z,\mathbb{R})\bigr)\wedge\forall A\,\Bigl(A\in\mathcal{G}\Leftrightarrow\Bigl(\forall b\,(b\in A\Rightarrow b\in Y)\wedge\forall H\,\bigl((\mathrm{sa}(Y,H)\wedge\kappa)\Rightarrow A\in H\bigr)\Bigr)\Bigr)\Bigr).$$

As for $\varphi$, $\varepsilon$ is predicative, with free variables among $x_{0}$, $x_{1}$, $x_{2}$ and the parameters $\mathbb{N}$, $R$, $\mathbb{R}$ and $\mathcal{B}(\mathbb{R})$.

Let sets $n$, $Y$ and $\mathcal{G}$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $n\notin\mathbb{N}$, then $\varepsilon$ fails, and so does the condition "$n\in\mathbb{N}$, $Y=\mathbb{R}^{n}$ and $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$". The same holds for $\varepsilon'$, $\psi_{E}$ and $\psi_{M}$ below: their conditions require $n\in\mathbb{N}$, or $p,q\in\mathbb{N}$, and so do the formulas, $\varepsilon'$ by its first conjuncts and $\psi_{E}$ and $\psi_{M}$ because their first conjunct, $\varepsilon$ or $\varepsilon'$, then fails for all sets assigned to the bound variables. So there we treat only the case $n\in\mathbb{N}$, or $p,q\in\mathbb{N}$. Let $n\in\mathbb{N}$, so $n\in\mathbb{N}_{0}$ and the only set $z$ with $\mathrm{seg}(z,n)$ is $[n]$; so $\varepsilon$ holds exactly when the bracket holds with $z=[n]$. Its second conjunct says that the sets $e\in Y$ are exactly the maps $e:[n]\to\mathbb{R}$, that is, the elements of $\mathbb{R}^{n}$ (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (ii)); so it holds exactly when $Y=\mathbb{R}^{n}$. Assume $Y=\mathbb{R}^{n}$, and let $s\in[n]$ and $B\in\mathcal{B}(\mathbb{R})$. For $a\in\mathbb{R}^{n}$ there is $y\in B$ with $(s,y)\in a$ exactly when $\pi_{s}(a)\in B$ (as $a(s)=a_{s}=\pi_{s}(a)$, with $\pi_{s}:\mathbb{R}^{n}\to\mathbb{R}$ the $s$-th component map of $\mathrm{id}_{\mathbb{R}^{n}}$). So the sets $a$ with $a\in Y\wedge\exists y\,(y\in B\wedge(s,y)\in a)$ are the elements of $\pi_{s}^{-1}(B)$, and as for $\varphi$ the part $\exists w\,(\dots)$ of $\kappa$ holds exactly when $\pi_{s}^{-1}(B)\in H$. Hence $\kappa$ holds exactly when $\pi_{s}^{-1}(B)\in H$ for all $s\in[n]$ and $B\in\mathcal{B}(\mathbb{R})$, that is, by The Set of Coordinate Preimages of Borel Sets in ℝⁿ and of Entry Preimages in the Real Matrices (i), when

$$\{\pi_{s}^{-1}(B):s\in[n],\ B\in\mathcal{B}(\mathbb{R})\}\subseteq H$$

(Subclasses and Subsets (i)); write $\mathcal{C}_{n}$ for this set, a set of subsets of $\mathbb{R}^{n}$. Every $\sigma$-algebra on $\mathbb{R}^{n}$ is a set, so the quantifier $\forall H$ ranges over all of them, and for a set $A$ the right side of the last conjunct says that $A\subseteq\mathbb{R}^{n}$ and $A\in H$ for every $\sigma$-algebra $H$ on $\mathbb{R}^{n}$ with $\mathcal{C}_{n}\subseteq H$. By The σ-Algebra Generated by a Set of Subsets (ii) this holds exactly when $A\in\sigma(\mathcal{C}_{n})$, and

$$\sigma(\mathcal{C}_{n})=\mathcal{B}(\mathbb{R}^{n})$$

by The Borel Sets of ℝⁿ and of the Real Matrices Are Generated by the Coordinates (iii). So the last conjunct says that every set $A$ satisfies $A\in\mathcal{G}\Leftrightarrow A\in\mathcal{B}(\mathbb{R}^{n})$, which holds exactly when $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$. Hence $\varepsilon$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing "$x_{0}\in\mathbb{N}$, $x_{1}=\mathbb{R}^{x_{0}}$ and $x_{2}=\mathcal{B}(\mathbb{R}^{x_{0}})$".

Maps into $\mathbb{R}^{n}$. Write $X$, $\mathcal{F}$, $n$ and $f$ for $x_{0},\dots,x_{3}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its $n$ equal to $6$, the formula $\varepsilon(x_{2},x_{4},x_{5})$, given by $0,1,2\mapsto2,4,5$, is a predicative formula in $x_{0},\dots,x_{5}$ expressing "$x_{2}\in\mathbb{N}$, $x_{4}=\mathbb{R}^{x_{2}}$ and $x_{5}=\mathcal{B}(\mathbb{R}^{x_{2}})$", and $\varphi(x_{0},x_{1},x_{4},x_{5},x_{3})$, given by $0,1,2,3,4\mapsto0,1,4,5,3$, is one expressing "$(x_{0},x_{1})$ and $(x_{4},x_{5})$ are measurable spaces and $x_{3}$ is an $x_{1}/x_{5}$-measurable map $x_{0}\to x_{4}$". Let

$$\psi_{E}=\exists x_{4}\,\exists x_{5}\,\bigl(\varepsilon(x_{2},x_{4},x_{5})\wedge\varphi(x_{0},x_{1},x_{4},x_{5},x_{3})\bigr).$$

It is predicative, with free variables among $x_{0},\dots,x_{3}$ and the parameters. Let sets $X$, $\mathcal{F}$, $n$ and $f$ be assigned to $x_{0},\dots,x_{3}$. As noted with $\varepsilon$, we may take $n\in\mathbb{N}$. Then the only sets assigned to $x_{4}$ and $x_{5}$ that satisfy the first conjunct are $\mathbb{R}^{n}$ and $\mathcal{B}(\mathbb{R}^{n})$, which are sets (Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations (i), Borel Sigma-Algebra of a Metric Space (iii)); so $\psi_{E}$ holds exactly when $(X,\mathcal{F})$ and $(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ are measurable spaces and $f$ is an $\mathcal{F}/\mathcal{B}(\mathbb{R}^{n})$-measurable map $f:X\to\mathbb{R}^{n}$. As $(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ is a measurable space, as noted at the start, by Measurable Map, and the Set of Measurable Maps (iv) $\psi_{E}$ holds exactly when the condition of (iii) holds with $X=x_{0}$, $\mathcal{F}=x_{1}$, $n=x_{2}$ and $f=x_{3}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $4$ and its renaming map given by $0,1,2,3\mapsto i,j,k,l$, the formula $\psi_{E}(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing that condition with $X=x_{i}$, $\mathcal{F}=x_{j}$, $n=x_{k}$ and $f=x_{l}$. This proves (iii).

The formula for $\mathbb{R}^{p\times q}$ and its Borel sets. Write $p$, $q$, $Y$ and $\mathcal{G}$ for $x_{0},\dots,x_{3}$, and let

$$\kappa'=\forall s\,\forall s'\,\forall B\,\Bigl(\bigl(s\in z\wedge s'\in z'\wedge B\in\mathcal{B}(\mathbb{R})\bigr)\Rightarrow\exists w\,\bigl(\forall a\,\bigl(a\in w\Leftrightarrow(a\in Y\wedge\exists y\,(y\in B\wedge((s,s'),y)\in a))\bigr)\wedge w\in H\bigr)\Bigr),$$ $$\begin{aligned} \varepsilon'={}&p\in\mathbb{N}\wedge q\in\mathbb{N}\wedge\exists z\,\exists z'\,\exists c\,\Bigl(\mathrm{seg}(z,p)\wedge\mathrm{seg}(z',q)\wedge\forall e\,\bigl(e\in c\Leftrightarrow\exists s\,\exists s'\,(s\in z\wedge s'\in z'\wedge e=(s,s'))\bigr)\\ &\wedge\forall e\,\bigl(e\in Y\Leftrightarrow\mathrm{mp}(e,c,\mathbb{R})\bigr)\wedge\forall A\,\Bigl(A\in\mathcal{G}\Leftrightarrow\Bigl(\forall b\,(b\in A\Rightarrow b\in Y)\wedge\forall H\,\bigl((\mathrm{sa}(Y,H)\wedge\kappa')\Rightarrow A\in H\bigr)\Bigr)\Bigr)\Bigr). \end{aligned}$$

As for $\varphi$, $\varepsilon'$ is predicative, with free variables among $x_{0},\dots,x_{3}$ and the parameters $\mathbb{N}$, $R$, $\mathbb{R}$ and $\mathcal{B}(\mathbb{R})$.

Let sets $p$, $q$, $Y$ and $\mathcal{G}$ be assigned to $x_{0},\dots,x_{3}$. As noted with $\varepsilon$, we may take $p,q\in\mathbb{N}$, the condition being "$p,q\in\mathbb{N}$, $Y=\mathbb{R}^{p\times q}$ and $\mathcal{G}=\mathcal{B}(\mathbb{R}^{p\times q})$". Then the only sets $z$ and $z'$ satisfying the first two conjuncts of the bracket are $[p]$ and $[q]$. The elements of the Cartesian product $[p]\times[q]$ are exactly the ordered pairs $(s,s')$ with $s\in[p]$ and $s'\in[q]$, and $[p]\times[q]$ is a set (Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii)); so, given $z=[p]$ and $z'=[q]$, the third conjunct holds exactly when $c=[p]\times[q]$. The fourth then says that the sets $e\in Y$ are exactly the maps $e:[p]\times[q]\to\mathbb{R}$, that is, the elements of the set $\mathcal{M}_{p\times q}(\mathbb{R})=\mathbb{R}^{p\times q}$ of real $p\times q$ matrices (Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)); so it holds exactly when $Y=\mathbb{R}^{p\times q}$. Assume this, and let $s\in[p]$, $s'\in[q]$ and $B\in\mathcal{B}(\mathbb{R})$. For $a\in\mathbb{R}^{p\times q}$ there is $y\in B$ with $((s,s'),y)\in a$ exactly when $E_{ss'}(a)\in B$ (as $a(s,s')=a_{ss'}=E_{ss'}(a)$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (ii), with $E_{ss'}:\mathbb{R}^{p\times q}\to\mathbb{R}$ the entry map of $\mathrm{id}_{\mathbb{R}^{p\times q}}$ in row $s$ and column $s'$). As for $\varepsilon$, $\kappa'$ therefore holds exactly when $E_{ss'}^{-1}(B)\in H$ for all $s\in[p]$, $s'\in[q]$ and $B\in\mathcal{B}(\mathbb{R})$, that is, by The Set of Coordinate Preimages of Borel Sets in ℝⁿ and of Entry Preimages in the Real Matrices (ii), when $\mathcal{C}'_{p,q}\subseteq H$ for the set

$$\mathcal{C}'_{p,q}=\{E_{ss'}^{-1}(B):s\in[p],\ s'\in[q],\ B\in\mathcal{B}(\mathbb{R})\}$$

of subsets of $\mathbb{R}^{p\times q}$. As for $\varepsilon$, by The σ-Algebra Generated by a Set of Subsets (ii) the last conjunct says that every set $A$ satisfies $A\in\mathcal{G}\Leftrightarrow A\in\sigma(\mathcal{C}'_{p,q})$, and

$$\sigma(\mathcal{C}'_{p,q})=\mathcal{B}(\mathbb{R}^{p\times q})$$

by The Borel Sets of ℝⁿ and of the Real Matrices Are Generated by the Coordinates (iv); so it holds exactly when $\mathcal{G}=\mathcal{B}(\mathbb{R}^{p\times q})$. Hence $\varepsilon'$ is a predicative formula in $x_{0},\dots,x_{3}$ expressing "$x_{0},x_{1}\in\mathbb{N}$, $x_{2}=\mathbb{R}^{x_{0}\times x_{1}}$ and $x_{3}=\mathcal{B}(\mathbb{R}^{x_{0}\times x_{1}})$".

Maps into $\mathbb{R}^{p\times q}$. Write $X$, $\mathcal{F}$, $p$, $q$ and $f$ for $x_{0},\dots,x_{4}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its $n$ equal to $7$, the formula $\varepsilon'(x_{2},x_{3},x_{5},x_{6})$, given by $0,1,2,3\mapsto2,3,5,6$, is a predicative formula in $x_{0},\dots,x_{6}$ expressing "$x_{2},x_{3}\in\mathbb{N}$, $x_{5}=\mathbb{R}^{x_{2}\times x_{3}}$ and $x_{6}=\mathcal{B}(\mathbb{R}^{x_{2}\times x_{3}})$", and $\varphi(x_{0},x_{1},x_{5},x_{6},x_{4})$, given by $0,1,2,3,4\mapsto0,1,5,6,4$, is one expressing "$(x_{0},x_{1})$ and $(x_{5},x_{6})$ are measurable spaces and $x_{4}$ is an $x_{1}/x_{6}$-measurable map $x_{0}\to x_{5}$". Let

$$\psi_{M}=\exists x_{5}\,\exists x_{6}\,\bigl(\varepsilon'(x_{2},x_{3},x_{5},x_{6})\wedge\varphi(x_{0},x_{1},x_{5},x_{6},x_{4})\bigr).$$

It is predicative, with free variables among $x_{0},\dots,x_{4}$ and the parameters. Exactly as for $\psi_{E}$, using that $\mathbb{R}^{p\times q}$ is a set (Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations (i)), that $\mathcal{B}(\mathbb{R}^{p\times q})$ of Borel Sigma-Algebra of a Metric Space (iv) is a set and $(\mathbb{R}^{p\times q},\mathcal{B}(\mathbb{R}^{p\times q}))$ a measurable space, as noted at the start, and Measurable Map, and the Set of Measurable Maps (v), $\psi_{M}$ holds, under every assignment of sets, exactly when $(x_{0},x_{1})$ is a measurable space, $x_{2},x_{3}\in\mathbb{N}$, and $x_{4}$ is a map $x_{0}\to\mathbb{R}^{x_{2}\times x_{3}}$ that is measurable as a map into $\mathbb{R}^{x_{2}\times x_{3}}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $5$ and its renaming map given by $0,1,2,3,4\mapsto i,j,k,l,m$, the formula $\psi_{M}(x_{i},x_{j},x_{k},x_{l},x_{m})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (iv). This proves (iv).