Under the Axiom of Countable Choice, Baire sequence space is Polish, and its standard ultrametric is complete

Given: The objects, hypotheses, and choice principles stated above.

The Baire sequence space is $\mathcal{N}:={\mathbb{N}}^{\mathbb{N}}$, the set of functions from $\mathbb{N}$ to itself (def-the-set-of-functions-from-one-set-to-another), with the product topology obtained by giving each copy of $\mathbb{N}$ the discrete topology (def-product-topology, def-standard-topologies). For a finite sequence $s=(s_0,\dots ,s_{k-1})$, its cylinder is $N_s:=\{x\in \mathcal{N}:x_i=s_i\text{ for }i<k\}$. The empty sequence has cylinder $\mathcal{N}$, and these cylinders form a basis. (Baire sequence space ${\mathbb{N}}^{\mathbb{N}}$ and its cylinder topology).

A topological space is Polish when it is separable (def-separable-space) and completely metrizable: its topology is induced by some complete metric (lem-complete-remetrisation). No particular compatible complete metric or countable dense subset is part of the structure. (Polish spaces are separable completely metrizable spaces).

Let $(X,d)$ be a metric space (def-metric-space). $(X,d)$ is complete if every Cauchy sequence in $(X,d)$ converges to a point of $X$; a subset $A\subseteq X$ is called complete when the metric subspace $(A,d_A)$ is complete. (Complete metric space: every Cauchy sequence converges in the space).

Assume the Axiom of Countable Choice. Let $(A_n{)}_{n\in \mathbb{N}}$ be a family of at most countable sets indexed by $\mathbb{N}$. Then $U={\bigcup }_{n\in \mathbb{N}}{A}_n$ is at most countable (Countable unions of at most countable sets, assuming ${\mathrm{A}\mathrm{C}}_{\omega }$).