I've been reading Nagata-Smirnov metrization theorem these days. It states that a space is metrizable if and only if it is regular(and Hausdorff) and has a $\sigma-$locally finite basis. I've searched the Internet and found out surprisingly that the if($\Leftarrow$) part requires no axiom of choice, but the only if part($\Rightarrow$) actually requires some choice.
Then I start to think of the space $\mathbb{R}^\omega$ in the uniform topology. It is known that it doesn't have second countable basis nor separable. I tried hard to find a constructive(or explicit) $\sigma-$locally finite basis for the space, as the metrization theorem ensures its existence, but I failed.
So I wonder whether the construction in the theorem using the well-ordering principle can be substituted. Thanks!!
Definition
$\sigma-$locally finite basis is a basis that is a countable union of locally finite collections.
A collection of subsets of a space is locally finite if every point of the space has a neighbourhood that intersects only finitely many elements of the collection.
The space of $\mathbb{R}^\omega$ in the uniform topology is the space $\mathbb{R}^\mathbb{N}$ equipped with the metric $\rho(\textbf{x},\textbf y)=\sup\{\min\{|x_i-y_i|,1\}|i\in \mathbb{N}\}$,$\textbf{x}=(x_i)_{i\in \mathbb{N}}$,$\textbf{y}=(y_i)_{i\in \mathbb{N}}$.