Under choice, every regular $T_1$ second-countable space is metrizable

First $X$ is normal. Given disjoint closed $A,B$, enumerate the basis members whose closures avoid $B$ as $(U_n)$ and those whose closures avoid $A$ as $(V_n)$, padding by empty sets if necessary. By [L1] and the basis property, the first family covers $A$ and the second covers $B$. Put $U={\bigcup }_n(U_n\setminus {\bigcup }_{i\le n}{\bar{V}}_i)$ and $V={\bigcup }_n(V_n\setminus {\bigcup }_{i\le n}{\bar{U}}_i)$. Each summand is open because only finitely many closed sets are removed. The sets contain $A,B$ respectively. They are disjoint: a point in the $n$th summand of $U$ and $m$th summand of $V$ would contradict the removal of ${\bar{V}}_m$ if $m\le n$, and of ${\bar{U}}_n$ if $n\le m$. This proves normality.

For every pair $(i,j)$ with ${\bar{B}}_i\subseteq B_j$, [L2] gives a continuous $f_{ij}:X\to [0,1]$ equal to $1$ on ${\bar{B}}_i$ and $0$ on $X\setminus B_j$. Use AC to select all these functions, and list them as a sequence $(f_k{)}_{k\ge 1}$, adding zero functions when necessary. For every point $x$ and open neighbourhood $O$, choose $B_j$ with $x\in B_j\subseteq O$, shrink inside $B_j$ using [L1], and choose $B_i$ containing $x$ inside that shrinking. Then ${\bar{B}}_i\subseteq B_j$, so one listed function is $1$ at $x$ and vanishes outside $O$. This also separates distinct points because $T_1$ makes $X\setminus \{y\}$ open.

Define $d(x,y)={\sum }_{k\ge 1}{2}^{-k}\mathrm{\mid }{f}_k(x)-f_k(y)\mathrm{\mid }$. Each term is at most $2^{-k}$, so the sum converges. Symmetry and the triangle inequality follow termwise, and step 2.1 gives $d(x,y)>0$ for $x\mathrm{\ne }y$. Thus $d$ is a metric (including the empty-space case).

For fixed $x$ and $\epsilon >0$, choose $N$ with ${\sum }_{k>N}{2}^{-k}<\epsilon \mathrm{/}2$. Continuity of the first $N$ functions gives an original open neighbourhood $W$ of $x$ where their weighted differences from their values at $x$ sum to less than $\epsilon \mathrm{/}2$. Hence $W\subseteq B_d(x,\epsilon )$. Conversely, for an original open $O$ containing $x$, take the index $k$ supplied by step 2.1. If $d(x,y)<2^{-k}$, then $f_k(y)>0$, so $y\in O$. Thus every original neighbourhood contains a metric ball and every metric ball contains an original neighbourhood at its centre; the topologies coincide. Hence $X$ is metrizable.