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 ⊢ 𝐽 = ( 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 ) → 𝐽 ≠ ∅ )