Say $V$ is a vector space over some field.
Lemma Suppose $A,B,C\subset V$, $A\cup B$ spans $V$ and $B\cup C$ is independent. For every $c\in C$ there exists $a\in A$ such that if $A'=A\setminus\{a\}$ and $B'=B\cup\{c\}$ then $A'\cup B'$ spans $V$.
(Write $c$ as a linear combination of elements of $A\cup B$ and note that some element of $A$ must appear with a non-zero coefficient, since $B\cup C$ is independent...)
Cor Suppose $A$ spans $V$ and $C$ is independent. If $A$ is finite then $|A|\ge|C|$.
Proof: Let $A_0=A$, $B_0=\emptyset$, $C_0=C$. Apply the lemma repeatedly, setting $A_{n+1}=A_n'$, $B_{n+1}=B_n'$, $C_{n+1}=C_n'=C_n\setminus \{c\}$. If $|A|<|C|$ then there exists $n$ so that $A_n=\emptyset$ and $C_n\ne\emptyset$; hence $B_n$ is a proper subset of the independent set $C$ and $B_n$ spans $V$, contradiction.
Question: Is there a way to get the Corollary from the Lemma if $A$ is infinite?
"My work so far:" The obvious transfinite recursion. The problem is if $\alpha$ is a limit ordinal: I can't imagine what' $A_\alpha$ and $B_\alpha$ could be other than $\bigcap_{\beta<\alpha}A_\beta$ and $\bigcup_{\beta<\alpha}B_\beta$, but in that case I see no reason that $A_\alpha\cup B_\alpha$ should span $V$.
The reason I suspect I may just be missing something is that in Finite Dimensional Vector Spaces Halmos comments that he tends to give proofs that can be generalized to the infinite-dimensional case.
Edit: It seems likely the answer is no, since nobody's come up with a yes. This raises the question "ok, how do you prove the corollary for infinite $A$?" In fact there's a very simple proof of the corollary for infinite $A$ on Wikipedia; see the Answer below for a paraphrase.
For anyone missing the point:
Exercise. (i) Show that "maximal independent set" is equivalent to "minimal spanning set". (ii) Explain why nonetheless the first phrase always comes up in a proof that every vector space has a basis, never the second..
It seems likely the answer is no, since nobody's come up with a yes. This raises the question "ok, how do you prove the corollary for infinite $A$?" In fact there's a very simple proof of the corollary for infinite $A$ on Wikipedia;. Here's the same proof, in a version that seems somewhat cleaner to me:
Suppose $A$ is infinite. Since any independent set is contained in a maximal independent set, wlog $C$ is actually a basis. For $c\in C$ let $\pi_c$ be the corresponding coordinate functional, so that $$x=\sum_{c\in C}\pi_c(x)c$$for every $x\in V$.
Let $S(x)$ be the support of $x\in V$: $$S(x)=\{c\in C:\pi_c(x)\ne0\}.$$Since $A$ spans $V$ it's clear that $$S(x)\subset S(A):=\bigcup_{a\in A}S(a)$$for every $x\in V$. We certainly have $$S(c)=\{c\}\quad(c\in C),$$ so $$C\subset S(A).$$And since $A$ is infinite and each $S(a)$ is finite it follows that $$|S(A)|\le|A|.$$
I feel so silly not having come up with that on my own.