I mean, in order to define dimension, we have to know that bases exist (and all have the same cardinality). Which means that before I can use the notion of "di

I mean, in order to define dimension, we have to know that bases exist (and all have the same cardinality). Which means that before I can use the notion of "dimension", I have to know about bases. I mean I suppose you could just restrict the definition of dimension to vector spaces that have bases, and then you wouldn't have to. I guess that's what you're implicitly suggesting, that dimension would just not apply to vector spaces that don't have bases. That would make sense. But I'm used to thinking of dimension as, well, a function of vector spaces, not a partial function, so as I was thinking of it, you have to prove they all have bases before you can use it!