Infinite dimensional weak topology is not first countable

Suppose $(U_n)$ is a countable weak local base at zero. For each $n$ the set of finite lists of functionals and positive radii defining a basic neighborhood $V_n\subseteq U_n$ is nonempty. Apply Countable Choice once to these sets, fixing such finite lists. Enumerate their entries by pairs of natural numbers, padding each finite list with zero functionals. This gives a sequence $(h_k)$ containing every chosen functional.

Fix $f\in X^{\ast }$. It is weakly continuous by F2. Some $U_n$ lies inside $\{\mathrm{\mid }f\mathrm{\mid }<1\}$, so $V_n$ lies there too. Scaling shows that $f$ vanishes on the common kernel of its finite defining list. For its coordinate map $A$, the rule $\mathrm{\ell }(Ax)=f(x)$ is well-defined by this kernel inclusion. Extend a finite basis of $A(X)$ to one of ${\mathbb{K}}^m$, and set $\mathrm{\ell }=0$ on added basis vectors. If $c_j$ are the values of the extension on standard coordinate vectors, then $f(x)={\sum }_j{c}_j(Ax{)}_j$. Hence $f$ is a finite linear combination of the defining list. Thus the algebraic span of $(h_k)$ is all of $X^{\ast }$.

Scan $(h_k)$ in order, retaining an entry precisely when it is outside the span of preceding retained entries. This deterministic rule gives either a finite basis or an infinite subsequence forming a countably infinite Hamel basis of $X^{\ast }$: every discarded entry is in the earlier retained span, while each retained entry preserves independence. The infinite outcome is impossible because $X^{\ast }$ is Banach and F4 is choice-free. Therefore $X^{\ast }$ has a finite basis $g_1,\dots ,g_d$.

The map $x\mapsto (g_1(x),\dots ,g_d(x))$ is injective: a kernel vector is killed by every member of their span $X^{\ast }$ and is zero by HB separation. But $d+1$ independent vectors in $X$ would have dependent images in ${\mathbb{K}}^d$, contradicting injectivity. Such vectors exist by finite induction from infinite dimension. This contradiction excludes the supplied countable local base. Countable Choice was used only in step 1.1 and HB only in this step. $\mathrm{\square }$