The Borel Sets of ℝⁿ, Lebesgue Measure on ℝⁿ and Integrals against It Are Predicative in the Dimension

In the setting of Product Measures and Lebesgue Measure on ℝⁿ: Standing Notation and Background, assume the axiom of dependent choice; this item is a statement of the metatheory. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k<N$, not necessarily distinct. Each clause states that a condition on $x_{0},\dots,x_{N-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables. The other letters, among them the sets of numbers and $[0,\infty]$ with their operations and orders, are parameters. For $n\in\mathbb{N}$, $\mathbb{R}^{n}$ is Euclidean space, $\mathcal{B}(\mathbb{R}^{n})$ its Borel $\sigma$-algebra, $\lambda_{n}$ Lebesgue measure on $\mathbb{R}^{n}$, and $\mathcal{M}^{+}(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ and $\int_{\mathbb{R}^{n}}g\,d\lambda_{n}$ are as in the setting.

(i) Borel sets. With $n=x_{i}$ and $\mathcal{G}=x_{j}$: "$n\in\mathbb{N}$ and $\mathcal{G}=\mathcal{B}(\mathbb{R}^{n})$".

(ii) Lebesgue measure. With $n=x_{i}$ and $\kappa=x_{j}$: "$n\in\mathbb{N}$ and $\kappa=\lambda_{n}$".

(iii) Integrals against Lebesgue measure. With $n=x_{i}$, $g=x_{j}$ and $r=x_{k}$: "$n\in\mathbb{N}$, $g\in\mathcal{M}^{+}(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ and $r=\int_{\mathbb{R}^{n}}g\,d\lambda_{n}$".