Proof of The Open Sets of a Metric Space Form a Set, Given by a Predicative Formula

Each result cited is universally quantified over the data in its own statement.

Clause predicative. The formula $\omega(U)$ is written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols: the connectives $\Rightarrow$ and the quantifier $\forall$ of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, the ordered pairs $(x,y)$, $((x,y),z)$, $(0,r)$ and $(z,r)$, which are defined set symbols used properly for all sets, and membership of these pairs in the sets $d$ and $<$. Its quantifiers $\forall y$, $\forall x$, $\exists r$ and $\exists z$ are applied to set variables only, and no class abstraction is written in it; so $\omega(U)$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. Its free variables are $U$ and the parameters $X$, $d$, $\mathbb{R}$, $<$ and $0$.

Let $U$ be a set. By Subclasses and Subsets §subclass, the first conjunct of $\omega(U)$ holds if and only if $U\subseteq X$. If $U\not\subseteq X$, then $\omega(U)$ fails, and so does the condition. Let now $U\subseteq X$, let $x\in U$, so that $x\in X$, and let $y\in X$. The map $d:X\times X\to\mathbb{R}$ has domain $X\times X$, which contains $(x,y)$, so by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, for every set $z$, $((x,y),z)\in d$ if and only if $z=d(x,y)$; hence $\exists z\,(((x,y),z)\in d\wedge z<r)$ holds if and only if $d(x,y)<r$, which is the last assertion of the clause. Therefore, for $r\in\mathbb{R}$ with $0<r$, the part $\forall y\,((y\in X\wedge\exists z\,(\dots))\Rightarrow y\in U)$ holds if and only if every $y\in X$ with $d(x,y)<r$ lies in $U$, that is, by Open Ball in a Metric Space §membership and Subclasses and Subsets §subclass, if and only if the open ball $B_{d}(x,r)$ is a subset of $U$. As $r>0$ means $0<r$ by Sets and Maps: Ordinary Notation §orders, the second conjunct of $\omega(U)$ holds if and only if 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 §open, if and only if $U$ is open in $(X,d)$. So, for every set $U$, $\omega(U)$ holds if and only if $U\subseteq X$ and $U$ is open in $(X,d)$, and $\omega$ expresses this condition in the sense of Conditions Expressed by a Predicative Formula, and Guards §expressed.

Clause set. $\mathcal{P}(X)$ is a set by The Union Set and the Power Set of a Set §power. As $\omega$ is predicative, $\mathcal{T}=\{U\in\mathcal{P}(X):\omega(U)\}$ is a class as in Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and a set by Sets and Maps: Ordinary Notation §set-builder. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, for every set $U$, $U\in\mathcal{T}$ if and only if $U\in\mathcal{P}(X)$ and $\omega(U)$; by The Union Set and the Power Set of a Set §power, $U\in\mathcal{P}(X)$ if and only if $U\subseteq X$; and by the clause predicative, $\omega(U)$ holds if and only if $U\subseteq X$ and $U$ is open in $(X,d)$. So $U\in\mathcal{T}$ if and only if $U\subseteq X$ and $U$ is open in $(X,d)$. If $\mathcal{T}'$ is a set with the same property, then $\mathcal{T}'$ and $\mathcal{T}$ have the same elements, and $\mathcal{T}'=\mathcal{T}$ by Axiom of Extensionality for Classes. The class $\mathcal{T}_{d}$ of all $U\in\mathcal{P}(X)$ open in $(X,d)$ named in Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §topology has exactly these elements, so it is $\mathcal{T}$, again by Axiom of Extensionality for Classes.