Theorem lbsel

Description: An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lbsss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lbsss.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion	lbsel	⊢ ( ( 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lbsss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lbsss.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3	1 2	lbsss	⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉 )
4	3	sselda	⊢ ( ( 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ 𝑉 )