Implicit $AC$ in Munkres' Proof? (Completely Regular Spaces)

I'm not sure why you think that $F$ was defined by implicitly using the axiom of choice. We are given $J$, and the family of functions satisfy a certain condition. The definition is quite literal, it is the evaluation function.

Also, nowhere we claim that $J$ is somehow well-ordered, or that it can be. Or that it is linearly ordered, or that it can be. It's just an index set.

The point is that all the technical difficulties were relegated into the assumptions.

Finally, seeing how Urysohn’s Metrization Theorem has a choice-free proof, there's no use of choice here at all.

Good, C.; Tree, I. J., Continuing horrors of topology without choice, Topology Appl. 63, No. 1, 79-90 (1995). ZBL0822.54001.

Others have touched on the same points that I want to make, but let me say explicitly where you went wrong.

You wrote:

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}$$

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:

If $Y$ is a set and $\{Z_{\beta}\}_{\beta\in J}$ is an indexed family of sets

s.t. for each $\require{enclose} \enclose{horizontalstrike}{\beta\in J, \exists}$ some $\enclose{horizontalstrike}{g_{\beta}: Y\rightarrow Z_{\beta}}$

and $\{g_\beta : Y \to Z_\beta\}_{\beta \in J}$ is an indexed family of functions,

then there exists a function: $$G:Y\rightarrow \prod_{\beta\in J} Z_{\beta}$$ defined by $$G=\left(g_{\beta}\right)_{\beta\in J}$$