Separable dual implies separable primal

If $X=\{0\}$, then $\{0\}$ itself is a finite dense subset of $X$, so the conclusion holds. Henceforth suppose $X\mathrm{\ne }\{0\}$.

By [F1], choose an at most countable norm-dense subset $S\subseteq X^{\ast }$. Enlarge it by the zero functional, so it is nonempty and [F1] supplies a sequence $(f_n{)}_{n\ge 0}$ whose range is $S$. This sequence is norm dense in $X^{\ast }$.

For each $n$, if $f_n=0$ set $C_n=\{0\}$; otherwise let $C_n=\{x\in X:\mathrm{\parallel }x\mathrm{\parallel }\le 1\text{ and }\mathrm{\mid }{f}_n(x)\mathrm{\mid }>\frac{1}{2}\mathrm{\parallel }{f}_n\mathrm{\parallel }\}\mathrm{.}$ The set $C_n$ is nonempty by [F2]. Apply ${\mathrm{A}\mathrm{C}}_{\omega }$ to the family $(C_n)$ and choose $x_n\in C_n$ for every $n$. This is the only selection of an arbitrary countable family in the proof.

Let ${\mathbb{K}}_0=\mathbb{Q}$ in the real case and ${\mathbb{K}}_0=\mathbb{Q}+i\mathbb{Q}$ in the complex case, and let $D$ be the ${\mathbb{K}}_0$-linear span of the sequence $(x_n)$. The field ${\mathbb{K}}_0$ is at most countable by [F4]. For each fixed number of summands, the coefficient-index tuples form a finite product of at most countable sets; the union over all finite lengths is at most countable by [F4]. Its image under evaluation is $D$, so $D$ is at most countable. Density of $\mathbb{Q}$ in $\mathbb{R}$ shows that $D$ is norm dense in the real or complex linear span of the $x_n$.

Let $g\in X^{\ast }$ vanish on $D$. Then $g(x_n)=0$ for every $n$. Given $\epsilon >0$, norm density of $(f_n)$ gives an $n$ with $\mathrm{\parallel }g-f_n\mathrm{\parallel }<\epsilon$. By the definition of $x_n$ in step 1.3, $\frac{1}{2}\mathrm{\parallel }{f}_n\mathrm{\parallel }\le \mathrm{\mid }{f}_n(x_n)\mathrm{\mid }=\mathrm{\mid }(f_n-g)(x_n)\mathrm{\mid }\le \mathrm{\parallel }{f}_n-g\mathrm{\parallel }<\epsilon ,$ where the first inequality is also true when $f_n=0$. Therefore $\mathrm{\parallel }g\mathrm{\parallel }\le \mathrm{\parallel }g-f_n\mathrm{\parallel }+\mathrm{\parallel }{f}_n\mathrm{\parallel }<3\epsilon$. Since this holds for every $\epsilon >0$, $g=0$.

Suppose that the norm closure $M=\bar{D}$ were a proper subset of $X$. It is a nonempty closed real-linear subspace, and in the complex case it is complex-linear because ${\mathbb{K}}_0$ is dense in $\mathbb{C}$. Choose $z\mathrm{\notin }M$. By [F3] there is a nonzero $h\in X^{\ast }$ strictly separating $z$ from $M$. Because $M$ is a subspace and $\mathrm{Re}h$ is bounded on one side there, scaling forces $\mathrm{Re}h(m)=0$ for every $m\in M$. In the complex case, applying this also to $im\in M$ gives $\mathrm{Im}h(m)=0$. Thus $h$ vanishes on $D$, contradicting step 2.2. Consequently $\bar{D}=X$.

The at most countable set $D$ is norm dense in $X$ by steps 2.1 and 3.1, so $X$ is separable by [F1]. The use of ${\mathrm{A}\mathrm{C}}_{\omega }$ is exactly the simultaneous choice in step 1.3 and the countable-union result in step 2.1; HB is used exactly in the separation step 3.1.