Theorem cssss

Description: A closed subspace is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cssss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion	cssss	⊢ ( 𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		cssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		cssss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
4	3 2	cssi	⊢ ( 𝑆 ∈ 𝐶 → 𝑆 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) )
5	1 3	ocvss	⊢ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ⊆ 𝑉
6	4 5	eqsstrdi	⊢ ( 𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑉 )