Proof of The Set of Coordinate Preimages of Borel Sets in ℝⁿ and of Entry Preimages in the Real Matrices

One argument serves both clauses. For (i) let $Y=\mathbb{R}^{n}$, $J=[n]$ and $c_{j}=\pi_{j}$ for $j\in J$; for (ii) let $Y=\mathcal{M}_{p\times q}(\mathbb{R})$, $J=[p]\times[q]$ and $c_{(i,j)}=E_{ij}$ for $(i,j)\in J$. In both cases $J$ is a set, $[n]$, $[p]$ and $[q]$ being sets by Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (v) and $[p]\times[q]$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii). The identities $\mathrm{id}_{\mathbb{R}^{n}}:\mathbb{R}^{n}\to\mathbb{R}^{n}$ and $\mathrm{id}_{\mathcal{M}_{p\times q}(\mathbb{R})}:\mathcal{M}_{p\times q}(\mathbb{R})\to\mathcal{M}_{p\times q}(\mathbb{R})$ are maps by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii). By Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them (i), applied to $\mathrm{id}_{\mathbb{R}^{n}}$, and by Component Maps of a Map into $\mathbb{R}^{q}$, Entry Maps of a Map into Matrices, and Maps Assembled from Them (ii), applied to $\mathrm{id}_{\mathcal{M}_{p\times q}(\mathbb{R})}$, $j\mapsto c_{j}$ is a map $c:J\to\mathbb{R}^{Y}$ into the set $\mathbb{R}^{Y}$ of maps $Y\to\mathbb{R}$. By Borel Sigma-Algebra of a Metric Space (ii), Borel Sigma-Algebra of a Metric Space (i) and Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (iii), $\mathcal{B}(\mathbb{R})$ is a $\sigma$-algebra on $\mathbb{R}$, so $\mathcal{B}(\mathbb{R})\subseteq\mathcal{P}(\mathbb{R})$ by σ-Algebra and Measurable Space (i).

The condition is predicative. Let $j$ and $B$ be distinct set variables, and let $\gamma$ be the formula $j\in J\wedge B\in\mathcal{B}(\mathbb{R})$, with the parameters $J$ and $\mathcal{B}(\mathbb{R})$; it is predicative, having no quantifier, so it is a guard for the variables $j$ and $B$. Under every assignment satisfying $\gamma$, $j\in J$ and $B\in\mathcal{P}(\mathbb{R})$, so $j$ is a term of type $J$ and $B$ a term of type $\mathcal{P}(\mathbb{R})$ under $\gamma$, by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i); then $c(j)$, written with the parameter $c$, is a term of type $\mathbb{R}^{Y}$ under $\gamma$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), and $c(j)^{-1}(B)$ is a term of type $\mathcal{P}(Y)$ under $\gamma$ by Preimages, Unions and Intersections over an Index Set, Suprema and Infima, and Superlevel Sets as Typed Terms (i). Its value under an assignment satisfying $\gamma$ is $c_{j}^{-1}(B)$, the preimage, which is the defined set symbol of Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i). Let $C$ be a set variable other than $j$ and $B$ that occurs in none of the parameters. By Terms and Typed Terms under a Guard (iv), there is a predicative formula $\psi$, with free variables among $j$, $B$, $C$ and the parameters, expressing the condition $\gamma\wedge C=c(j)^{-1}(B)$: for all sets $j$, $B$ and $C$, $\psi$ holds if and only if $j\in J$, $B\in\mathcal{B}(\mathbb{R})$ and $C=c_{j}^{-1}(B)$. Let $\varphi(C)$ be the formula $\exists j\,\exists B\,\psi$. Its quantifiers bind set variables only, so it is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v), and for every set $C$, $\varphi(C)$ holds if and only if $\psi$ holds for some sets assigned to $j$ and $B$ (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)), that is, if and only if $C=c_{j}^{-1}(B)$ for some $j\in J$ and some $B\in\mathcal{B}(\mathbb{R})$.

The set. Let $\mathcal{C}_{Y}=\{C\in\mathcal{P}(Y):\varphi(C)\}$, formed by Sets and Maps: Ordinary Notation (iii) from the predicative formula $\varphi$; it is a set and a subset of $\mathcal{P}(Y)$. Let $C$ be a set. If $C\in\mathcal{C}_{Y}$, then $\varphi(C)$ holds, so $C=c_{j}^{-1}(B)$ for some $j\in J$ and $B\in\mathcal{B}(\mathbb{R})$. Conversely, if $C=c_{j}^{-1}(B)$ for such $j$ and $B$, then $C\subseteq Y$ by Preimages under a Map: Membership, the Preimage Map, Sequences of Preimages, and the Set of Sets with Preimage in a Given Set (i), so $C\in\mathcal{P}(Y)$ by The Union Set and the Power Set of a Set (ii), and $\varphi(C)$ holds, so $C\in\mathcal{C}_{Y}$. Hence $\mathcal{C}_{Y}$ has the stated property. Two sets with this property have the same elements, so they are equal by Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii).

In the case of (i), $c_{j}=\pi_{j}$ for $j\in[n]$, and $\mathcal{C}=\mathcal{C}_{Y}$ is the set required there. In the case of (ii), an element of $J=[p]\times[q]$ is a pair $(i,j)$ with $i\in[p]$ and $j\in[q]$, by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i), and $c_{(i,j)}=E_{ij}$; so $C=c_{l}^{-1}(B)$ for some $l\in J$ if and only if $C=E_{ij}^{-1}(B)$ for some $i\in[p]$ and $j\in[q]$, and $\mathcal{C}'=\mathcal{C}_{Y}$ is the set required there.