Kit for def:open-subset-metric-space

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, 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; $\mathbb{R}$, the addition $+$, the element $0$ and the order $\le$ of $\mathbb{R}$ are parameters. Metric spaces are as in Metric Space (vi), subsets as in Subclasses and Subsets (i), and open subsets as in Open Subset of a Metric Space (i). In the first clause $X=x_{i}$, $d=x_{j}$ and $U=x_{k}$.

(i) Open subsets. The condition "$(X,d)$ is a metric space, $U\subseteq X$, and $U$ is open in $(X,d)$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) The class of open subsets. For every metric space $(X,d)$ there is a class $C$ such that, for every class $U$, $U\in C$ if and only if $U\subseteq X$ and $U$ is open in $(X,d)$.