Proof of Kit for def:convergent-sequence-metric-space

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, 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_{0},x_{1},x_{2},x_{3}$ are distinct also when $n<4$. The parameters are those of the statement, variables other than $x_{0},x_{1},\dots$, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i): $\mathbb{N}$, $\mathbb{R}$, $\le$, $<$, $+$ and $0$ are those of the setting of the statement, which are also those of the lemmas applied below. Routine set bookkeeping is used without comment: elements of classes are sets (Classes, Membership, Sets and Proper Classes (i)), and so are maps $f:A\to B$ between sets, which lie in the class $B^{A}$ of functions from $A$ to $B$ (Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), in particular both components of a metric space (Metric Space) and the sequences in a set; and a one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)).

The formula for metric spaces. By Kit for def:metric-space (vi) with $n=2$, $i=0$ and $j=1$, there is a predicative formula $\rho(x_{0},x_{1})$ in $x_{0},x_{1}$, with parameters among $\mathbb{R}$, $+$, $0$ and $\le$, that holds, under every assignment of sets to $x_{0}$ and $x_{1}$, if and only if $x_{1}$ is a map $x_{0}\times x_{0}\to\mathbb{R}$ and $(x_{0},x_{1})$ is a metric space (Metric Space (vi)). For arbitrary sets, "$(X,d)$ is a metric space" includes the standing hypothesis of Metric Space that $d$ is a map from the Cartesian product $X\times X$ to $\mathbb{R}$, so $\rho$ expresses it with $X=x_{0}$ and $d=x_{1}$.

Earlier readings. The helper Predicative Formulas for Convergence and Limits, and Maps Defined by Limits applied below is stated for the readings Metric Space (vi), Sequences (i), Convergent Sequence in a Metric Space (i) and Convergent Sequence in a Metric Space (ii); they 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).

The formula for convergence. Apply Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i) with the set variables $x_{0}$ and $x_{1}$ as its parameters $X$ and $d$, $x_{2}$ as its variable $s$, $x_{3}$ as its variable $z$, and its variables $\varepsilon$, $N$ and $m$, and $z'$ any further set variable, distinct from one another, 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$, from $\varepsilon$, $N$ and $m$, and from the parameters; with $x_{2}$, $\mathbb{N}$ and $x_{0}$ as its $F$, $A$ and $B$, this meets the distinctness hypotheses of that lemma. Let $\kappa(x_{0},x_{1},x_{2},x_{3})$ be the resulting formula; it is predicative, and its free variables are $x_{0},\dots,x_{3}$ and the parameters $\mathbb{N}$, $\mathbb{R}$, $\le$, $<$ and $0$. Let

$$\varphi(x_{0},x_{1},x_{2},x_{3})=\rho(x_{0},x_{1})\wedge\kappa(x_{0},x_{1},x_{2},x_{3}),$$

which is predicative, being a conjunction of predicative formulas (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)). Let sets $X$, $d$, $s$ and $x$ be assigned to $x_{0}$, $x_{1}$, $x_{2}$ and $x_{3}$. If $(X,d)$ is not a metric space, then $\rho$ fails, so $\varphi$ fails, and so does the condition

$$(X,d)\text{ is a metric space},\quad s\text{ is a sequence in }X,\quad x\in X,\quad s\to x\text{ in }(X,d).$$

If $(X,d)$ is a metric space, then $\rho$ holds, and Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (i), applied to this metric space as the values of its parameters $x_{0}$ and $x_{1}$ (a statement holds for all values of its parameters satisfying its hypotheses, Conditions Expressed by a Predicative Formula, and Guards (i)), says that $\kappa$ holds if and only if $s$ is a sequence in $X$, $x\in X$ and $s$ converges to $x$ in $(X,d)$. In both cases $\varphi$ holds if and only if the displayed condition does. So $\varphi$ is a predicative formula in $x_{0},\dots,x_{3}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing the displayed condition with $X,d,s,x$ the sets assigned to $x_{0},\dots,x_{3}$.

Convergence. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $4$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$ and $\sigma(3)=l$, the formula $\varphi(x_{i},x_{j},x_{k},x_{l})$ 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},x_{j})$ is a metric space, $x_{k}$ is a sequence in $x_{i}$, $x_{l}\in x_{i}$ and $x_{k}$ converges to $x_{l}$ in $(x_{i},x_{j})$. This proves (i).

Convergent sequences. Let

$$\psi(x_{0},x_{1},x_{2})=\rho(x_{0},x_{1})\wedge\exists x_{3}\,\kappa(x_{0},x_{1},x_{2},x_{3}).$$

With the choice of variables made above, $\exists x_{3}\,\kappa$ is the formula $\gamma$ of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (ii), which is predicative; so $\psi$ is predicative, being a conjunction of predicative formulas (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and its free variables are $x_{0}$, $x_{1}$, $x_{2}$ and parameters. Let sets $X$, $d$ and $s$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $(X,d)$ is not a metric space, then $\rho$ fails, and so does $\psi$. If $(X,d)$ is a metric space, then $\rho$ holds, and Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (ii), applied to this metric space as the values of its parameters, says that $\exists x_{3}\,\kappa$ holds if and only if $s$ is a sequence in $X$ that is convergent in $(X,d)$. In both cases $\psi$ holds if and only if $(X,d)$ is a metric space and $s$ is a sequence in $X$ that is convergent in $(X,d)$. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\sigma(0)=i$, $\sigma(1)=j$ and $\sigma(2)=k$, the formula $\psi(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $(x_{i},x_{j})$ is a metric space and $x_{k}$ is a sequence in $x_{i}$ that is convergent in $(x_{i},x_{j})$. This proves (ii).

The class of sequences converging to a point. For a metric space $(X,d)$ and $x\in X$, The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi$ with its abbreviations eliminated, with $x_{2}$ as its single variable and $x_{0}$, $x_{1}$, $x_{3}$ and the parameters of the statement as its parameters, $x_{0}$, $x_{1}$ and $x_{3}$ being assigned $X$, $d$ and $x$, gives 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)$. This proves (iii).

The class of convergent sequences. Likewise, for a metric space $(X,d)$, The Class Comprehension Theorem for Predicative Formulas (i), applied to $\psi$ with its abbreviations eliminated, with $x_{2}$ as its single variable and $x_{0}$, $x_{1}$ and the parameters of the statement as its parameters, $x_{0}$ and $x_{1}$ being assigned $X$ and $d$, gives 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)$. This proves (iv).