Proof of "every finite dimensional vector space has a finite basis"

You can do it using the following theorem:

Theorem: In a finite-dimensional vector space, the length of every linearly independent list of vectors is less than or equal to the length of every spanning list of vectors.

I culled this formulation of the theorem from this question, where it is quoted as Theorem 2.23 from Axler's Linear Algebra Done Right, but I think remember seeing something very similar in Beezer's A First Course in Linear Algebra -- it should be a standard theorem. The proof (see the linked question for details) doesn't rely on any concept of dimension or basis.

Once you have that theorem, the proof of Theorem 2 proceeds as follows. We construct a linearly independent list of vectors by the process the text describes. This process must terminate because we know that there is a finite list of spanning vectors (fact 1), and the list of linearly independent vectors cannot grow longer than that list of spanning vectors (by the theorem I quoted). Thus the list must terminate at some finite length. After the list terminates, it is a maximal linearly independent set, thus a basis.

The proof of the corollary is as you surmised. Start with the empty list, and extend it to a basis.