Proof of Kit for def:open-subset-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}$ are distinct also when $n<3$. 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 $p$ and $q$, $p<q$ abbreviates $(p,q)\in{\le}\wedge\neg\,p=q$, the strict order of $\mathbb{R}$. The letters $w,x,y,r,t$ 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 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 formula. Write $X$, $d$ and $U$ for $x_{0}$, $x_{1}$ and $x_{2}$. 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}$. By Kit for def:metric-space (vi) with $n=2$, $i=0$ and $j=1$, there is a predicative formula $\mu_{0}$ in $x_{0},x_{1}$, with parameters among $\mathbb{R}$, $+$, $0$ and $\le$, that expresses "$d$ is a map $X\times X\to\mathbb{R}$ and $(X,d)$ is a metric space"; its bound variables are chosen other than the letters above. Let

$$\omega=\forall w\,(w\in U\Rightarrow w\in X)\wedge\forall x\,\Bigl(x\in U\Rightarrow\exists r\,\bigl(r\in\mathbb{R}\wedge0<r\wedge\forall y\,\forall t\,\bigl((y\in X\wedge((x,y),t)\in d\wedge t<r)\Rightarrow y\in U\bigr)\bigr)\Bigr),$$ $$\varphi=\mu_{0}\wedge\omega,$$

where $\mu_{0}$ is also a predicative formula in $x_{0},x_{1},x_{2}$ (Renaming and Substituting Variables in Predicative Formulas (ii)). It is predicative, no quantifier in it being applied to a class variable (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)), and its free variables are among $x_{0},x_{1},x_{2}$ and the parameters. Let sets $X$, $d$ and $U$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If $d$ is not a map $X\times X\to\mathbb{R}$ or $(X,d)$ is not a metric space, then $\mu_{0}$ fails, and so do $\varphi$ and the condition

$$(X,d)\text{ is a metric space},\quad U\subseteq X,\quad U\text{ is open in }(X,d).$$

Suppose now that $d:X\times X\to\mathbb{R}$ and that $(X,d)$ is a metric space, so that $\mu_{0}$ holds. The first conjunct of $\omega$ holds exactly when $U\subseteq X$ (Subclasses and Subsets (i)); if it fails, $\varphi$ and the displayed condition both fail. So suppose $U\subseteq X$, let $x\in U$, so that $x\in X$, and let $r$ be a real number with $0<r$. For $y\in X$ the pair $(x,y)$ 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, $d$ being a function, $((x,y),t)\in d$ holds exactly for $t=d(x,y)$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)); hence, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), $\forall t\,\bigl((y\in X\wedge((x,y),t)\in d\wedge t<r)\Rightarrow y\in U\bigr)$ holds exactly when $d(x,y)<r$ implies $y\in U$, while for $y\notin X$ it holds trivially. So the part of $\omega$ beginning with $\forall y$ says that every $y$ with $y\in X$ and $d(x,y)<r$ lies in $U$, that is, by Open Ball in a Metric Space (ii) and Subclasses and Subsets (i), that the open ball satisfies

$$B_{d}(x,r)\subseteq U.$$

Hence the second conjunct of $\omega$ says that for every $x\in U$ there is a real number $r>0$ with $B_{d}(x,r)\subseteq U$, that is, by Open Subset of a Metric Space (i), that $U$ is open in $(X,d)$. In all cases $\varphi$ holds if and only if the displayed condition does. So $\varphi$ is a predicative formula in $x_{0},x_{1},x_{2}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing the displayed condition with $X$, $d$ and $U$ the sets assigned to $x_{0}$, $x_{1}$ and $x_{2}$.

Open subsets. 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 $\varphi(x_{i},x_{j},x_{k})$ 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}\subseteq x_{i}$ and $x_{k}$ is open in $(x_{i},x_{j})$. This proves (i).

The class of open subsets. Let $(X,d)$ be a metric space. Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\varphi$ with its abbreviations eliminated, with $x_{2}$ as its single variable and $x_{0}$, $x_{1}$, $\mathbb{R}$, $+$, $0$ and $\le$ as its parameters, $x_{0}$ and $x_{1}$ being assigned $X$ and $d$. It gives a class $C$ whose elements are exactly the sets $U$ for which $\varphi$ holds with $x_{0}$, $x_{1}$ and $x_{2}$ assigned $X$, $d$ and $U$, that is, as $(X,d)$ is a metric space, the sets $U\subseteq X$ that are open in $(X,d)$. This proves (ii).