Proof of Kit for def:separable-metric

Throughout, formulas are written with abbreviations and quantify over set variables only, so they are predicative. The parameters $\mathbb{N}$, $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ are variables other than $x_{0},x_{1},\dots$ and other than the bound variables below; $0$ and $1$ are sets, being elements of $\mathbb{R}$. 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)). For sets $r$ and $s$, $r<s$ abbreviates $(r,s)\in{\le}\wedge\neg\,r=s$, the strict order of $\mathbb{R}$. We first build formulas in the set variables $x_{0},x_{1},\dots,x_{4}$ and move them to the given positions at the end; the letters $D,w,w',w'',x,y,z,u,v,r,t,c,p$ denote further set variables.

Separable metric spaces. Write $X$ and $d$ for $x_{0}$ and $x_{1}$. 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 $\Gamma_{1}$; its bound variables are chosen other than the letters above. Let $\mathrm{cnt}(D)$ be the formula of Countability as a Predicative Condition, and Finite Powers of a Set as a Typed Term (i) with $D$ for its $x$, its bound variables chosen other than $X$, $d$, $D$ and the letters listed above, and its parameter $N$ having the value $\mathbb{N}$, a set by The Set of Natural Numbers and the Number One (i): for every set $D$, $\mathrm{cnt}(D)$ holds exactly when $D$ is countable. Let

$$\beta(D)=\forall x\,\forall r\,\Bigl(\bigl(x\in X\wedge r\in\mathbb{R}\wedge0<r\bigr)\Rightarrow\exists y\,\exists t\,\bigl(y\in D\wedge y\in X\wedge((x,y),t)\in d\wedge t<r\bigr)\Bigr),$$ $$\varphi_{1}=\mu_{0}\wedge\exists D\,\bigl(\forall w\,(w\in D\Rightarrow w\in X)\wedge\mathrm{cnt}(D)\wedge\beta(D)\bigr).$$

Assume $\Gamma_{1}$, and let $D\subseteq X$. For $x,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)$, a real number, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x). Hence, for $x\in X$ and a real number $r>0$, the existential part of $\beta(D)$, whose premise $((x,y),t)\in d$ names this value, says that some $y$ satisfies $y\in D$, $y\in X$ and $d(x,y)<r$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii)), that is, by Open Ball in a Metric Space (ii) and The Boolean Operations on Classes, Disjointness, and the Universal Class (i), that $D\cap B_{d}(x,r)\neq\emptyset$ (this class is a set by 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), being a subclass of $X$, and the empty set is the only set with no element). Thus $\beta(D)$ holds exactly when $D$ is dense in $(X,d)$. The subsets of $X$ are exactly the sets $D$ with $\forall w\,(w\in D\Rightarrow w\in X)$ (Subclasses and Subsets (i)). So, under $\Gamma_{1}$, the second conjunct of $\varphi_{1}$ holds exactly when $X$ has a countable subset that is dense in $(X,d)$, that is, by Separable Metric Space and Separable Real Normed Space (i), exactly when $(X,d)$ is separable. As $\mu_{0}$ expresses $\Gamma_{1}$, the formula $\varphi_{1}$, with parameters among $\mathbb{N}$, $\mathbb{R}$, $+$, $0$ and $\le$, expresses the condition of (i) with $X=x_{0}$ and $d=x_{1}$.

The norm metric. Now write $V$, $a$, $s$, $\nu$ and $d$ for $x_{0}$, $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$. By Kit for def:normed-space (vi) with $n=4$ and the positions $0,1,2,3$, there is a predicative formula $\chi$ in $x_{0},\dots,x_{3}$, with parameters among $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$, that expresses $\Gamma_{2}$; its bound variables are chosen other than the letters above. Let

$$\zeta(z)=z\in V\wedge\forall w''\,\bigl(w''\in V\Rightarrow((w'',z),w'')\in a\bigr),\qquad \delta(u,v,w)=\exists w'\,\exists z\,\bigl(w'\in V\wedge\zeta(z)\wedge((v,w'),z)\in a\wedge((u,w'),w)\in a\bigr).$$

Assume $\Gamma_{2}$. Then $a$ is a binary operation on $V$ (Vector Space over a Field (ix)), so for sets $u$, $v$ and $z$, $((u,v),z)\in a$ holds exactly when $u,v\in V$ and $z=u+v$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi)). Hence $\zeta(z)$ says that $z\in V$ and $w+z=w$ for every $w\in V$, which holds exactly for $z=0_{V}$, the zero vector. For $u,v\in V$, $\delta(u,v,w)$ then says that there is $w'\in V$ with $v+w'=0_{V}$ and $w=u+w'$; the only such $w'$ is the negative $-v$, so $\delta(u,v,w)$ holds exactly for $w=u+(-v)$, the difference $u-v$. 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)$, 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

$$\theta=\exists c\,\bigl(\pi(c,V,V)\wedge\mu(d,c,\mathbb{R})\bigr)\wedge\forall u\,\forall v\,\forall t\,\forall w\,\forall y\,\Bigl(\bigl(u\in V\wedge v\in V\wedge((u,v),t)\in d\wedge\delta(u,v,w)\wedge(w,y)\in\nu\bigr)\Rightarrow t=y\Bigr).$$

The only set $c$ with $\pi(c,V,V)$ is the Cartesian product $V\times V$, which is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii); so, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii), the first conjunct of $\theta$ holds exactly when $d$ is a map $d:V\times V\to\mathbb{R}$. When it does, for $u,v\in V$ the premises of the second conjunct name $t=d(u,v)$, $w=u-v\in V$ and $y=\lVert u-v\rVert$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x), the function $\lVert\cdot\rVert=\nu$ having domain $V$; 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)). So $\theta$ holds exactly when $d$ is a map $V\times V\to\mathbb{R}$ with

$$d(u,v)=\lVert u-v\rVert\qquad\text{for all }u,v\in V,$$

that is, by The Norm Metric of a Real Normed Space (i) and Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii), exactly when $d$ is the norm metric $d_{V}$.

Separable real normed spaces. By Renaming and Substituting Variables in Predicative Formulas (i) with $\sigma(0)=0$ and $\sigma(1)=4$, the formula $\varphi_{1}(x_{0},x_{4})$ is a predicative formula in $x_{0},\dots,x_{4}$ that holds exactly when $\varphi_{1}$ holds with $x_{0}$ assigned $V$ and $x_{1}$ assigned $d$, that is, exactly when $d$ is a map $V\times V\to\mathbb{R}$, $(V,d)$ is a metric space and $(V,d)$ is separable. Let

$$\varphi_{2}=\chi\wedge\exists x_{4}\,\bigl(\theta\wedge\varphi_{1}(x_{0},x_{4})\bigr).$$

Its free variables are among $x_{0},\dots,x_{3}$ and the parameters $\mathbb{N}$, $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$. Under an assignment of sets to $x_{0},\dots,x_{3}$, the second conjunct holds exactly when some set $d$ satisfies $\theta$ and $\varphi_{1}(x_{0},x_{4})$ (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv)). Under $\Gamma_{2}$, the only set satisfying $\theta$ is $d_{V}$ (a set, being an element of the class $\mathbb{R}^{V\times V}$ of functions from $V\times V$ to $\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)); so the second conjunct holds exactly when $d_{V}$ is a map $V\times V\to\mathbb{R}$, $(V,d_{V})$ is a metric space and $(V,d_{V})$ is separable. The first two of these hold: $d_{V}$ is a map $V\times V\to\mathbb{R}$ by The Norm Metric of a Real Normed Space (i) and a metric on $V$ by The Norm Metric of a Real Normed Space (ii), so $(V,d_{V})$ is a metric space by Metric Space (vi). Hence, under $\Gamma_{2}$, the second conjunct holds exactly when $(V,d_{V})$ is separable, that is, by Separable Metric Space and Separable Real Normed Space (ii), exactly when $V$ is separable. As $\chi$ expresses $\Gamma_{2}$, the formula $\varphi_{2}$ expresses the condition of (ii) with $V=x_{0}$, addition $x_{1}$, scalar multiplication $x_{2}$ and $\lVert\cdot\rVert=x_{3}$.

Any positions. Thus $\varphi_{1}$ is a predicative formula in $x_{0},x_{1}$ and $\varphi_{2}$ one in $x_{0},\dots,x_{3}$, in the sense of Renaming and Substituting Variables in Predicative Formulas. By Renaming and Substituting Variables in Predicative Formulas (i) with $\sigma(0)=i$ and $\sigma(1)=j$ for $\varphi_{1}$, and with $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$ and $\sigma(3)=l$ for $\varphi_{2}$ (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},\dots,x_{4}$ above are distinct from $x_{0}$ whatever $n$ is), the formulas $\varphi_{1}(x_{i},x_{j})$ and $\varphi_{2}(x_{i},x_{j},x_{k},x_{l})$ are predicative formulas in $x_{0},\dots,x_{n-1}$ that hold, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $\varphi_{1}$ and $\varphi_{2}$ hold with their variables assigned the sets assigned to $x_{i},x_{j}$ and to $x_{i},x_{j},x_{k},x_{l}$. This proves (i) and (ii).

The class of separable metrics. Let $X$ be a set. Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\varphi_{1}$, with $x_{1}$ as its single variable and $x_{0}$, $\mathbb{N}$, $\mathbb{R}$, $+$, $0$ and $\le$ as its parameters, $x_{0}$ being assigned $X$. It gives a class $S$ such that, for every set $d$, $d\in S$ if and only if $\varphi_{1}$ holds with $x_{0}$ assigned $X$ and $x_{1}$ assigned $d$, that is, by the above and Metric Space (vi), exactly when $d$ is a map $d:X\times X\to\mathbb{R}$ that is a metric on $X$ with $(X,d)$ separable. As the elements of $S$ and these maps are all sets (such a map lies in the class $\mathbb{R}^{X\times X}$, as $d_{V}$ did above), the same holds for every class $d$, which proves (iii).