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 \land W \in LVec) \to J \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		lbsex.j	$⊢ J = LBasis (W)$
2		id	$⊢ W \in LVec \to W \in LVec$
3		fvex	$⊢ {Base}_{W} \in V$
4	3	pwex	$⊢ 𝒫 {Base}_{W} \in V$
5		dfac10	$⊢ CHOICE \leftrightarrow dom card = V$
6	5	biimpi	$⊢ CHOICE \to dom card = V$
7	4 6	eleqtrrid	$⊢ CHOICE \to 𝒫 {Base}_{W} \in dom card$
8		0ss	$⊢ \emptyset \subseteq {Base}_{W}$
9		ral0	$⊢ \forall x \in \emptyset \neg x \in LSpan (W) (\emptyset ∖ \{x\})$
10		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11		eqid	$⊢ LSpan (W) = LSpan (W)$
12	1 10 11	lbsextg	$⊢ ((W \in LVec \land 𝒫 {Base}_{W} \in dom card) \land \emptyset \subseteq {Base}_{W} \land \forall x \in \emptyset \neg x \in LSpan (W) (\emptyset ∖ \{x\})) \to \exists s \in J \emptyset \subseteq s$
13	8 9 12	mp3an23	$⊢ (W \in LVec \land 𝒫 {Base}_{W} \in dom card) \to \exists s \in J \emptyset \subseteq s$
14	2 7 13	syl2anr	$⊢ (CHOICE \land W \in LVec) \to \exists s \in J \emptyset \subseteq s$
15		rexn0	$⊢ \exists s \in J \emptyset \subseteq s \to J \neq \emptyset$
16	14 15	syl	$⊢ (CHOICE \land W \in LVec) \to J \neq \emptyset$