Kit for def:separable-metric

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,l<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 natural numbers, $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ are parameters. Below, in (i), $X=x_{i}$ and $d=x_{j}$, and $\Gamma_{1}$ is the standing hypothesis of Separable Metric Space and Separable Real Normed Space: "$d$ is a map from the Cartesian product $X\times X$ to $\mathbb{R}$, and $(X,d)$ is a metric space"; in (ii), $V=x_{i}$, the addition of $V$ is $x_{j}$, its scalar multiplication is $x_{k}$ and $\lVert\cdot\rVert=x_{l}$, and $\Gamma_{2}$, the hypothesis of Separable Metric Space and Separable Real Normed Space (ii), is: "$V$, with addition $x_{j}$ and scalar multiplication $x_{k}$, is a real vector space, $\lVert\cdot\rVert$ is a function from $V$ to $\mathbb{R}$, and $(V,\lVert\cdot\rVert)$ is a real normed space".

(i) Separable metric spaces. The condition "$\Gamma_{1}$, and $(X,d)$ is separable" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Separable real normed spaces. The condition "$\Gamma_{2}$, and $V$ is separable" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) The class of separable metrics. For every set $X$ there is a class $S$ such that, for every class $d$, $d\in S$ if and only if $d$ is a map from $X\times X$ to $\mathbb{R}$ that is a metric on $X$ and $(X,d)$ is separable.