Does ZF prove that topological groups are completely regular? Let $\mathbf{G} = \langle G,\cdot,\mathcal{T}\;\rangle$ be a topological group. Let $\mathbf{e}$ be the identity element of $\langle G,\cdot \rangle$.
Assume $\{\mathbf{e}\}$ is closed in $\langle G,\cal{T}\;\rangle$. Then, I have managed to convince myself that:


*

*ZF proves that $\langle G,\cal{T}\;\rangle$ is regular Haudorff.

*ZF + (Dependent Choice) proves that $\langle G,\cal{T}\;\rangle$ is completely regular.


My questions are:


*

*Are those right?

*Does ZF prove that $\langle G,\cal{T}\;\rangle$ is completely regular?

*If no to question 2, does assuming one or more of following suffice for ZF to conclude that $\langle G,\cal{T}\,\rangle$ is completely regular?

*

*$\mathbf{G}$ is two-sided complete

*$\langle G,\cdot \rangle$ is abelian

*Countable Choice


 A: I'm not sure about the proof I gave, But as I checked, it didn't use full AC, but as Asaf mentioned in a comment it uses DC. The following theorem is due to Pontrjagin. See Book by Montgomery and Zippin(Page 29).
I will give a sketch of proof.
Note: Maybe it's needed to add some separation axiom to the following theorem. please edit it, if needed.
Theorem: Every $T_{0}$ topological group is completely regular.
Proof.
It's enough to prove that a given topological group $(G,*)$ is completely regular at $e$. Let $F$ be a closed set not containing $e$. Put $O=F^{c}$. Choose symmetric open neighborhoods  of $e$, $U_{n}$ By continuity of $*$, such that $U_{0}=O$(w.l.o.g assume $O$ is symmetric) $U_{n+1}^2 \subseteq U_{n} \cap O ~~~~n=0,1,2...$.
Now for rational numbers of the form $r=\frac{k}{2^n}~~k \in \{1,2,3,...2^n \},~~ n \in \{0,1,2,...\}$ inductively define open neighborhood $V_{r}$ of $e$ such that:
1) $V_{\frac{1}{2^n}}=U_{n}~~~~~\forall n$
2) $V_{\frac{2k}{2^{n+1}}}=V_{\frac{k}{2^n}}$
3) $V_{\frac{2k+1}{2^{n+1}}}=V_{\frac{1}{2^{n+1}}}V_{\frac{k}{2^n}}$
The definition does not depend to the representation of $r$ and the family $V_{r}$ has the following properties:
4) $V_{\frac{1}{2^n}}V_{\frac{m}{2^{n}}} \subseteq V_{\frac{m+1}{2^n}}~~~~~~~~~m+1 \leq 2^n$
5) $V_{r} \subseteq V_{s}~~~~~$if $~r <s<1$
Now define the function $f:G \longrightarrow [0, 1]$ as follows:
$f(x)=0~$ if $x \in \bigcap \limits_{r} V_{r}$
$f(x)=1$ if $~~x \notin V_{1}$, and in other cases define:
$f(x)= \sup \{r \leq 1 : x \notin V_{r}\}$
Claim: $f$ is as required.
