Kit for def:convergent-sequence-nbg

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{N}$, $\mathbb{R}$, the order $\le$, the strict order $<$ and the element $0$ of $\mathbb{R}$, and the distance $d_{\mathbb{R}}$ on $\mathbb{R}$ are parameters. Sequences are as in Sequences (i), and convergence, convergent sequences and null sequences as in Convergent Sequences of Real Numbers (i), Convergent Sequences of Real Numbers (ii) and Convergent Sequences of Real Numbers (iii).

(i) Convergence. The condition "$x_{i}$ is a sequence in $\mathbb{R}$, $x_{j}\in\mathbb{R}$, and $x_{i}$ converges to $x_{j}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Convergent sequences. The condition "$x_{i}$ is a convergent sequence in $\mathbb{R}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) Null sequences. The condition "$x_{i}$ is a null sequence in $\mathbb{R}$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iv) The class of convergent sequences. There is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is a convergent sequence in $\mathbb{R}$.

(v) The class of null sequences. There is a class $Z$ such that, for every class $a$, $a\in Z$ if and only if $a$ is a null sequence in $\mathbb{R}$.