If I'm not mistaken there is another proof that BPI implies that any two bases of a vector space have the same cardinality. As has been noted earlier, if $(u_i)_{i \in I}$ and $(v_j)_{j\in j}$ are two bases of $V$ vector space over $K$ it suffices to show that there's an injection $I\to J$.
We're going to use the equivalence "BPI$\iff$ Compactness for propositional logic". For each $i\in I$ there exists a unique minimal finite set $J_i \subset J$ such that $u_i$ is spanned by $J_i$. For $i \in I, j\in J$ we create a propositional variable $P_{i,j}$ supposed to mean $f(i)=j$. Then we create a theory $T$ that contains all the $\neg (P_{i,j} \land P_{i, j'})$ when $j\neq j' \in J$, and $\neg (P_{i,j}\land P_{i',j})$ when $i\neq i' \in I$. This is supposed to mean "$f$ is injective". But obviously this isn't enough (otherwise one could prove that any set injects into another), as we need to express something like "$f(i)$ is defined for any $i\in I$". This is where we use the $J_i$ : we add to the theory the formulas $\displaystyle\bigvee_{j\in J_i} P_{i,j}$ for $i\in I$, which is a well defined formula (up to logical equivalence), as each $J_i$ is finite. Now if $T$ is satisfiable, then we have found our injection : assume $v$ is a model for $T$, then $f:=\{(i,j) \in I\times J\mid v(P_{i,j}) =1\}$ is an injection, whose domain is $I$. Compactness shows it's enough to have $T$ finitely satisfiable, and if $T_0$ is a finite subtheory of $T$, ot is contained in a finite subtheory $T_1$ which expresses (modulo our identification) that a certain finite subset $I_0\subset I$ is injected into $J$ with every $i\in I_0$ being sent into $J_i$. Now unless I'm making a mistake, this is possible, as it only uses the cardinality of bases for finite dimensional spaces, which is true without any sort of choice.
So $T$ is satisfiable, we have our injection, and symmetry + Cantor-Bernstein allow us to conclude

EDIT : I might actually be making a mistake, it's possible that a "Hall's mariage theorem" argument can't be avoided