Proof of Kit for def:continuous-map-metric-spaces

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},\dots,x_{6}$ are distinct also when $n<7$. The parameters $\mathbb{R}$, $+$, $0$ and $\le$ are variables other than $x_{0},x_{1},\dots$ and other than the bound variables below, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); $0$ is a set, being an element of $\mathbb{R}$. For sets $g$ and $h$, $g<h$ abbreviates $(g,h)\in{\le}\wedge\neg\,g=h$, the strict order of $\mathbb{R}$. The letters $\varepsilon,\delta,w,y,t,a,b,s$ denote further 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 subclasses of sets (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)) and 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 a one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)).

The formulas. Write $X$, $d_{X}$, $Y$, $d_{Y}$, $A$, $f$ and $x$ for $x_{0},\dots,x_{6}$. For arbitrary sets, "$(X,d_{X})$ is a metric space" includes the standing hypothesis of Metric Space that $d_{X}$ is a map from the Cartesian product $X\times X$ to $\mathbb{R}$, and likewise for $(Y,d_{Y})$. By Kit for def:metric-space (vi) with $n=4$, applied once with $i=0$ and $j=1$ and once with $i=2$ and $j=3$, there are predicative formulas $\rho_{X}$ and $\rho_{Y}$ in $x_{0},\dots,x_{3}$, with parameters among $\mathbb{R}$, $+$, $0$ and $\le$, expressing "$d_{X}$ is a map $X\times X\to\mathbb{R}$ and $(X,d_{X})$ is a metric space" and "$d_{Y}$ is a map $Y\times Y\to\mathbb{R}$ and $(Y,d_{Y})$ is a metric space"; their bound variables are chosen other than the letters above, and they are also predicative formulas in $x_{0},\dots,x_{5}$ and in $x_{0},\dots,x_{6}$ (Renaming and Substituting Variables in Predicative Formulas (ii)). Let $\mu(f,A,Y)$ 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) with $x_{5}$, $x_{4}$ and $x_{2}$ as its $F$, $A$ and $B$ and with its auxiliary set variables chosen pairwise distinct and distinct from $x_{0},x_{1},\dots$, from the letters above and from the parameters; it is predicative, its free variables are $x_{2}$, $x_{4}$ and $x_{5}$, and for sets $f$, $A$ and $Y$ it holds if and only if $f$ is a map $f:A\to Y$. Let

$$\alpha=\forall w\,(w\in A\Rightarrow w\in X),$$ $$\kappa=\forall\varepsilon\,\Bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists\delta\,\Bigl(\delta\in\mathbb{R}\wedge0<\delta\wedge\forall y\,\Bigl(y\in A\Rightarrow\forall t\,\forall a\,\forall b\,\forall s\,\bigl((((x,y),t)\in d_{X}\wedge t<\delta\wedge(y,a)\in f\wedge(x,b)\in f\wedge((a,b),s)\in d_{Y})\Rightarrow s<\varepsilon\bigr)\Bigr)\Bigr)\Bigr),$$ $$\varphi=\rho_{X}\wedge\rho_{Y}\wedge\alpha\wedge\mu(f,A,Y)\wedge x\in A\wedge\kappa, \qquad \psi=\rho_{X}\wedge\rho_{Y}\wedge\alpha\wedge\mu(f,A,Y)\wedge\forall x\,(x\in A\Rightarrow\kappa),$$

where in $\psi$ the quantified $x$ is the variable $x_{6}$. No quantifier in $\alpha$ or $\kappa$ is applied to a class variable, so they are predicative (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)), and $\varphi$ and $\psi$ are predicative, being built from predicative formulas by conjunction, implication and quantification over set variables (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)). The free variables of $\varphi$ are among $x_{0},\dots,x_{6}$ and the parameters; those of $\psi$ are among $x_{0},\dots,x_{5}$ and the parameters, since $x_{6}$ is free in neither $\rho_{X}$, $\rho_{Y}$, $\alpha$ nor $\mu(f,A,Y)$.

What $\kappa$ says. Let sets $X$, $d_{X}$, $Y$, $d_{Y}$, $A$, $f$ and $x$ be assigned to $x_{0},\dots,x_{6}$, and suppose that $(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces, with $d_{X}:X\times X\to\mathbb{R}$ and $d_{Y}:Y\times Y\to\mathbb{R}$, that $A\subseteq X$, that $f:A\to Y$ and that $x\in A$. Let $\varepsilon$ and $\delta$ be real numbers and let $y\in A$. Then $x,y\in X$, so the pair $(x,y)$ lies in $X\times X=\operatorname{dom}d_{X}$ (Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i)), and, $d_{X}$ being a function, $((x,y),t)\in d_{X}$ holds exactly for $t=d_{X}(x,y)$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)). Likewise, as $x,y\in A=\operatorname{dom}f$, $(y,a)\in f$ holds exactly for $a=f(y)$ and $(x,b)\in f$ exactly for $b=f(x)$; these values lie in $Y$, so $(f(y),f(x))\in Y\times Y=\operatorname{dom}d_{Y}$, and $((f(y),f(x)),s)\in d_{Y}$ holds exactly for $s=d_{Y}(f(y),f(x))$. Hence the antecedent of the innermost implication of $\kappa$ fails unless $t$, $a$, $b$ and $s$ are these values, and for them it reduces to $t<\delta$. So the part of $\kappa$ beginning with $\forall t$ holds if and only if

$$d_{X}(x,y)<\delta\ \Rightarrow\ d_{Y}(f(y),f(x))<\varepsilon.$$

So $\kappa$ says that for every real $\varepsilon>0$ there is a real $\delta>0$ such that every $y\in A$ with $d_{X}(x,y)<\delta$ satisfies $d_{Y}(f(y),f(x))<\varepsilon$, that is, by Continuous Map Between Metric Spaces (i), that $f$ is continuous at $x$ relative to $A$.

What $\varphi$ and $\psi$ say. Let sets $X$, $d_{X}$, $Y$, $d_{Y}$, $A$, $f$ and $x$ be assigned to $x_{0},\dots,x_{6}$. The conjuncts $\rho_{X}$, $\rho_{Y}$, $\alpha$, $\mu(f,A,Y)$ and $x\in A$ hold exactly when $(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces with $d_{X}:X\times X\to\mathbb{R}$ and $d_{Y}:Y\times Y\to\mathbb{R}$, $A\subseteq X$ (Subclasses and Subsets (i)), $f:A\to Y$ and $x\in A$. If one of them fails, $\varphi$ fails, and so does the condition

$$(X,d_{X}),\,(Y,d_{Y})\text{ are metric spaces},\quad A\subseteq X,\quad f:A\to Y,\quad x\in A,\quad f\text{ is continuous at }x\text{ relative to }A.$$

If all of them hold, then $\varphi$ holds exactly when $\kappa$ does, that is, by the previous paragraph, exactly when the displayed condition holds. So $\varphi$ is a predicative formula in $x_{0},\dots,x_{6}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing the displayed condition. Similarly, under an assignment of sets $X$, $d_{X}$, $Y$, $d_{Y}$, $A$ and $f$ to $x_{0},\dots,x_{5}$, if the metric-space, subset and map conditions hold, then for every set $x'$ assigned to $x_{6}$ with $x'\in A$ the previous paragraph applies, so $\forall x\,(x\in A\Rightarrow\kappa)$ says that $f$ is continuous at $x'$ relative to $A$ for every $x'\in A$, that is, by Continuous Map Between Metric Spaces (ii), that $f$ is continuous on $A$; and if one of them fails, $\psi$ fails. So $\psi$ is a predicative formula in $x_{0},\dots,x_{5}$ expressing the condition "$(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces, $A\subseteq X$, $f:A\to Y$ and $f$ is continuous on $A$".

Continuity at a point. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $7$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, $\sigma(3)=l$, $\sigma(4)=m$, $\sigma(5)=p$ and $\sigma(6)=q$, the formula $\varphi(x_{i},x_{j},x_{k},x_{l},x_{m},x_{p},x_{q})$ 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 the condition of (i) holds for $X=x_{i}$, $d_{X}=x_{j}$, $Y=x_{k}$, $d_{Y}=x_{l}$, $A=x_{m}$, $f=x_{p}$ and $x=x_{q}$. This proves (i).

Continuity at a point of the space. Apply Renaming and Substituting Variables in Predicative Formulas (i) as in the previous paragraph, but with $\sigma(4)=i$. The formula $\varphi(x_{i},x_{j},x_{k},x_{l},x_{i},x_{p},x_{q})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when the displayed condition holds with $A=X$. As $X\subseteq X$ always, and continuity at $x$ relative to $X$ is continuity at $x$ (Continuous Map Between Metric Spaces (i)), this is the condition of (ii), which is therefore predicative.

Continuity on a subset. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $6$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, $\sigma(3)=l$, $\sigma(4)=m$ and $\sigma(5)=p$, the formula $\psi(x_{i},x_{j},x_{k},x_{l},x_{m},x_{p})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ expressing the condition of (iii). This proves (iii).

Continuous maps. The same, with $\sigma(4)=i$, gives the predicative formula $\psi(x_{i},x_{j},x_{k},x_{l},x_{i},x_{p})$, which expresses the condition with $A=X$; as $X\subseteq X$ and continuity on $X$ is continuity (Continuous Map Between Metric Spaces (ii)), this is the condition of (iv). This proves (iv).

The class of maps continuous at a point. Let $(X,d_{X})$ and $(Y,d_{Y})$ be metric spaces, let $A\subseteq X$ and let $x\in A$; then $X$, $d_{X}$, $Y$, $d_{Y}$, $A$ and $x$ are sets. Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\varphi$ with its abbreviations eliminated, with $x_{5}$ as its single variable and $x_{0}$, $x_{1}$, $x_{2}$, $x_{3}$, $x_{4}$, $x_{6}$, $\mathbb{R}$, $+$, $0$ and $\le$ as its parameters, $x_{0},x_{1},x_{2},x_{3},x_{4},x_{6}$ being assigned $X$, $d_{X}$, $Y$, $d_{Y}$, $A$ and $x$. It gives a class $C$ whose elements are exactly the sets $f$ for which $\varphi$ holds with $f$ assigned to $x_{5}$, that is, as the metric-space, subset and membership conditions hold, the sets $f$ with $f:A\to Y$ continuous at $x$ relative to $A$. This proves (v).

The class of maps of the space continuous at a point. Let $(X,d_{X})$ and $(Y,d_{Y})$ be metric spaces and let $x\in X$. As $X\subseteq X$, (v) with $A=X$ gives a class $C$ such that, for every class $f$, $f\in C$ if and only if $f:X\to Y$ is continuous at $x$ relative to $X$, that is, continuous at $x$ (Continuous Map Between Metric Spaces (i)). This proves (vi).

The class of maps continuous on a subset. For metric spaces $(X,d_{X})$ and $(Y,d_{Y})$ and $A\subseteq X$, The Class Comprehension Theorem for Predicative Formulas (i), applied to $\psi$ with its abbreviations eliminated, with $x_{5}$ as its single variable and $x_{0},\dots,x_{4}$ (assigned $X$, $d_{X}$, $Y$, $d_{Y}$ and $A$), $\mathbb{R}$, $+$, $0$ and $\le$ as its parameters, gives a class $C$ whose elements are exactly the maps $f:A\to Y$ that are continuous on $A$, which proves (vii).

The class of continuous maps. Let $(X,d_{X})$ and $(Y,d_{Y})$ be metric spaces. As $X\subseteq X$, (vii) with $A=X$ gives a class $C$ such that, for every class $f$, $f\in C$ if and only if $f:X\to Y$ is continuous on $X$, that is, continuous (Continuous Map Between Metric Spaces (ii)). This proves (viii).