Totally bounded, sequentially compact, complete, bounded, closed, equicontinuous $\Rightarrow$ compact?

Question

Related; When $K$ is compact, if $S\subset C_b(K)$ is closed,bounded and equicontinuous, then $S$ is compact? (ZF)

I just edited my whole question since i think it was a bit messy.

Here is my question.

Let $K$ be a separable compact metric space and $S\subset C(K,\mathbb{C})$.

Let $S$ be closed,bounded,uniformly equicontinuous on $K$, sequentially compact, totally bounded and complete.

Then is $S$ compact? (in ZF)

Thank you in advance!

Answer 1

You might want to read an answer to a slightly different question over at MathOverflow.

The short answer is: Arzelà–Ascoli does require (a weak form of) choice.