Proof of Kit for def:metric-space

Throughout, formulas are written with abbreviations and quantify over set variables only, so they are predicative. The parameters $\mathbb{R}$, $+$, $0$ and $\le$ are variables other than $x_{0},\dots,x_{n-1}$ and $x_{1}$ and other than the bound variables below; $0$ is a set, being an element of $\mathbb{R}$, and $+$ and $\le$ are sets, being a map from $\mathbb{R}\times\mathbb{R}$ to $\mathbb{R}$ and a subclass of $\mathbb{R}\times\mathbb{R}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), 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)). Elements of classes are sets (Classes, Membership, Sets and Proper Classes (i)), and a one-entry tuple $\langle d\rangle$ is $d$ (The Ordered Pair of Two Sets and Nested Tuples (ii)). We first build formulas in $x_{0}$ and $x_{1}$, written $X$ and $d$, and move them to the positions $i$ and $j$ at the end. The letters $x,y,z,u,v,v',p,c,r,s,t,q$ denote further set variables.

The standing hypothesis. For variables $A$ and $B$ let $\pi(c,A,B)$ be the formula $\forall p\,\bigl(p\in c\Leftrightarrow\exists u\,\exists v\,(u\in A\wedge v\in B\wedge p=(u,v))\bigr)$. For a set $X$, the only set $c$ with $\pi(c,X,X)$ is the Cartesian product $X\times X$, which is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii). 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), which holds exactly when $F$ is a map $F:A\to B$, and let

$$\gamma=\exists c\,\bigl(\pi(c,X,X)\wedge\mu(d,c,\mathbb{R})\bigr).$$

By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), $\gamma$ holds exactly when $\mu(d,X\times X,\mathbb{R})$ does, that is, exactly when $d$ is a map $d:X\times X\to\mathbb{R}$; so $\gamma$ expresses $\Gamma$.

Assume $\gamma$. Throughout, that pairs of elements of $X$ lie in $X\times X=\operatorname{dom}d$, that values of $d$ lie in $\mathbb{R}$, and that $+$ and $\le$ are a binary operation and a relation on $\mathbb{R}$, are routine facts of the setting. For $x,y\in X$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x), $((x,y),t)\in d$ holds for exactly one set $t$, the value $d(x,y)\in\mathbb{R}$. For $r,s\in\mathbb{R}$, $((r,s),q)\in{+}$ holds exactly for $q=r+s$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), as $+$ is a binary operation on $\mathbb{R}$; and $r\le s$ means $(r,s)\in{\le}$. So in each formula below every premise of these forms singles out exactly one set, which exists, and a universally quantified implication whose premises name values in this way states the property of the named values given in its conclusion (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii)).

The four conditions. Let $\eta_{1},\dots,\eta_{4}$ be the formulas

$$\begin{aligned} &\forall x\,\forall y\,\forall t\,\bigl((x\in X\wedge y\in X\wedge((x,y),t)\in d)\Rightarrow(0,t)\in{\le}\bigr),\\ &\forall x\,\forall y\,\forall t\,\bigl((x\in X\wedge y\in X\wedge((x,y),t)\in d)\Rightarrow(t=0\Leftrightarrow x=y)\bigr),\\ &\forall x\,\forall y\,\forall t\,\forall s\,\bigl((x\in X\wedge y\in X\wedge((x,y),t)\in d\wedge((y,x),s)\in d)\Rightarrow t=s\bigr),\\ &\forall x\,\forall y\,\forall z\,\forall r\,\forall s\,\forall t\,\forall q\,\bigl((x\in X\wedge y\in X\wedge z\in X\wedge((x,z),r)\in d\wedge((x,y),s)\in d\wedge((y,z),t)\in d\wedge((s,t),q)\in{+})\Rightarrow(r,q)\in{\le}\bigr). \end{aligned}$$

Under $\gamma$ their premises name $t=d(x,y)$ in the first and the second; $t=d(x,y)$ and $s=d(y,x)$ in the third; and $r=d(x,z)$, $s=d(x,y)$, $t=d(y,z)$ and $q=d(x,y)+d(y,z)$ in the fourth, where $s,t\in\mathbb{R}$. So, under $\gamma$, $\eta_{1},\dots,\eta_{4}$ state that

$$0\le d(x,y),\qquad d(x,y)=0\iff x=y,\qquad d(x,y)=d(y,x)\qquad\text{for all }x,y\in X,$$ $$d(x,z)\le d(x,y)+d(y,z)\qquad\text{for all }x,y,z\in X.$$

Hence $\gamma\wedge\eta_{1}$, $\gamma\wedge\eta_{2}$, $\gamma\wedge\eta_{3}$ and $\gamma\wedge\eta_{4}$ express the conditions of (i), (ii), (iii) and (iv) with $X=x_{0}$ and $d=x_{1}$.

Metrics and metric spaces. Let $\psi=\gamma\wedge\eta_{1}\wedge\eta_{2}\wedge\eta_{3}\wedge\eta_{4}$. As $X$, a set variable, stands for a set, under $\Gamma$ the set $d$ is a metric on $X$ by Metric Space (i) exactly when the conditions of Metric Space (ii), Metric Space (iii), Metric Space (iv) and Metric Space (v) hold for all $x,y,z\in X$. The first three do not involve $z$, so they hold for all $x,y,z\in X$ exactly when they hold for all $x,y\in X$ (take $z=x$); thus $d$ is a metric on $X$ exactly when the four displayed conditions hold, and $\psi$ expresses the condition of (v). By Metric Space (vi), under $\Gamma$ the pair $(X,d)$ is a metric space exactly when $d$ is a metric on $X$, so $\psi$ also expresses the condition of (vi).

Any positions. Each formula $\varphi$ obtained above, namely $\gamma\wedge\eta_{1}$, $\gamma\wedge\eta_{2}$, $\gamma\wedge\eta_{3}$, $\gamma\wedge\eta_{4}$ and $\psi$, is thus a predicative formula in $x_{0},x_{1}$ in the sense of Renaming and Substituting Variables in Predicative Formulas, with parameters among $\mathbb{R}$, $+$, $0$ and $\le$. By Renaming and Substituting Variables in Predicative Formulas (i) with $\sigma(0)=i$ and $\sigma(1)=j$ (the given $x_{0},\dots,x_{n-1}$ being the first of the distinct set variables $x_{0},x_{1},\dots$ there, so that $x_{1}$ is distinct from $x_{0}$ also when $n=1$), 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 the condition of the corresponding clause holds with $X=x_{i}$ and $d=x_{j}$. This proves (i), (ii), (iii), (iv), (v) and (vi).

The class of metrics. For a set $X$, The Class Comprehension Theorem for Predicative Formulas (i), applied to $\psi$ with $x_{1}$ as its single variable and $x_{0}$, $\mathbb{R}$, $+$, $0$ and $\le$ as its parameters, $x_{0}$ being assigned $X$, gives a class $M$ such that, for every class $d$, $d\in M$ if and only if $d$ is a map $d:X\times X\to\mathbb{R}$ that is a metric on $X$ (every such map is a set, being an element of the class $\mathbb{R}^{X\times X}$ of functions from $X\times X$ to $\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)). This proves (vii).