A proper metric space is a metric space where closed balls are compact. Equivalently, it's a metric space such that bounded sets are compact.
In this answer user Saucy O'Path describes, given a countable sequence $\{(X_j,d_j)\}_{j\in\Bbb N}$ of (non-empty) proper metric spaces, a proper metric on $\coprod_{j\in\Bbb N} X_j$ such that the natural embeddings are isometries. The answer is (perhaps unnecessarily) lengthy, but long story short the geometric idea is that there is a building $B$ where the $n$-th floor is $(X_n,d_n)$ and there is one staircase connecting all the floors at distance $1$ each from the next. The disjoint union is seen as the subspace you obtain by removing the staircase. However, for each floor $X_n$ we must keep track of the point $x_n$ where the door to the staircase used to be, so that the distance is $$d((a,n),(b,m))=\begin{cases}d_n(a,b)&\text{if }n=m\\ d_n(a,x_n)+\lvert n-m\rvert+d_m(b,x_m)&\text{if }n\ne m\end{cases}$$
for some sequence $\{x_k\}_{k\in\Bbb N}$ such that $x_k\in X_k$.
Question: This construction metrizes the topological space $\coprod_{j\in\Bbb N}X_j$ with a proper metric $d$ such that the canonical embeddings $(X_k,d_k)\hookrightarrow \left(\prod_{j\in\Bbb N}X_j,d\right)$ are isometries. However, it uses countable choice. Is there a construction that achieves the same goal while avoiding countable choice?
There is no such construction in ZF (assuming ZF is consistent).
As Milo Brandt noted in the comments, the statement that it's always possible to add a (proper) metric to the disjoint union with isometries on every component is equivalent to asking that for every countable sequence of non-empty proper metric spaces $(X_i,d_i)$ one can construct a sequence of non-empty compact sets $C_i\subseteq X_i.$
Let $\mathcal P(\mathbb N)$ denote the powerset of the set of naturals. Let $a\sim b$ mean that the symmetric difference $a\triangle b$ is finite. I claim that it is consistent with ZF that the following statement "(V)" holds.
Each equivalence class $X_i$ can be given a proper metric space structure by $d(a,b)=\sum_{i\in a\triangle b} i.$ (Assuming the convention $0\not\in\mathbb N.$) A non-empty compact subset has a minimum element in lexicographic order. So a sequence of choices of non-empty compact sets $C_i\subset X_i$ would give a choice function for the sequence $X_i,$ contradicting (V).
To construct a suitable model of ZF, I don't know a standard example so you need to dive into set theory. I think it's a straightforward modification of standard techniques but needs a lot of background, and I'm just going to give a sketch. I suggest modifying the construction in Jech, Set Theory, 3rd Millenium Ed, Example 15.59. Given a transitive model $M$ of ZFC this produces a model $N\supset M$ with nice properties (every ultrafilter on $\omega$ is principal). Instead of taking symmetries to be arbitrary sets $X\subset\omega\times\omega$ in $M,$ take only the $X$ such that $\{m : (n,m)\in X\}$ is finite for each $n.$ The symmetric model $N$ will contain the Cohen reals $\dot{a_i}$ and the sequence of $\sim$-equivalence classes $[\dot{a_1}],[\dot{a_2}],\dots,$ but no choice function for this sequence.