Proof of Kit for def:complete-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. For sets $r$ and $r'$, $r\le r'$ and $r<r'$ stand for $(r,r')\in{\le}$ and $(r,r')\in{<}$. The letters $\varepsilon$, $N$, $m$, $\ell$, $a$, $b$ and $t$ denote set variables, distinct from one another, from $x_{0},x_{1},\dots$ and from the parameters. 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 metrics on a set and sequences in a set; and a one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)).

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) and Convergent Sequence in a Metric Space (ii), 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). Likewise Cauchy Sequence in a Metric Space (i), which Complete Metric Space (i) cites, is stated for the first two of these readings, so it applies to the current ones by the same bridge clauses.

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)); its bound variables are chosen other than the letters above. So $\rho$ expresses $\Gamma$ with $X=x_{0}$ and $d=x_{1}$; the first part of $\Gamma$ is the standing hypothesis of Metric Space, and the second that of Complete Metric Space.

Sequences. Let $\mu(F,A,B)$ be the formula of 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), its auxiliary set variables $p$, $u$, $u'$, $v$ and $v'$ pairwise distinct and distinct from $x_{0},x_{1},\dots$, from the letters above 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. So, for sets $X$ and $s$ assigned to $x_{0}$ and $x_{2}$, $\mu(x_{2},\mathbb{N},x_{0})$ holds if and only if $s$ is a map $s:\mathbb{N}\to X$, that is, a sequence in $X$ (Sequences (i)).

The formula for Cauchy sequences. Let

$$\beta(x_{1},x_{2})=\forall\varepsilon\,\Bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists N\,\Bigl(N\in\mathbb{N}\wedge\forall m\,\forall\ell\,\Bigl((m\in\mathbb{N}\wedge\ell\in\mathbb{N}\wedge N\le m\wedge N\le\ell)\Rightarrow\forall a\,\forall b\,\forall t\,\bigl(((m,a)\in x_{2}\wedge(\ell,b)\in x_{2}\wedge((a,b),t)\in x_{1})\Rightarrow t<\varepsilon\bigr)\Bigr)\Bigr)\Bigr).$$

Let sets $X$, $d$ and $s$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$, such that $(X,d)$ is a metric space and $s$ is a sequence in $X$. Let $m,\ell\in\mathbb{N}$. As $s$ is a function with domain $\mathbb{N}$, for every set $a$ we have $(m,a)\in s$ if and only if $a=s(m)$, and likewise $(\ell,b)\in s$ if and only if $b=s(\ell)$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)). As $s(m),s(\ell)\in X$, the pair $(s(m),s(\ell))$ lies in $X\times X=\operatorname{dom}d$ (Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i)), so, by the same clause, $((s(m),s(\ell)),t)\in d$ holds exactly for $t=d(s(m),s(\ell))$, a real number. Hence the premise of the innermost implication holds for exactly one triple of sets, namely

$$a=s(m),\qquad b=s(\ell),\qquad t=d(s(m),s(\ell)),$$

and the formula $\forall a\,\forall b\,\forall t\,(\dots)$ holds if and only if $d(s(m),s(\ell))<\varepsilon$. On elements of $\mathbb{N}$ the order $\le$ of $\mathbb{R}$ agrees with the order of $\mathbb{N}$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (vi)). So $\beta$ holds if and only if for every real number $\varepsilon>0$ there is $N\in\mathbb{N}$ with

$$d(s(m),s(\ell))<\varepsilon\qquad\text{for all }m,\ell\in\mathbb{N}\text{ with }m\ge N\text{ and }\ell\ge N,$$

that is, by Cauchy Sequence in a Metric Space (i), if and only if $s$ is a Cauchy sequence in $(X,d)$.

The formula for convergent sequences. Let $\gamma(x_{0},x_{1},x_{2})$ be the formula $\exists x_{3}\,\kappa(x_{0},x_{1},x_{2},x_{3})$ of Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (ii), 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$ (which occur bound only), and $z'$ any further set variable, distinct from one another, from $x_{0},x_{1},\dots$ and from the parameters, and the auxiliary variables of $\mu$ in it chosen as above. It is predicative, and its free variables are $x_{0}$, $x_{1}$, $x_{2}$ and the parameters $\mathbb{N}$, $\mathbb{R}$, $\le$, $<$ and $0$. Let sets $X$, $d$ and $s$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$, such that $(X,d)$ is a metric space. Then Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (ii), applied to this metric space as the values of its parameters (a statement holds for all values of its parameters satisfying its hypotheses, Conditions Expressed by a Predicative Formula, and Guards (i)), says that $\gamma$ holds if and only if $s$ is a sequence in $X$ that is convergent in $(X,d)$.

The formula for completeness. Let

$$\varphi(x_{0},x_{1})=\rho(x_{0},x_{1})\wedge\forall x_{2}\,\bigl((\mu(x_{2},\mathbb{N},x_{0})\wedge\beta(x_{1},x_{2}))\Rightarrow\gamma(x_{0},x_{1},x_{2})\bigr).$$

It is predicative: $\beta$ is, as no quantifier in it is applied to a class variable (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)), and $\varphi$ is built from $\beta$ and the predicative formulas $\rho$, $\mu$ and $\gamma$ by connectives and a quantifier over a set variable (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), and its free variables are $x_{0}$, $x_{1}$ and the parameters $\mathbb{N}$, $\mathbb{R}$, $\le$, $<$, $+$ and $0$. Let sets $X$ and $d$ be assigned to $x_{0}$ and $x_{1}$. If $\Gamma$ fails, then $\rho$ fails, so $\varphi$ fails. If $\Gamma$ holds, then $(X,d)$ is a metric space and $\rho$ holds. The quantifier $\forall x_{2}$ ranges over sets (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv)), among them every sequence in $X$. For a set $s$ that is not a sequence in $X$ the premise $\mu(x_{2},\mathbb{N},x_{0})$ fails; for a sequence $s$ in $X$, by the above, the premise holds if and only if $s$ is a Cauchy sequence in $(X,d)$, and the conclusion holds if and only if $s$ is convergent in $(X,d)$. Hence the second conjunct of $\varphi$ holds if and only if every Cauchy sequence in $(X,d)$ is convergent in $(X,d)$, that is, if and only if $(X,d)$ is complete (Complete Metric Space (i)). In both cases $\varphi$ holds if and only if $\Gamma$ holds and $(X,d)$ is complete. So $\varphi$ is a predicative formula in $x_{0},x_{1}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing the condition of (i) with $X=x_{0}$ and $d=x_{1}$.

Complete metric spaces. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $2$ and $\sigma(0)=i$ and $\sigma(1)=j$, the formula $\varphi(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 $\varphi$ holds with $x_{0}$ and $x_{1}$ assigned the sets assigned to $x_{i}$ and $x_{j}$, that is, exactly when $\Gamma$ holds and $(X,d)$ is complete, with $X=x_{i}$ and $d=x_{j}$. This proves (i).

The class of complete metrics. For a set $X$, The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi$ with its abbreviations eliminated, with $x_{1}$ as its single variable and $x_{0}$ and the parameters of the statement as its parameters, $x_{0}$ being assigned $X$, gives a class $S$ such that, for every class $d$, $d\in S$ if and only if $d$ is a map $d:X\times X\to\mathbb{R}$ that is a metric on $X$ with $(X,d)$ complete (for such a map, $(X,d)$ is a metric space exactly when $d$ is a metric on $X$, Metric Space (vi)). This proves (ii).