This exercise is from my textbook:
Let $A =\{x_1, x_2, x_3, \dots\}$ be a countable set. For each $n\in\mathbb{N}$, let $f_n$ be a real valuated funcion on $A$ and assume that there exists an $M>0$ such that $|f_n(x)|\leq M$ for all $n\in\mathbb{N}$ and all $x\in A$. Show that $(f_n)_{n=1}^{\infty}$ has a subsequence that converges pointwise on $A$.
The idea of the proof is the following: by the Bolzano-Weierstrass theorem, the sequence of real numbers $(f_n(x_1))_{n=1}^{\infty}$ has a convergent subsequence $\big(f_{n_k}(x_1)\big)_{k=1}^{\infty}$ which we denote as $\big(f_{1, k}(x_1)\big)_{k=1}^{\infty}$, we make the same observation with the sequence $\big(f_{1, k}(x_2)\big)_{k=1}^{\infty}$, then this last sequence has a convergent subsequence $\big(f_{2, k}(x_2)\big)_{k=1}^{\infty}$, if we repeat this procedure infinitely many times we get a family of convergent sequences $\big(f_{m, k}(x_m)\big)_{k=1}^{\infty}$ with the property that $(f_{m+1,k})_{k=1}^{\infty}$ is a subsequence of $(f_{m, k})_{k=1}^{\infty}$. Finally we take the sequence $(f_{n,n})_{n=1}^{\infty}$ and only remains to show that this is a subsequence of $(f_n)_{n=1}^{\infty}$ and it converges pointwise on $A$.
I understand this, but I tried to avoid the argument of "repeat this procedure infinitely many times", in order to do this I made use of the following proposition
For all $n\in\mathbb{N}$ let $A_n$ be a non-empty set and let $\sim$ be a binary relation on $\bigcup_{n=1}^{\infty} A_n$ with the property that for all $x\in A_n$ there exists $y\in A_{n+1}$ such that $x\sim y$, then the exists a sequence $(x_k)_{k=1}^{\infty}$ in $\bigcup_{n=1}^{\infty} A_n$ such that for all $k\in\mathbb{N}$ we have that $x_k\in A_k$ and $x_{k}\sim x_{k+1}$.
Which is equivalent to the Axiom of Dependent Choice and I continued in this way: Let $\Omega$ be the set of all strictly increasing functions from $\mathbb{N}$ to $\mathbb{N}$, for all $i\in\mathbb{N}$ I defined
$$A_{i}:= \left\{g\in \Omega \ : \ \big(f_{g(k)}(x_i)\big)_{k=1}^{\infty} \quad \text{converges}\right\}$$
and for all $F, G\in \bigcup_{i=1}^{\infty} A_i$ I defined the relation
$$G \sim F \quad \Leftrightarrow \quad \text{There exists} \ h\in\Omega \ \text{such that} \ G\circ h=F$$
By the Bolzano-Weierstrass theorem we have that $A_i$ is not empty and for all $G\in A_i$ there exists $F\in A_{i+1}$ such that $G\sim F$, then there exists a sequence $(\varphi_{m})_{m=1}^{\infty}$ in $\bigcup_{i=1}^{\infty} A_i$ such that for all $m\in\mathbb{N}$ we have that $\varphi_m\in A_m$ and $\varphi_m \sim \varphi_{m+1}$, so the sequence $(f_{\varphi_n(n)})_{n=1}^{\infty}$ is the same sequence $(f_{n,n})_{n=1}^{\infty}$ that we constructed in our first argument.
My question is, in this case is rigorous enought if we just say "perform this procedure infinitely many times" to construct the family of sequences $(f_{m,k}(x_m))_{k=1}^{\infty}$? Some time ago, I made a similar question in which I had to construct a sequence in a similar way and I asked how to avoid the same argument of "perform this procedure infinitely many times", in that case the problem was solved with the Axiom of Dependent Choice too, the use of the Axiom of Choice in this new case to solve a similar problem makes me think that when we say "perform this procedure infinitely many times" we are jumping some arguments and it is not rigorous enough since we can use more rigorous arguments to do the same.