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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $(X,d)$ be a metric space, let $<$ and $0$ be the strict order and the zero of $\mathbb{R}$, and let $\mathcal{P}(X)$ be the power set of $X$.

¶ The condition on the set variable $U$, with parameters $X$, $d$, $\mathbb{R}$, $<$ and $0$, that $U\subseteq X$ and $U$ is open in $(X,d)$ is expressed by a predicative formula, namely by $\omega(U)$:

$$\forall y\,(y\in U\Rightarrow y\in X)\wedge\forall x\,\Bigl(x\in U\Rightarrow\exists r\,\bigl(r\in\mathbb{R}\wedge0<r\wedge\forall y\,\bigl((y\in X\wedge\exists z\,(((x,y),z)\in d\wedge z<r))\Rightarrow y\in U\bigr)\bigr)\Bigr),$$

where $x$, $y$, $z$ and $r$ are set variables distinct from $U$ and from one another, $0<r$ and $z<r$ stand for $(0,r)\in{<}$ and $(z,r)\in{<}$, and for $x,y\in X$ and $r\in\mathbb{R}$ the part $\exists z\,(((x,y),z)\in d\wedge z<r)$ holds if and only if $d(x,y)<r$.

¶ There is exactly one set $\mathcal{T}$ such that, for every set $U$, $U\in\mathcal{T}$ if and only if $U\subseteq X$ and $U$ is open in $(X,d)$; it is $\{U\in\mathcal{P}(X):\omega(U)\}$, and it is the set denoted $\mathcal{T}_{d}$ in Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §topology.