Direct proof from AC that every vector space has a basis? Let AC be the axiom of choice and VB be the proposition that every vector space has a basis. What's the "most direct" possible proof that AC$\implies$VB (in ZF)?
I know it's possible to prove Zorn's lemma (ZL) and then prove ZL$\implies$VB, and also to develop the theory of ordinals and then prove VB using transfinite induction. But, just out of curiosity, is there a more direct way?
I realize "more/most direct" is somewhat opinion based, but if you prefer, you could interpret my question as, "Can we prove AC$\implies$VB without ordinals and without explicitly mentioning (and without simply copying the argument of) ZL?"
 A: The axiom of choice by itself is useless. It just gives you a function. What can you do with it? Not that much, in most cases.
On the other hand, transfinite recursion is something that $\sf ZF$ itself can do pretty well already. And remember that the key point in transfinite recursion is that there is a function that tells you how to proceed to the $\alpha$ stage, assuming that you've done all the stages before $\alpha$.
Well, a choice function is a function. And it interfaces with transfinite recursion very well. Indeed, Zorn's Lemma and other similar equivalents were introduced to alleviate the need for transfinite recursion and induction. But any proof with Zorn's Lemma can be transformed into a proof using a choice function and transfinite recursion, including this one.
Fix a choice function from all the non-empty subsets of $V$. Now recursively add more and more vectors to your set, with the recursive rule being that if we have already gathered $\{v_i\mid i<\alpha\}$, then $v_\alpha$ is chosen to be any vector in $V\setminus\operatorname{span}(\{v_i\mid i<\alpha\})$. The only way we cannot make such choice is when what we gathered already is a basis; and so eventually the recursion must come to a halt, otherwise we are contradicting Hartogs' theorem, as it defines an injection from the class of ordinals into $V$, which is a set.
Now, we can, and should, also prove that this set of vectors is linearly independent. We can do that by induction; where we simply note that since $v_\alpha\notin\operatorname{span}(\{v_i\mid i<\alpha\})$, then it is not a linear combination of any finitely many $v_i$s for $i<\alpha$. Now, since the induction hypothesis is that those were already linearly independent, this completes the proof.
