Arzelà--Ascoli for real $C(K)$ under Countable Choice and Dependent Choice: compact closure iff equicontinuous and pointwise bounded

If $\mathcal{F}=\mathrm{\varnothing }$, its closure is empty and compact, while both family properties hold vacuously. Hence assume $\mathcal{F}\mathrm{\ne }\mathrm{\varnothing }$. Suppose first that $\mathcal{F}$ is equicontinuous and pointwise bounded, and fix $\epsilon >0$. Let $\mathcal{U}$ contain every ball $B(a,r)$ with $a\in K$, $r>0$, and $\mathrm{\mid }f(x)-f(a)\mathrm{\mid }<\epsilon \mathrm{/}3$ for all $f\in \mathcal{F}$ whenever $d(x,a)<2r$. Equicontinuity makes $\mathcal{U}$ an open cover without selecting a radius for every $a$. By [L1] take a finite subcover $B(a_i,r_i)$, $i=1,\dots ,N$. Pointwise boundedness supplies finite bounds $M_i$ for the values $\mathrm{\mid }f(a_i)\mathrm{\mid }$. Partition the bounded box ${\prod }_{i=1}^N[-M_i,M_i]$ into finitely many boxes of coordinate diameter less than $\epsilon \mathrm{/}3$, and choose one member of $\mathcal{F}$ from each box met by an evaluation vector $(f(a_i){)}_i$. For any $f\in \mathcal{F}$, a chosen $g$ in the same box satisfies $\mathrm{\mid }f(a_i)-g(a_i)\mathrm{\mid }<\epsilon \mathrm{/}3$ for all $i$; if $x\in B(a_i,r_i)$, the two equicontinuity bounds give $\mathrm{\mid }f(x)-g(x)\mathrm{\mid }<\epsilon$. Thus these finitely many representatives form an $\epsilon$-net. The closure is totally bounded as well, by using an $\epsilon \mathrm{/}2$-net for $\mathcal{F}$ and approximating each point of its closure by a member of $\mathcal{F}$.

Conversely suppose the closure is compact. For $\epsilon >0$, [L3] supplies a finite $\epsilon \mathrm{/}3$-net $g_1,\dots ,g_N$ in the closure. By [L5], a common positive radius makes every $g_i$ vary by less than $\epsilon \mathrm{/}3$.

The closure of $\mathcal{F}$ is closed in the complete space of [L2], hence complete by [L3]. It is totally bounded by step 1.1, so [L3] makes it compact.

For $f\in \mathcal{F}$, choose $g_i$ within $\epsilon \mathrm{/}3$ in supremum distance. The two uniform-distance bounds and step 1.2 give $\mathrm{\mid }f(x)-f(y)\mathrm{\mid }<\epsilon$ whenever $d(x,y)$ is below the common radius.

The same finite net bounds $\mathrm{\mid }f(a)\mathrm{\mid }$ at each fixed $a\in K$, so $\mathcal{F}$ is pointwise bounded.

Step 2.1 proves the forward implication; steps 2.2 and 2.3 give equicontinuity and pointwise boundedness in the converse.