Kit for def:convergent-sequence-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,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; $\mathbb{N}$, $\mathbb{R}$, the order $\le$, the strict order $<$, the addition $+$ and the element $0$ of $\mathbb{R}$ are parameters. Metric spaces are as in Metric Space (vi), sequences as in Sequences (i), and convergence to a point and convergent sequences as in Convergent Sequence in a Metric Space (i) and Convergent Sequence in a Metric Space (ii). In the first two clauses $X=x_{i}$ and $d=x_{j}$.

(i) Convergence. The condition "$(X,d)$ is a metric space, $x_{k}$ is a sequence in $X$, $x_{l}\in X$, and $x_{k}$ converges to $x_{l}$ in $(X,d)$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Convergent sequences. The condition "$(X,d)$ is a metric space and $x_{k}$ is a sequence in $X$ that is convergent in $(X,d)$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) The class of sequences converging to a point. For every metric space $(X,d)$ and every $x\in X$ there is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is a sequence in $X$ that converges to $x$ in $(X,d)$.

(iv) The class of convergent sequences. For every metric space $(X,d)$ there is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is a sequence in $X$ that is convergent in $(X,d)$.