Kit for def:complete-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 set variables listed in Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{N}$, $\mathbb{R}$, the order $\le$, the strict order $<$, the addition $+$ and the element $0$ of $\mathbb{R}$ are parameters. Metric spaces and metrics are as in Metric Space (vi) and Metric Space (i), and complete metric spaces as in Complete Metric Space (i). In the first clause $X=x_{i}$ and $d=x_{j}$.

(i) Complete metric spaces. The condition "$\Gamma$, and $(X,d)$ is complete" on $x_{0},\dots,x_{n-1}$, where $\Gamma$ is "$d$ is a map from the Cartesian product $X\times X$ to $\mathbb{R}$, and $(X,d)$ is a metric space", is predicative.

(ii) The class of complete 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 complete.