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

Metamath Proof Explorer

Theorem lbsex

Description: Every vector space has a basis. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypothesis lbsex.j ⊢ J = LBasis ⁡ W
Assertion lbsex ⊢ W ∈ LVec → J ≠ ∅

Proof

Step Hyp Ref Expression
1 lbsex.j ⊢ J = LBasis ⁡ W
2 axac3 ⊢ CHOICE
3 1 lbsexg ⊢ CHOICE ∧ W ∈ LVec → J ≠ ∅
4 2 3 mpan ⊢ W ∈ LVec → J ≠ ∅