Separable Hilbert space weak sequential compactness

Separable Hilbert space weak sequential compactness

To preface, Banach-Alaoglu shows weak* sequential compactness of the unit
ball, and in Hilbert spaces weak* and weak convergence is the same. So I
already know that the unit ball of a Hilbert space is
weakly-sequentially-compact.
However, for separable Hilbert spaces, and let's just focus on $l^2$ as we
have an inner product isomorphism, there should be an easy constructive
proof, but I don't quite see it.
Let $x_n$ be a bounded sequence in $l^2$. By diagonalization we can obtain
a subsequence for which $x_{n_k} \to x_\infty$ pointwise. For that matter,
we can obtain a subsequence for which $\langle x_{n_k} - x_\infty, g_i
\rangle \to 0$ for a dense countable subset $g_i$ of $l^2$.
So, the question is, can we show that $x_\infty \in l^2$ ?
Alternatively, perhaps there is a different route. But the idea is that we
should not have to appeal to the axiom of choice (which Banach Alaoglu
does). Ok, so as I type this, I see
http://en.wikipedia.org/wiki/Banach%E2%80%93Alaoglu_theorem mentions
defining a metric using a dense set. But for some reason, I still don't
see how to complete the proof. What is missing? It appears that $x_{n_k}$
converges to $x_\infty$ in the metric defined in wikipedia.. hmm... but
why is that metric complete? Any ideas?