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?