I was reading a proof of the following theorem: Let $(X,d)$ be a metric space, if $(X,d)$ is complete and totally bounded then is compact (in the sequencial sense).
Proof: Let $(x^{(n)})_{n=1}^{\infty}$ be a sequence in $X$, the metric space is totally boundend then we can find $y_1,\dots, y_n\in X$ such that
$$X= \bigcup_{i=1}^n B(y_i, 1)$$
notice that there must exists $1\leq k\leq n$, such that for all $N\geq 1$, there exist $n\geq N$, and $x^{(n)}\in B(y_k,1)$ and we set:
$$(1;1):= \min\{m\in\mathbb{N} : x^{(m)}\in B(y_k, 1)\}$$
$$(n; 1):= \min\{m\in\mathbb{N} : m > (n-1, 1), \ x^{(m)}\in B(y_k, 1)\} \quad\forall n\geq2$$
then $(x^{(n;1)})_{n=1}^{\infty}$ is a subsequence of $(x^{(n)})_{n=1}^{\infty}$ and $(x^{(n;1)})_{n=1}^{\infty}$ is contained in a $1$-ball; we repeat this procedure with the sequence $(x^{(n;1)})_{n=1}^{\infty}$ using $1/2$-balls to cover $X$, then we obtain a subsequence $(x^{(n;2)})_{n=1}^{\infty}$ of $(x^{(n;1)})_{n=1}^{\infty}$, such that $(x^{(n;2)})_{n=1}^{\infty}$ is contained in a single $1/2$-ball; we repeat this procedure infinte times, then for all $j\geq 1$ we get a subsequence $(x^{(n;j)})_{n=1}^{\infty}$ of $(x^{(n)})_{n=1}^{\infty}$, such that for each $j$, the elements of $(x^{(n;j)})_{n=1}^{\infty}$ are contained in a single ball of radius $1/j$, and also that each sequence $(x^{(n;j+1)})_{n=1}^{\infty}$ is a subsequence of the previous one $(x^{(n;j)})_{n=1}^{\infty}$, finally we take the sequence $(x^{(n;n)})_{n=1}^{\infty}$, this sequence is a subsequence of $(x^{(n)})_{n=1}^{\infty}$, also is a Cauchy sequence and is convergent, since, the space is complete, then every sequence in $X$ has a convergent subsequence.
My doubt is in the way we construct the sequence $(x^{(n,n)})_{n=1}^{\infty}$, How we can use more rigorous arguments to construct that sequence? I suspect that we need Axiom of choice, so my attempt was: Let $\mathcal{C}$ be set of all subsequence $(y^{(n)})_{n=1}^{\infty}$ of $(x^{(n)})_{n=1}^{\infty}$ and define $\Omega:= \mathcal{C}\times \mathbb{N}$ with the relation $\sim$ defined as follows: $\big((y^{(n)})_{n=1}^{\infty}, \ k\big) \sim \big((z^{(n)})_{n=1}^{\infty}, \ j\big)$ iff $j=k+1$ and $(z^{(n)})_{n=1}^{\infty}$ is a subsequence of $(y^{(n)})_{n=1}^{\infty}$ such that $d(z^{(m)}, z^{(n)}) < 2/j$ for all $n,m\geq 1$, with a similar prodecure to we used at the beginning of the proof we can show that for all $a\in \Omega$ there exist $b\in\Omega$ such that $a\sim b$, for each $a\in\Omega$ we define $R(a):=\{b\in\Omega : a\sim b\}$, with the axiom of choice we can find a function:
$$f : \Omega\rightarrow \bigcup_{a\in\Omega} R(a)$$
such that $f(a)\in R(a)$ for all $a\in\Omega$, so consider the sequence $\big[\big(f^k((x^{(n)})_{n=0}^{\infty},0\big)\big]_{k=1}^{\infty}$, for each $j\geq 1$ we define the sequence $(x^{(n:j)})_{n=1}^{\infty}$ as the sequence of the first entry of $f^j((x^{(n)})_{n=0}^{\infty},0\big)$
Your approach looks good to me! Note that it also shows the full axiom of choice isn't needed for this fact, only the axiom of dependent choice. Let me make a further point that you might still find illuminating: the only place choice is being used in this proof is in getting the sequence of increasingly small families of balls. More precisely, the following can be proved without any choice at all:
Theorem: Let $(X,d)$ be a complete metric space, and suppose there exist $(y_{ni})_{n,i\in\mathbb{N}}$ and $k_n\in\mathbb{N}$ such that $X=\bigcup_{i=1}^{k_n}B(y_{ni},1/n)$ for each $n\in\mathbb{N}$. Then $X$ is sequentially compact. $\blacksquare$
The proof is identical to the one you've written, but let me spell out one or two details where it might seem like you're using choice, but you're actually not. The structure of your proof is to define a sequence of subsequences of $(x^{n})_{n\in\mathbb{N}}$, where the $m$-th sequence is contained in a ball of radius $1/m$ and the $(m+1)$-th sequence is a subsequence of the $m$-th. One way of formalizing this is as follows. We want to define a function $f:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ with the following two properties: (i) for each $n\in\mathbb{N}$, the sequence $(x^{f(n+1,i)})_{i\in\mathbb{N}}$ is a subsequence of $(x^{f(n,i)})_{i\in\mathbb{N}}$, and (ii) for each $n\in\mathbb{N}$, there exists some $l_n\in\{1,\dots,k_n\}$ such that $x^{f(n,i)}\in B(y_{nl_n},1/n)$ for each $i\in\mathbb{N}$. Once we've done this, the rest of your proof proceeds in exactly the same way, without any need for choice. So after we've constructed $f$ we're done.
The fundamental reason we can construct this function $f$ is that $\mathbb{N}\times\mathbb{N}$ is a countable set (no need for choice to prove this!), and hence can be well-ordered. This means we can choiceless-ly define functions from $\mathbb{N}\times\mathbb{N}$ to other sets using recursion.
In our case, the most useful ordering to put onto $\mathbb{N}\times\mathbb{N}$ is the lexicographic order, where we take $(n,i)\prec(m,j)$ to hold if and only if either $m<n$ or $m=n$ and $i<j$; I'll leave it to you to check that this is a well-order.
Okay, let's use this to define our function $f$! Following the notation of the proofwiki link, let $\mathcal{F}$ be the set of all functions from a proper $\prec$-initial segment of $\mathbb{N}\times\mathbb{N}$ to $\mathbb{N}$. To apply recursion we need a function $\Phi$ from $\mathcal{F}$ to $\mathbb{N}$. We'll do this as following: fix an element $g\in\mathcal{F}$, ie a function $g:I\to\mathbb{N}$, where $I\subseteq\mathbb{N}\times\mathbb{N}$ is a proper $\prec$-initial segment. Since $(\mathbb{N}\times\mathbb{N},\prec)$ is a well-order and $I$ is a proper initial segment, the set $\mathbb{N}\times\mathbb{N}\setminus I$ has a $\prec$-minimal element $(n,i)$. By hypothesis, we know $X$ is the union of the finitely many sets $B(y_{n1},1/n),\dots,B(y_{nk_n},1/n)$. Now, if $n=1$ define $z^i=x^i$ for each $i\in\mathbb{N}$, and if $n>1$ define $z^i=x^{g(n-1,i)}$ for each $i\in\mathbb{N}$. By the pigeonhole principle, there exists $l\in\{1,\dots,k_n\}$ such that the sequence $(z^i)_{i\in\mathbb{N}}$ "lands" in $B(y_{nl},1/n)$ infinitely often; let $l_I\in\{1,\dots,k_n\}$ be minimal with this property. (There is no need for choice here; $l_I$ is uniquely determined by $I$.) Now, we can define $\Phi(g):I\cup\{(n,j):j\geqslant i\}\to\mathbb{N}$ by taking $\Phi(g)|_{I}=g$ and taking $$\Phi(g)(n,j)=\min\{p\in\mathbb{N}:p>\Phi(g)(n,j')\text{ for all }j'\in\{i,\dots,j-1\}\text{ and }p\in B(y_{nl_I},1/n)\}.$$ (This is again something that looks like it uses choice, but it actually doesn't, since the map $j\mapsto \Phi(g)(n,j)$ for $j\geqslant i$ is a function from the well-ordered set $\{j\in\mathbb{N}:j\geqslant i\}$ to $\mathbb{N}$ and thus can be defined recursively; I'm omitting the details here lest the post become too cluttered, and it's a good exercise to fill them out.) Since $I\cup\{(n,j):j\geqslant i\}$ is a $\prec$-initial segment of $\mathbb{N}\times\mathbb{N}$, we have thus given a well-defined element $\Phi(g)\in\mathcal{F}$.
Now, $\Phi(g)$ was uniquely determined given $g$, so we have constructed the function $\Phi:\mathcal{F}\to\mathbb{N}$ without any use of the axiom of choice. By recursion (see the proofwiki link), we hence obtain a unique function $f:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ such that $f(n,i)=\Phi(f|_{\{(m,j):(m,j)\prec(n,i)\}})$ for every $(n,i)\in\mathbb{N}$. I'll leave it to you to check that $f$ now has the desired properties; feel free to ask me if you have any questions! (As a starting point, given $n\in\mathbb{N}$, can you see what $l_n$ will be? It should be equal to $l_I$ for some suitable $\prec$-initial segment $I$ of $\mathbb{N}\times\mathbb{N}$.)
From hereonout, the proof proceed exactly as yours does, and so we are done.