Discrete sequence spaces are complete in ZF

By the function-set construction $Y$ is a set. Fix one $a_{\ast }\in A$; the constant function $n\mapsto a_{\ast }$ belongs to $Y$. If $f\mathrm{\ne }g$, their nonempty set of differing coordinates has a least member, so $d$ is a well-defined real-valued function (its graph is obtained by Replacement). Its values are nonnegative, it is symmetric, and it is zero exactly on the diagonal. No selection from a family of different carriers is involved.

For every $t\in \omega$, $d(f,g)<1\mathrm{/}(t+1)$ holds exactly when $f$ and $g$ agree at all coordinates $i\le t$: a first disagreement at $k\le t$ gives distance at least $1\mathrm{/}(t+1)$; a first disagreement at $k>t$ gives a smaller reciprocal, and equality of functions gives zero. Also, agreement at all $i<l$ implies $d(f,g)\le 1\mathrm{/}(l+1)$, including $l=0$.

To prove the strong triangle inequality, equalities $f=g$ or $g=h$ reduce it to equality. Otherwise let $i$ and $j$ be the first disagreements of $(f,g)$ and $(g,h)$ and set $t=\min (i,j)$. All three functions agree below $t$, so either $f=h$ or their first disagreement is at least $t$. Thus $d(f,h)\le 1\mathrm{/}(t+1)=\max (d(f,g),d(g,h))$. Nonnegative numbers have maximum at most their sum, so the ordinary triangle inequality follows as well. Hence $d$ is an ultrametric.

For $s:l\to A$, define $\widehat{s}(i)=s(i)$ for $i<l$ and $\widehat{s}(i)=a_{\ast }$ otherwise. Then $\widehat{s}\in [s]$, including the empty prefix $l=0$, whose cylinder is $Y$. If $l\ge 1$ and $f\in [s]$, the equivalence above gives $B(f,1\mathrm{/}l)=[s]$, so $[s]$ is open. If $g\mathrm{\notin }[s]$, there is $i<l$ with $g(i)\mathrm{\ne }s(i)$, and $B(g,1\mathrm{/}(i+1))$ fixes that coordinate and misses $[s]$. The complement is therefore open. For $l=0$ the complement is empty and open. Thus every cylinder is nonempty and clopen.

Let $(f_j{)}_{j\in \omega }$ be any Cauchy sequence in $Y$. For each $n$, its Cauchy property at the rational tolerance $1\mathrm{/}(n+1)$ makes the set of $K$ satisfying $(\mathrm{\forall }p,q\ge K)d(f_p,f_q)<1\mathrm{/}(n+1)$ nonempty. Let $K_n$ be its least member. Define $f(n)=f_{K_n}(n)$. Leastness makes both $K_n$ and this value unique, so Replacement gives the graph of a function $f:\omega \to A$, without any choice principle. By the prefix equivalence, for $j\ge K_n$ one has $f_j(n)=f_{K_n}(n)=f(n)$.

Given $f\in O$ with $O$ open, take $\epsilon >0$ with $B(f,\epsilon )\subseteq O$ and take $l\ge 1$ with $1\mathrm{/}l<\epsilon$. If $g$ extends $f\upharpoonright l$, its distance to $f$ is at most $1\mathrm{/}(l+1)<\epsilon$. Thus $f\in [f\upharpoonright l]\subseteq O$, proving the basis assertion.

For a finite prefix length $l$, put $H_0=0$ and successively $H_{t+1}=\max (H_t,K_t)$ for $t<l$. This finite deterministic construction uses no selections; induction shows $H_l\ge K_t$ for every $t<l$. Hence every $j\ge H_l$ has $f_j\upharpoonright l=f\upharpoonright l$, and $d(f_j,f)\le 1\mathrm{/}(l+1)$. Given positive rational $\epsilon$, take $l\ge 1$ with $1\mathrm{/}l<\epsilon$; this bound proves $f_j\to f$. The construction works also when $A$ is a singleton, in which case every distance is zero. Thus every Cauchy sequence converges in $Y$, completing the proof.