Let $(\Omega_n,\mathcal T_n)_{n\geq1}$ be a a sequence of topological spaces with countable base. For $n\geq1$, let $\{V^k_n:k\in I_n\}$ be a countable base of $(\Omega_n,\mathcal T_n)_{n\geq1}$, where $I_n$ is finite or countably infinite. Let $\Omega:=\prod_{n=1}^\infty\Omega_n$ and let $\mathcal T$ be the product topology on $\Omega$. For all $p\geq 1$ let
$$\mathcal{H}^p:=\bigg\{V_1^{k_1}\times\dots\times V_p^{k_p}\times\prod_{n=p+1}^\infty\Omega_n : (k_1,\dots, k_p)\in I_1\times\dots\times I_p\bigg\}$$
and let $\mathcal{H}:=\cup_{p\geq1}\mathcal{H}^p$. The goal is to show that $\mathcal{H}$ is a countable base for $(\Omega,\mathcal T)$. Suppose we have already shown that $\mathcal{H}$ is countable. Consider the following argument:
Let $U\in \mathcal T$ and let $x\in U$. By definition of the product topology there exist $p\geq 1$ and open sets $U_1,\dots, U_p$ in $\Omega_1,\dots,\Omega_p$ respectively such that
$$ x\in U_1\times\dots\times U_p\times\prod_{n=p+1}^\infty\Omega_n \subset U$$
Now, for each $1\leq n\leq p$, there exist $I'_n\subset I_n$ such that $U_n=\cup_{k\in I'_n}V^k_n$. In particular there exist $k_n\in I'_n\subset I_n$ such that $x_n \in V^k_n$. We have found $k_1,\dots,k_p$ such that
$$x \in V_x:= V_1^{k_1}\times\dots\times V_p^{k_p} \times\prod_{n=p+1}^\infty\Omega_n$$
Since $V_x \in \mathcal{H}^p\subset \mathcal{H}$, $U=\cup_{x\in U} V_x$ and $U$ is arbitrary, we conclude that $\mathcal{H}$ is a countable base for $(\Omega,\mathcal T)$.
Question: Is the axiom of choice used here? I feel it is used twice: first at the beginning to pick a countable base for each topology and then also to pick $V_x$ for each $x$. Is this correct? Is there a way to avoid using the axiom of choice?