Can this proof of existence of a Hamel basis using transfinite recursion be shortened/simplified? This is (I hope) a solution to Problem 112 in A. Shen and N. K. Vereshchagin, Basic Set Theory (AMS 2002).
It is - I thought! - a semi-routine exercise, part of whose purpose is to enlighten the reader as to "what transfinite induction is and why it is always replaced by Zorn's Lemma" [from the blurb].
So, I'm moderately confident that the proof below is valid; also, given its context, I'm not surprised that it's longer and messier than a proof of the same result using Zorn's Lemma would surely be.
However, I'm learning on my own, and I still feel clumsy and awkward in my use of set theory - it has never become a "natural language" for me - so, I'd like to know whether or not I've made unnecessarily heavy weather of this proof (as I did with some earlier exercises in the book).
The book is excellent for self-study, by the way, and one of a small number of mathematical texts which I've found positively pleasurable to read.
$\newcommand{\powerset}{\mathscr{P}}$
$\newcommand{\sspan}[1]{\left\langle#1\right\rangle}$
$\DeclareMathOperator{\ham}{ham}$
The result to be proved is:

Any linearly independent set $S \subset V$ in any linear space $V$ can
  be extended to a Hamel basis $S' \supset S$.

The authors first prove this theorem themselves, using an auxiliary well-ordered set $I$, of cardinality greater than that of $V$.  They use transfinite recursion to construct a partial function $f$, defined on a proper initial segment of $I$, taking values in $V$; and they show that the union of $S$ with the range of this function $f$ constitutes a Hamel basis of $V$, as required.  Then they write:

We could also have avoided the use of an auxiliary set $I$ of large
  cardinality by introducing a well-ordering on $V$.  At each step we
  c0nsider some element $v \in V$; if it is not a linear combination of
  current basis elements, then we add $v$ to the basis; otherwise the
  basis remains unchanged.
Problem 112.  Provide missing details in this proof.

I don't know how transfinite recursion is normally presented, so I quote in full a theorem which they proved earlier (changing the notation for the least element of a well-ordered set from '$0$' to '$\bot$', to avoid confusion with the zero element of $V$):

Let $A$ be a well-ordered set, and $B$ an arbitrary set.  Let a
  recursive rule be given, that is, a mapping $F$ whose arguments are an
  element $x \in A$ and a function $g: [\bot, x) \to B$, and whose value
  is an element of $B$.  Then there exists exactly one function $f: A \to B$
  such that
  $$ f(x) = F\big(x, f|_{[\bot, x)}\big) $$
  for all $x \in A$.

Choose separate well-orderings for $S$ and $V \setminus S$, and well-order $V$ as
$S + (V \setminus S)$.
In the theorem just quoted, take $A = V$, and $B = \powerset(V)$.
For $x \in V$ and $f: V \to \powerset(V)$, define:
$$
f(x-) = \bigcup_{w < x} f(w), \\
\ham(f) = \{ x \in V : x \notin \sspan{f(x-)} \}.
$$
[I'm accustomed, from some time long ago, to using the notation '$\sspan{X}$' for the subspace spanned by a subset $X$ of a vector space, but can this notation be used without explanation, as I've just done?]
From the theorem, it follows that there exists a unique function $f: V \to \powerset(V)$ such that, for all $x \in V$:
$$
f(x) =
\begin{cases}
f(x-) & \text{if } x \notin \ham(f) \\
f(x-) \cup \{x\} & \text{if } x \in \ham(f)
\end{cases}
$$
For all $x \in V$, if $w \leqslant x$ and $w \in \ham(f)$, then $w \in f(w) \subseteq f(x-) \subseteq f(x)$; so, $f(x) \supseteq \ham(f) \cap [\bot, x]$.
Conversely, also, $f(x) \subseteq \ham(f) \cap [\bot, x]$. This is proved by transfinite induction on $x$, thus: if $f(w) \subseteq \ham(f) \cap [\bot, w]$ for all $w < x$, then
$f(x-) \subseteq \ham(f) \cap [\bot, x)$, and so $f(x) \subseteq \ham(f) \cap [\bot, x]$.
We have proved $f(x) = \ham(f) \cap [\bot, x]$, for all $x \in V$.
Hence, $f(x-) = \ham(f) \cap [\bot, x)$ for all $x \in V$.
Therefore, for all $x \in V$, $x \in \ham(f)$ if and only if
$x \notin \sspan{\ham(f) \cap [\bot, x)}$.
In particular, because $S$ is linearly independent, and because it is an initial segment of $V$, for all $x \in S$ we have $x \notin \sspan{[\bot, x)}$, therefore $x \in \ham(f)$. So, $S \subseteq \ham(f)$.
If $F$ is a non-empty finite subset of $\ham(f)$, let $x$ be its largest element (w.r.t. the well-ordering of $V$); then $x \notin \sspan{F \setminus \{x\}}$.  Hence, $\ham(f)$ is
linearly independent.
Also, for all $x \in V$, we have $x \in \sspan{f(x)} \subseteq \sspan{\ham(f)}$. So, $\ham(f)$ spans $V$.
Therefore, $\ham(f)$ is a Hamel basis of $V$, which extends $S$.  Q.E.D.
[I had to break off from writing this question, yesterday, in order to go to bed; and when trying to sleep, I managed to simplify and shorten the proof.  I really only managed to complete it today, because it wasn't as "routine" as I imagined.  It doesn't look quite so clumsy now, but the question still seems worth asking.]
D'oh!  Wouldn't a much simpler approach have been to use transfinite recursion to define a function from $V$ into a two-element set, such as $\{0, 1\}$, or $\{false, true\}$, instead of $\powerset(V)$?  I'll think about it tomorrow - I don't want another exhausting bedtime, when I find it's not as simple as it looks!
(Is there a tag for 'confounded-idiocy'?)
 A: You are essentially correct. The simplest way of thinking about it, putting aside the full formality of transfinite recursion argument (which is really just cluttering the beauty of these proofs), is to go about this whole thing in the most obvious way you'd expect.
Choose some vector, then choose a vector from the complement of the span of the previous one; then choose some vector from the complement of the span of the first two, and so on, by transfinite recursion. At the end, the recursion has to stop because the vector space is just a set, and you will be left with a basis.
Fleshing this idea a little bit, let $V$ be a vector space, and $C$ a choice function from subsets of $V$. We define by transfinite recursion a $\subseteq$-increasing sequence of sets, $B_\alpha$ all of which are linearly independent.
Suppose that for all $\gamma<\alpha$, $B_\gamma$ was defined. Then $B_{<\alpha}=\bigcup_{\gamma<\alpha}B_\gamma$, is a linearly independent set (as the increasing union of linearly independent sets is a linearly independent set). If $F$ is undefined on $V\setminus\langle B_{<\alpha}\rangle$, then it is empty and $B_{<\alpha}$ is a linearly independent set which spans $V$, therefore it is a basis for $V$; otherwise let $B_\alpha=B_{<\alpha}\cup\{F(V\setminus\langle B_{<\alpha}\rangle)\}$. 
We argue that there is some step in the construction where the recursion has to halt, otherwise we found an injection from $\sf Ord$ into $V$, which is impossible1 since $V$ is a set, and $\sf Ord$ is a proper class.
If you'd like, you can full formalize this proof by defining $f$ and arguing there is a unique function etc. etc., but the essence is in the proof above, and it's much clearer too.

1 As a set theorist, $V$ denotes the universe. So writing that there is no injection from $\sf Ord$ into $V$ made me feel strange from the inside.
A: Here's the much simpler argument I had in mind last night, when I realised what a fool I'd been.
$\newcommand{\powerset}{\mathscr{P}}$
$\newcommand{\sspan}[1]{\left\langle#1\right\rangle}$
It's about as simple as Asaf Karagila's answer above, and it meets the requirement of Problem 112, which is to use a well-ordering on $V$, rather than a sufficiently large ordinal or [other] well-ordered set, as an indexing set for a family of elements or subsets of $V$.
For the latter kind of argument, it makes little difference to its complexity whether you choose to construct a family of elements of $V$ (as in the authors' proof, only briefly sketched above), or on the other hand, a family of subsets of $V$ (as in Karagila's proof); whereas, in the kind of argument that uses a well-ordering of $V$, it was a bad initial choice that I made to construct a function from $V$ into $\powerset(V)$, when I should have constructed [the characteristic function of] a subset of $V$ directly.
I now think that it was not so much my specific discomfort with set theory (real though that is), nor an excessive impulse towards formality - that may have played a part, too, but I felt I needed to take great care over my argument, to control the unexpected intricacy of what I had expected to be a straightforward exercise - but this bad initial choice of proof strategy, accompanied by mental rigidity and tunnel vision (a more general kind of mathematical disability!), that largely accounts for the sense of clumsiness and awkwardness about my proof, which led me to post my question.
I now feel quite sure it was an argument of the following kind that the authors had in mind, and expected the reader to come up with; but it will be interesting to see if there are more suggestions.
As before, well-order $V$ as a sum $S + (V \setminus S)$.
Abusing notation if necessary, let $2 = \{0, 1\}$, with $0$ signifying 'false', and $1$ signifying 'true'.  Recursively, construct a function $\chi: V \to 2$, where, for all $x \in V$, $\chi(x)$ is $0$ or $1$ according to whether $x$ is or is not a linear combination of finitely many elements of $V$ strictly less than $x$.
This is simpler than asking if $x$ is a combination of  elements $w < x$ satisfying $\chi(w) = 1$, although that would also work.
Actually, it's so simple, it doesn't even need the theorem of transfinite recursion!  The definition:
$$
\chi(x) =
\begin{cases}
0 & \text{if } x \in    \sspan{[\bot, x)} \\
1 & \text{if } x \notin \sspan{[\bot, x)}
\end{cases}
$$
is already perfectly explicit.
Define:
$$
S' \left[ = \chi^{-1}(1) \right] =  \{x \in V : x \notin \sspan{[\bot, x)}\}.
$$
So, we didn't really need $\chi$ at all - but I'll leave it in, if only as a salutary embarrassing reminder of the persistence of tunnel vision even when you think you've seen the light at the end of the tunnel!
The fact that $S'$ extends $S$ is obvious, because $S$ is linearly independent, and an initial segment of $V$.
The fact that $S'$ itself is linearly independent is proved in the same way as before, viz. by taking the largest element of a finite subset $F \subseteq S'$ w.r.t. the ordering of $V$.
That $S'$ spans $V$ is proved by transfinite induction on $x \in V$, thus: suppose $w \in \sspan{S'}$ for all $w < x$; then $[\bot, x) \subseteq \sspan{S'}$; and either $x \in S' \subseteq \sspan{S'}$, or else $x \in \sspan{[\bot, x)} \subseteq \sspan{S'}$. Q.E.D.
(I think that's all there is to it, but it seems almost too good to be true, so I may have slipped up.)
