Recently, I have been reading Munkres' Topology. In Chapter $4$, he presents a couple of proofs of the Urysohn Metrization Theorem and then, at the end of the section, generalizes one of them to an 'Imbedding Theorem' for completely regular spaces (Munkres' definition of completely regular includes the $T_0$ axiom):
Theorem 34.2 (Imbedding theorem). Let $X$ be a space in which one-point sets are closed. Suppose that $\{f_{\alpha}\}_{\alpha\in J}$ is an indexed family of continuous functions $f_a: X\rightarrow \mathbb R$ satisfying the requirement that for each point $x_0$ of $X$ and each neighborhood $U$ of $x_0$, there is an index $\alpha$ such that $f_{\alpha}$ is positive at $x_0$ and vanishes outside $U$. Then the function $F:X\rightarrow \mathbb R^J$ defined by $$F(x)=\left(f_{\alpha}(x)\right)_{\alpha\in J}$$ is an imbedding of $X$ in $\mathbb R^J$. If $f_{\alpha}$ maps $X$ into $[0,1]$ for each $\alpha$, then $F$ imbeds $X$ in $[0,1]^J$.
My question is this: does the proof of this theorem (the way Munkres outlines it above) implicitly rely on the Axiom of Choice or some weaker version? If the answer is "a weaker version" what is that version? Is the theorem itself equivalent to some well-known weaker version of $AC$?
Elaboration:
The essential parts of the proof - that $F$ is injective, continuous, and an open map, follow easily by simply plugging in $J$ in place of the index set in the first proof of the Urysohn Metrization Theorem Munkres presents.
The thing that has been bothering upon a recent rereading of this proof is the construction of the '$F$' used in the statement of the imbedding theorem itself.
It seems like, implicitly, in constructing the function, '$F$', we have used the truth of a statement that would look something like:
If $Y$ is a set and $\{Z_{\beta}\}_{\beta\in J}$ is an indexed family of sets s.t. for each $\beta\in J$, $\exists$ some $g_{\beta}: Y\rightarrow Z_{\beta}$, then there exists a function: $$G:Y\rightarrow \prod_{\beta\in J} Z_{\beta}$$ defined by $$G=\left(g_{\beta}\right)_{\beta\in J}$$
But this statement looks like, at least to me, a version of the Axiom of Choice.
For, with the truth of the Axiom of Choice, given such $Y$, $\{Z_{\beta}\}_{\beta\in J}$, and $\{g_{\beta}\}_{\beta\in J}$, we may well-order the index set, $J$, and then recursively define $\pi_{\beta}(G)=g_{\beta}$ (where $\pi_{\beta}$ denotes the $\beta$th projection map).
On the other, if the above statement were true, given any indexed family of nonempty sets, $\{X_{\alpha}\}_{\alpha\in J}$, we have that, for each $\alpha$, $\exists$ $f_{\alpha}: \{0\}\rightarrow X_{\alpha}$ (since each $X_{\alpha}$ is nonempty - I think this collection of functions should be well-defined). So, by the truth of the statement, there exists a map, $F:\{0\}\rightarrow \prod_{\alpha\in J} X_{\alpha}$. But then $\prod_{\alpha\in J} X_{\alpha}$ must contain $F(0)$, making $\prod_{\alpha\in J} X_{\alpha}$ nonempty.
So the statement seems to imply the Axiom of Choice too, making it look like they are equivalent. I have to say, however, that I am not sure that the above implications are true. My set theory is rusty and I haven't found and cannot recall ever seeing the Axiom of Choice stated in this way, so I think there may be some flaw with my reasoning.
So, my question is- well, first, if there is a flaw in my reasoning drawing an equivalence between the statement and $AC$, please leave an answer explaining this- but beyond that, is the statement equivalent to maybe something weaker? If not, is there a way around the full $AC$ in the proof of the Imbedding theorem? I ask mostly because I am only really familiar with $AC$ appearing in topology as versions of the Tychonoff theorem, the connection with which, seems more intuitive.
Others have touched on the same points that I want to make, but let me say explicitly where you went wrong.
You wrote:
This is not the statement you want to apply, because it omits important information that is given in the statement of Theorem 34.2: what you are given is not the mere existence of the function $g_\beta$ for each $\beta$, but you are actually given an indexed family of functions.
What you should have written is this statement, which contains no choice: