DMC implies Urysohn's lemma

Assume DMC, let $X$ be normal and let $F,G$ be disjoint closed subsets of $X$.

Under step 1.1, $X\setminus G$ is open and $F\subseteq X\setminus G$; by [F1] fix open $V_0$ with $F\subseteq V_0\subseteq \overline{V_0}\subseteq X\setminus G$, and put $V_1:=X\setminus G$.

Under step 1.1, define a node of level $n$ to be a tuple $⟨U_1,\dots ,U_{2^n}⟩$ of open subsets of $X$ such that $\overline{U_i}\subseteq U_{i+1}$ for $1\le i<2^n$, $F\subseteq U_1$, and $U_{2^n}=X\setminus G$. Let $T$ be the set of such nodes over all $n\in \mathbb{N}$, and let the relation $S$ on $T$ be: $aSb$ when $b$ is a node of level $n+1$ whose even entries are the entries of $a$, that is $b_{2i}=a_i$ for $1\le i\le 2^n$.

Under step 3.1, $⟨V_1⟩=⟨X\setminus G⟩$ is a node of level $0$ in $T$: it has the single required entry, $F\subseteq X\setminus G$ and its last entry is $X\setminus G$, so $T\mathrm{\ne }\mathrm{\varnothing }$. And $S$ is serial on $T$: given a node $a=⟨U_1,\dots ,U_{2^n}⟩$, apply [F1] to the closed set $F$ inside the open set $U_1$ to obtain an open $W_0$ with $F\subseteq W_0\subseteq \overline{W_0}\subseteq U_1$, for each $1\le i<2^n$ apply [F1] to the closed set $\overline{U_i}$ inside the open set $U_{i+1}$ to obtain an open $W_i$ with $\overline{U_i}\subseteq W_i\subseteq \overline{W_i}\subseteq U_{i+1}$, and use [F4] to choose all of $W_0,\dots ,W_{2^n-1}$ at once (when $n=0$ one may take $W_0$ to be the $V_0$ of step 2.1, which has exactly the required inclusions); then $b:=⟨W_0,U_1,W_1,U_2,\dots ,W_{2^n-1},U_{2^n}⟩$ has $2^{n+1}$ entries, its even entries are $b_{2i}=U_i$ for $1\le i\le 2^n$, and $F\subseteq b_1$, $\overline{b_j}\subseteq b_{j+1}$ for $1\le j<2^{n+1}$, $b_{2^{n+1}}=X\setminus G$ by step 3.1, so $b$ is a node of level $n+1$ with $aSb$.

Under step 4.1, apply [F5] to obtain finite nonempty menus $F_n\subseteq T$. They need not be level-aligned. Let $k$ be the least level represented in $F_0$ by [L2] and let $H_0$ consist of its level-$k$ members. Define $H_{n+1}=\{b\in F_{n+1}:(\mathrm{\exists }a\in H_n)aSb\}$. This is a definable recursion (encode the index and subset in a set state, with a default for other states), licensed by [L2]. Induction shows that $H_n$ is nonempty finite, every member has level $k+n$, and the $H_n$ have both successor and predecessor properties: each retained $a$ has a successor in the original next menu and that successor is retained. To recover levels below $k$, for a level-$k$ node $a$ and $0\le m\le k$ put ${\pi }_m(a{)}_i=a_{i{2}^{k-m}}$ for $1\le i\le 2^m$. Each projection is a level-$m$ node: all entries contain $F$, the last is $X\setminus G$, and the closure inclusions follow by skipping along the original chain. Moreover ${\pi }_{m+1}(a{)}_{2i}={\pi }_m(a{)}_i$ and ${\pi }_k(a)=a$. Now put $F_m^{\mathrm{\prime }}=\{{\pi }_m(a):a\in H_0\}$ for $m<k$, and $F_m^{\mathrm{\prime }}=H_{m-k}$ for $m\ge k$. These are nonempty finite menus of exactly level $m$, with both predecessor and successor properties, including the transition into level $k$. In particular $F_0^{\mathrm{\prime }}=\{⟨X\setminus G⟩\}$. No enumeration of infinitely many finite menus or branch choice is made.

Under step 5.1, for $n\in \mathbb{N}$ and $1\le i\le 2^n$ put $U_{n,i}:=\bigcap \{a_i:a\in F_n^{\mathrm{\prime }}\}$, the intersection of the $i$-th entries of the finitely many menu elements; each $U_{n,i}$ is open, $F\subseteq U_{n,1}$, $U_{n,2^n}=X\setminus G$, and $\overline{U_{n,i}}\subseteq U_{n,i+1}$, because the intersection is contained in every entry, its closure is contained in every entry closure by monotonicity, and each such closure is contained in the corresponding next entry. Monotonicity follows directly from the smallest-closed-superset characterization in [L1].

Under step 6.1, $U_{n+1,2i}=U_{n,i}$ for all $n$ and $1\le i\le 2^n$: every $b\in F_{n+1}^{\mathrm{\prime }}$ has $b_{2i}=a_i$ for the predecessor $a\in F_n^{\mathrm{\prime }}$ with $aSb$, and every $a\in F_n^{\mathrm{\prime }}$ occurs as the predecessor of some $b\in F_{n+1}^{\mathrm{\prime }}$ by the successor property, so the two intersections have the same entries.

Under step 7.1 define a family on all dyadics by $U_0:=\mathrm{\varnothing }$, $U_1:=X$, and, for $0<r<1$, $U_r:=U_{n,i}$ whenever $r=i\mathrm{/}{2}^n$ with $1\le i<2^n$. This is well defined by step 7.1 and [F2]. If $0<r<s<1$, choose $N$ with $r=i\mathrm{/}{2}^N$, $s=j\mathrm{/}{2}^N$ and $i<j$ by [F2]; then $U_r=U_{N,i}$, $U_s=U_{N,j}$, and $\overline{U_r}\subseteq U_s$ by step 6.1. The same inclusion is automatic when $r=0$ or $s=1$. Thus $(U_r{)}_{r\in D}$ satisfies the hypotheses of [F3] literally.

Under step 8.1, [F3] applies to the scale and gives the continuous $f(x)=\inf (\{r\in D:x\in U_r\}\cup \{1\}):X\to [0,1]$.

Under step 9.1, $F\subseteq f^{-1}(\{0\})$: if $a\in F$ and $0<r=i\mathrm{/}{2}^n<1$, then $a\in F\subseteq U_{n,1}\subseteq U_{n,i}=U_r$, and also $a\in U_1=X$. Hence $\{r\in D:a\in U_r\}=D\setminus \{0\}$, whose infimum is $0$, so $f(a)=0$.

Under step 9.1, $G\subseteq f^{-1}(\{1\})$: for $b\in G$, first $b\mathrm{\notin }{U}_0=\mathrm{\varnothing }$. For $r=i\mathrm{/}{2}^n\in D$ with $0<r<1$ we have $i\ge 1$, $i<2^n$ and $U_{n,i}\subseteq U_{n,2^n}=X\setminus G$, so $b\mathrm{\notin }{U}_r$; also $b\in X=U_1$; hence $\{r\in D:b\in U_r\}\cup \{1\}=\{1\}$ and $f(b)=1$.

Under steps 9.1, 10.1 and 10.2 the map $f$ is continuous with $F\subseteq f^{-1}(\{0\})$ and $G\subseteq f^{-1}(\{1\})$, which is Urysohn's lemma for the arbitrary normal space $X$ and disjoint closed sets $F,G$; the only choice principle used was DMC.