This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbsexg

Description: Every vector space has a basis. This theorem is an AC equivalent; this is the forward implication. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis lbsex.j 
|- J = ( LBasis ` W )
Assertion lbsexg 
|- ( ( CHOICE /\ W e. LVec ) -> J =/= (/) )

Proof

Step Hyp Ref Expression
1 lbsex.j 
 |-  J = ( LBasis ` W )
2 id 
 |-  ( W e. LVec -> W e. LVec )
3 fvex 
 |-  ( Base ` W ) e. _V
4 3 pwex 
 |-  ~P ( Base ` W ) e. _V
5 dfac10 
 |-  ( CHOICE <-> dom card = _V )
6 5 biimpi 
 |-  ( CHOICE -> dom card = _V )
7 4 6 eleqtrrid 
 |-  ( CHOICE -> ~P ( Base ` W ) e. dom card )
8 0ss 
 |-  (/) C_ ( Base ` W )
9 ral0 
 |-  A. x e. (/) -. x e. ( ( LSpan ` W ) ` ( (/) \ { x } ) )
10 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
12 1 10 11 lbsextg 
 |-  ( ( ( W e. LVec /\ ~P ( Base ` W ) e. dom card ) /\ (/) C_ ( Base ` W ) /\ A. x e. (/) -. x e. ( ( LSpan ` W ) ` ( (/) \ { x } ) ) ) -> E. s e. J (/) C_ s )
13 8 9 12 mp3an23 
 |-  ( ( W e. LVec /\ ~P ( Base ` W ) e. dom card ) -> E. s e. J (/) C_ s )
14 2 7 13 syl2anr 
 |-  ( ( CHOICE /\ W e. LVec ) -> E. s e. J (/) C_ s )
15 rexn0 
 |-  ( E. s e. J (/) C_ s -> J =/= (/) )
16 14 15 syl 
 |-  ( ( CHOICE /\ W e. LVec ) -> J =/= (/) )