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 ∈ LVec → J ≠ ∅

Proof

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