Infinite dimensional vector space. Linearly independent subsets and spanning subsets This question is a follow up to this question:
The dimension of the real continuous functions as a vector space over $\mathbb{R}$ is not countable?
I realized that the answer I accepted used an implicit assumption: that if $V$ is a vector space and $S$ is a spanning subset and $L$ is a linearly independent subset of $V$, then there is an injective function $f:L\hookrightarrow S$.
This is clearly true for a finite-dimensional vector space, but for infinite-dimensional ones it is not so immediate.
I expect some form of choice is needed. I know that in ZF, the Axiom of Choice is equivalent to every vector space has a basis. And every proof I've seen that shows two different bases for an infinite dimensional vector space have the same cardinality uses some degree of choice (through the Ultrafilter Lemma). 
But does anyone know how much choice is needed to prove the proposition above, if any?
 A: The general statement "If $S$ is a spanning set, and $L$ is linearly independent then $|L|\leq|S|$" is unfamiliar to me, and I'm not sure it was investigated enough to merit an answer either. It does imply that every two bases have the same cardinality, so it does require some weak form of the axiom of choice. My guess would be that it requires a bit more than just every two bases have the same cardinality.
However, it seems that you are interested in the particular case of a countable basis. That is, if there is a countable basis, does every linearly independent set inject into a spanning set? Well, we can do better. We can prove that every linearly independent is countable.

Claim. If $V$ is a vector space over $K$, and $B$ is a countable basis for $V$, then every linearly independent set have size $\leq\aleph_0$.

If $B$ Is finite, then we know it to be true, and it is not the interesting case anyway.
Fix an enumeration of $B=\{b_n\mid n\in\Bbb N\}$. And let $L$ be a linearly independent set, and assume by contradiction that $|L|\nleq\aleph_0$. For every $\ell\in L$ take $\langle\ell_n\mid n\in\Bbb N\rangle$ to be the sequence of coefficients for the unique sum of $\ell$ in term of $b_n$'s. Note that all but finitely many are zero.
Clearly $\ell\mapsto\langle\ell_n\mid n\in\Bbb N\rangle$ is injective. Since $L$ is not countable, there is an uncountable subset of elements which have exactly the same non-zero indices, so without loss of generality it will be all of $L$, and without loss of generality those indices are $0,\ldots,n-1$.
Therefore $L$ itself is linearly independent as a subset of $W=\operatorname{span}\{b_i\mid i<n\}$. But this is a contradiction since $W$ has a finite dimension, and therefore every linearly independent set is finite, but $L$ is uncountable. $\quad\square$
