Does ZF prove that proximity spaces are completely regular? (This is based on my earlier question, but I think this one would be easier to answer.)

Let $\langle X,\mathbf{\delta} \hspace{.01 in} \rangle$ be a separated proximity space, and let $\cal{T}\hspace{.04 in}$ be the induced topology on $X$.

Then, ZF proves that $\langle X,\cal{T}\hspace{.06 in} \rangle$ is regular Hausdorff, and

ZF + (Dependent Choice) $\;$proves that $\langle X,\cal{T}\hspace{.06 in} \rangle$ is completely regular.
Does ZF prove that $\langle X,\cal{T}\hspace{.06 in} \rangle$ is completely regular?

 A: The answer is no. In fact, it is consistent with ZF that $(*)$ there exists an infinite compact Hausdorff space $X$ such that every continuous function $f\colon X\to\mathbb R$ is constant, so that $X$ is not even completely Hausdorff.
A simple example can be given using a Fraenkel–Mostowski permutation model of ZFA (ZF with atoms). The general setup is as follows. We work in a model of ZFA + AC where the atoms form a set $A$. We are given a group $G$ of permutations of $A$, and a normal (= closed under the action of $G$ by conjugation) filter $F$ of subgroups of $G$ such that the stabilizer of every point $a\in A$ belongs to $F$. (The smallest such filter consists of all subgroups $H\subseteq G$ of finite support, i.e., such that $H$ includes the point-wise stabilizer of some finite subset of $A$.) The action of $G$ on $A$ can be extended to the whole universe so that $g(x)=\{g(y):y\in x\}$ for every set $x$. An object $x$ is symmetric if its stabilizer belongs to $F$, and it is hereditarily symmetric if every element of the transitive closure of $\{x\}$ is symmetric. Then one can show that the class $M$ of hereditarily symmetric objects is a transitive model of ZFA.
Now, in our particular case, assume that $A$ has the power of continuum so that we can put it in a 1–1 correspondence with $[0,1]$, and let $< $ be the induced order on $A$. We take for $G$ the group of all order-preserving permutations of $A$, and for $F$ the above mentioned minimal filter of subgroups with finite support. Let $M$ be the resulting permutation model. (This is a minor variant of the Mostowski ordered model, which has $(A,< )$ isomorphic to $\mathbb Q$ instead of $[0,1]$.)
$M$ contains the totally ordered set $(A,< )$, since every $g\in G$ preserves $< $. The induced order topology on $A$ is clearly Hausdorff, and it is also compact: if $C\in M$ is an open cover of $A$, it has a finite subcover $C'$ in the ambient model by compactness of $[0,1]$; we have $C'\in M$, because it is a finite subset of $M$.
On the other hand, let $f\colon A\to\mathbb R$ belong to $M$. Then there exists a finite subset $a=\{a_1<a_2<\dots<a_n\}\subseteq A$ such that every $g\in G$ that preserves $a$ also preserves $f$. This is easily seen to imply that $f$ is constant on every interval $(a_i,a_{i+1})$. (The only property of $\mathbb R$ we need here is that it is a pure set, and therefore all its elements are fixed by $G$.) In particular, if $f$ is continuous, it is constant.
In this way, we construct a model of ZFA + $(*)$. We can use the Jech–Sochor embedding theorem to obtain a model of ZF + $(*)$. Moreover, Halpern proved that the Boolean prime ideal theorem (BPI) holds in Mostowski’s ordered model; I suppose that BPI also holds in the model $M$ above by the same argument, hence $(*)$ is consistent with ZFA + BPI. I guess that it is also consistent with ZF + BPI, but I can’t vouch for it, as the Jech–Sochor theorem does not apply to BPI.
