Kit for def: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<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 variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{R}$, $+$, $0$ and $\le$ are parameters. Below, $X=x_{i}$ and $d=x_{j}$, and $\Gamma$ is the standing hypothesis of Metric Space: "$d$ is a map from the Cartesian product $X\times X$ to $\mathbb{R}$".

(i) Nonnegativity. The condition "$\Gamma$, and $0\le d(x,y)$ for all $x,y\in X$" on $x_{0},\dots,x_{n-1}$, from Metric Space (ii), is predicative.

(ii) Vanishing exactly on the diagonal. The condition "$\Gamma$, and, for all $x,y\in X$, $d(x,y)=0$ if and only if $x=y$" on $x_{0},\dots,x_{n-1}$, from Metric Space (iii), is predicative.

(iii) Symmetry. The condition "$\Gamma$, and $d(x,y)=d(y,x)$ for all $x,y\in X$" on $x_{0},\dots,x_{n-1}$, from Metric Space (iv), is predicative.

(iv) Triangle inequality. The condition "$\Gamma$, and $d(x,z)\le d(x,y)+d(y,z)$ for all $x,y,z\in X$" on $x_{0},\dots,x_{n-1}$, from Metric Space (v), is predicative.

(v) Metrics. The condition "$\Gamma$, and $d$ is a metric on $X$" on $x_{0},\dots,x_{n-1}$ is predicative.

(vi) Metric spaces. The condition "$\Gamma$, and $(X,d)$ is a metric space" on $x_{0},\dots,x_{n-1}$ is predicative.

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