Kit for def:borel-sigma-algebra-metric

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, 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. A condition on $x_{0},\dots,x_{n-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the set variables listed in Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), $\mathbb{R}$, the addition $+$, the element $0$ and the order $\le$ of $\mathbb{R}$ are parameters. Metric spaces are as in Metric Space (vi), the set $\mathcal{T}_{d}$ of subsets of $X$ that are open in $(X,d)$ as in The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula (ii), and the Borel $\sigma$-algebra $\mathcal{B}(X,d)$ as in Borel Sigma-Algebra of a Metric Space (i). In both clauses $X=x_{i}$ and $d=x_{j}$, and "$(X,d)$ is a metric space" includes the standing hypothesis of Metric Space (vi) that $d$ is a map from the Cartesian product $X\times X$ to $\mathbb{R}$.

(i) The set of open subsets. With $T=x_{k}$, the condition "$(X,d)$ is a metric space and $T=\mathcal{T}_{d}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) The Borel $\sigma$-algebra. With $B=x_{k}$, the condition "$(X,d)$ is a metric space and $B=\mathcal{B}(X,d)$" on $x_{0},\dots,x_{n-1}$ is predicative.