A proof can be found here, but it seems that it uses AC. I would like to know if there is a proof for this fact without AC.
I came up with this question after seeing a proof of sequential compactness $\implies$ Compactness for metrizable topological spaces without using generalized Lebesgue's Number Lemma for sequentially compact metric spaces. Both proofs can be found here.
Best Answer
The result cannot be proved without the axiom of choice. For instance, let $X$ be an infinite set which contains no countably infinite subset (the existence of such a set is consistent with ZF), and give $X$ the discrete metric. Then $X$ is sequentially compact since there are no sequences in $X$ which take infinitely many different values so every sequence has a constant subsequence. But $X$ is not Lindelöf, since the open cover of $X$ by singletons has no countable subcover.