In Halmos' Finite-Dimensional Vector Spaces, section I.8 has a proof of the Steinitz exchange lemma, which says that if $V$ is a vector space, $S$ is a finite independent subset of $V$, and $T$ is a finite generating subset of $V$, then the cardinality of $T$ is not less than the cardinality of $S$.
Having proved this, Halmos goes on to assert that "The number of elements in any basis of a finite-dimensional vector space $V$ is the same as in any other basis." But this is not quite right, because the lemma only proves that any two finite bases have the same number of elements. I don't see where it has been ruled out that there might still somehow be infinite bases lurking in a vector space with a finite basis.
There is a theorem in section I.7 which says that any independent set can be extended to a basis. Halmos assumes that the independent set is finite, but I think the proof still goes through if we assume it possibly infinite, so that if there are any infinite independent subsets, we can extend it to an infinite basis. So it seems we need to rule out the possibility that a vector space with a finite basis might have an infinite independent set.
Have I made a mistake anywhere in the above? And if not, can we repair the gap in this theorem easily?
I took a quick look at Roman's Advanced Linear Algebra and it seems to have the same defect of assuming that in a vector space with a finite spanning set, all bases must be finite. I'm not able to find where this is proved. Roman has a proof that works for arbitrary vector spaces, but it uses cardinal arithmetic, which I am not familiar with. Is there any easier way?