Dimension theorem (in infinite dimension) - all basis of any vector space have the same cardinality. I am reading a note from author Justin Tatch Moore, in which he proves the Dimension Theorem, which says that all the basis of a vector space have the same cardinality (in infinite dimension), using Zorn's Lemma. The text can be found HERE!
The idea is basically as follows: suppose that $A$ and $B$ are basis of the vector space $V$, and define $P$ to be the set consisting of all linear transformations $T$ from a subspace $W$ of
$V$ onto $W$ such that:

*

*$A \cap W$ and $B \cap W$ are each a basis for $W$, and

*the restriction of $T$ to $A \cap W$ is a bijection between $A \cap W$ and $B \cap W.$
then we show using Zorn's Lemma that $P$ has a maximal element, which is a transformation
$ T: W \rightarrow W $ with the properties (1) and (2). Note that if we show that $ W = V $, the theorem ends due to the propertie (2). Hence to do this the argument starts as in the figure below

My question is how to build two sets of sequences with the above four properties? The first two properties seem very reasonable, but the last two I have no idea how to do it. Can anyone help me with this?
 A: You can do it by induction.
Suppose $W$ is a proper subspace of $V$. Then $W$ can't contain $A$ so fix $a_{1}$ in $A$ which is not in $W$. Set $A_{1}=\{a_{1}\}$. Then $A_{1}$ is not contained in $W$.
Now for the induction hypothesis let $n\geq 1$ be given and assume we have constructed $A_{i}$ for $i\leq n$ and $B_{i}$ for $i<n$.
For the induction step we build $B_{n}$ first and then $A_{n+1}$.
Since $B$ is a basis for $V$, $A_{n}$ is contained in the span of $B$. Since $A_{n}$ is finite we only need a finite amount of $B$ to span all of $A_{n}$. In other words there is a finite subset $B'$ of $B$ such that $A_n$ is contained in the span of $B'$. So for our $B_{n}$ we can choose $B'\cup B_{n-1}$ (and if $n=1$ then say $B_{0}=\emptyset$). Note that we include $B_{n-1}$ in the union to make sure the sequence increases.
Now for $A_{n+1}$. By the same argument, $A$ has a finite subset $A'$ such that $B_{n}$ is contained in the span of $A'$. If $A_n\cup W$ spans $V$ then don't worry about making $A_{n+1}$ properly contain $A_n$, and just let $A_{n+1}=A'\cup A_{n}$. However if $A_{n}   \cup W$ doesn't span $V$ then, as $A$ is a basis for $V$, there must be some $v$ in $A$ that is not in $A_{n}\cup W$ so not in $A_{n}$ in particular. Now if $A_{n+1}=A'\cup A_{n}\cup\{v\}$ then we are ensured that $A_{n+1}$ properly contains $A_{n}$.
