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	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion	lbsexg	⊢ ( ( CHOICE ∧ 𝑊 ∈ LVec ) → 𝐽 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		lbsex.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2		id	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LVec )
3		fvex	⊢ ( Base ‘ 𝑊 ) ∈ V
4	3	pwex	⊢ 𝒫 ( Base ‘ 𝑊 ) ∈ V
5		dfac10	⊢ ( CHOICE ↔ dom card = V )
6	5	biimpi	⊢ ( CHOICE → dom card = V )
7	4 6	eleqtrrid	⊢ ( CHOICE → 𝒫 ( Base ‘ 𝑊 ) ∈ dom card )
8		0ss	⊢ ∅ ⊆ ( Base ‘ 𝑊 )
9		ral0	⊢ ∀ 𝑥 ∈ ∅ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ∅ ∖ { 𝑥 } ) )
10		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
12	1 10 11	lbsextg	⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 ( Base ‘ 𝑊 ) ∈ dom card ) ∧ ∅ ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ∅ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ∅ ∖ { 𝑥 } ) ) ) → ∃ 𝑠 ∈ 𝐽 ∅ ⊆ 𝑠 )
13	8 9 12	mp3an23	⊢ ( ( 𝑊 ∈ LVec ∧ 𝒫 ( Base ‘ 𝑊 ) ∈ dom card ) → ∃ 𝑠 ∈ 𝐽 ∅ ⊆ 𝑠 )
14	2 7 13	syl2anr	⊢ ( ( CHOICE ∧ 𝑊 ∈ LVec ) → ∃ 𝑠 ∈ 𝐽 ∅ ⊆ 𝑠 )
15		rexn0	⊢ ( ∃ 𝑠 ∈ 𝐽 ∅ ⊆ 𝑠 → 𝐽 ≠ ∅ )
16	14 15	syl	⊢ ( ( CHOICE ∧ 𝑊 ∈ LVec ) → 𝐽 ≠ ∅ )