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 =/= (/) )