Proof of Kit for def:convergent-sequence-nbg

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{1}$ is distinct from $x_{0}$ also when $n=1$. The parameters are those of the statement, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i).

The formula for convergence. The helper Predicative Formulas for Convergence and Limits, and Maps Defined by Limits and the lemma The Absolute Value Metric on the Real Numbers (i) used here are stated for the readings Metric Space (vi), Sequences (i) and Convergent Sequence in a Metric Space (i), which agree with the current ones by The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (i), The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i) and The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (iii). As $d_{\mathbb{R}}$ is a metric on $\mathbb{R}$ (The Absolute Value Metric on the Real Numbers (i)), $(\mathbb{R},d_{\mathbb{R}})$ is a metric space. Apply Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) to it, with $x_{0}$ as its variable $s$, $x_{1}$ as its variable $z$, its parameters $X$ and $d$ taken to be set variables (their values being sets), and its variables $\varepsilon$, $N$ and $m$ distinct from $x_{0},x_{1},\dots$ and from the parameters. In its formula take the auxiliary set variables $p$, $u$, $u'$, $v$ and $v'$ of $\mu$ from Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii) pairwise distinct and distinct from $x_{0},x_{1},\dots$ (among them $s=x_{0}$ and $z=x_{1}$), from $\varepsilon$, $N$ and $m$, and from the parameters; with $s$, $\mathbb{N}$ and $X$ as its $F$, $A$ and $B$, this meets the distinctness hypotheses of that lemma. Let $\kappa(x_{0},x_{1})$ be the resulting formula with the parameter $\mathbb{R}$ put for $X$ and $d_{\mathbb{R}}$ put for $d$. By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i) applied to $\kappa$ with its abbreviations eliminated, with $k=2$, $X$ and $d$ as its $v_{1}$ and $v_{2}$, and the parameters $\mathbb{R}$ and $d_{\mathbb{R}}$ as its $y_{1}$ and $y_{2}$ (their values are sets, $d_{\mathbb{R}}$ being a map between sets, Sets and Maps: Ordinary Notation (iv) and Sets and Maps: Ordinary Notation (v)), $\kappa$ is predicative and holds exactly when the formula of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) holds with $X$ given the value $\mathbb{R}$ and $d$ the value $d_{\mathbb{R}}$, the other variables keeping their values. So the free variables of $\kappa$ are $x_{0}$, $x_{1}$ and parameters of the statement, and, for all sets $x_{0}$ and $x_{1}$, it holds if and only if $x_{0}$ is a map $\mathbb{N}\to\mathbb{R}$, that is, a sequence in $\mathbb{R}$ (Sequences (i)), $x_{1}\in\mathbb{R}$, and $x_{0}$ converges to $x_{1}$ in $(\mathbb{R},d_{\mathbb{R}})$. By Convergent Sequence in a Metric Space (i) the last condition says that for every real $\varepsilon>0$ there is $N\in\mathbb{N}$ with

$$d_{\mathbb{R}}(x_{0}(m),x_{1})=|x_{0}(m)-x_{1}|<\varepsilon\qquad\text{for every }m\in\mathbb{N}\text{ with }m\ge N,$$

the equality being The Distance on the Real Numbers (i); this is the condition of Convergent Sequences of Real Numbers (i) for the sequence $x_{0}$, whose $m$-th term is $x_{0}(m)$, and $L=x_{1}$. Hence $\kappa(x_{0},x_{1})$ holds if and only if $x_{0}$ is a sequence in $\mathbb{R}$, $x_{1}\in\mathbb{R}$, and $x_{0}$ converges to $x_{1}$; so $\kappa$ is a predicative formula in $x_{0},x_{1}$ in the sense of Renaming and Substituting Variables in Predicative Formulas.

Convergence. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=2$, $\sigma(0)=i$ and $\sigma(1)=j$, the formula $\kappa(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{i}$ is a sequence in $\mathbb{R}$, $x_{j}\in\mathbb{R}$, and $x_{i}$ converges to $x_{j}$. This proves (i).

Convergent sequences. Let $\gamma(x_{0})$ be the formula $\exists x_{1}\,\kappa(x_{0},x_{1})$, the formula of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (ii) with the same replacements; it is predicative, and its only free variable other than the parameters is $x_{0}$. For a set $x_{0}$, $\gamma(x_{0})$ holds if and only if there is a set $x_{1}$ such that $x_{0}$ is a sequence in $\mathbb{R}$, $x_{1}\in\mathbb{R}$ and $x_{0}$ converges to $x_{1}$. This says that $x_{0}$ is a sequence in $\mathbb{R}$ that converges to some real number (elements of $\mathbb{R}$ are sets, being elements of a class, Classes, Membership, Sets and Proper Classes (i)), that is, by Convergent Sequences of Real Numbers (ii), a convergent sequence in $\mathbb{R}$. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, the formula $\gamma(x_{i})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}$ is a convergent sequence in $\mathbb{R}$. This proves (ii).

Null sequences. By Renaming and Substituting Variables in Predicative Formulas (iii) with $k=2$, $\tau_{0}=x_{i}$ and $\tau_{1}=0$ (the value of the parameter $0$ is the zero of $\mathbb{R}$, a set, Classes, Membership, Sets and Proper Classes (i)), the formula $\kappa(x_{i},0)$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}$ is a sequence in $\mathbb{R}$, $0\in\mathbb{R}$ and $x_{i}$ converges to $0$, that is, by Convergent Sequences of Real Numbers (iii), exactly when $x_{i}$ is a null sequence in $\mathbb{R}$. This proves (iii).

The classes. Take $n=1$ and $i=0$ above, so that $\gamma(x_{0})$ and $\kappa(x_{0},0)$ are predicative formulas in $x_{0}$ expressing that $x_{0}$ is a convergent sequence, respectively a null sequence, in $\mathbb{R}$. Then The Class Comprehension Theorem for Predicative Formulas (i), applied to $\gamma(x_{0})$ with $x_{0}$ as its single variable and the parameters of the statement as its parameters, gives a class $C$ such that, for every class $a$, $a\in C$ if and only if $a$ is a convergent sequence in $\mathbb{R}$ (every sequence in $\mathbb{R}$, a map $\mathbb{N}\to\mathbb{R}$, is a set, being an element of the class $\mathbb{R}^{\mathbb{N}}$ of functions from $\mathbb{N}$ to $\mathbb{R}$, and a class is a set exactly when it is an element of a class: The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), Classes, Membership, Sets and Proper Classes (i); the one-entry tuple $\langle a\rangle$ is $a$, The Ordered Pair of Two Sets and Nested Tuples (ii)). This proves (iv). The same argument with $\kappa(x_{0},0)$ in place of $\gamma(x_{0})$ and null sequences in place of convergent sequences gives a class as required by (v), in the role of its $Z$.