Theorem cssss

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

	Ref	Expression
Hypotheses	cssss.v	|- V = ( Base ` W )
	cssss.c	|- C = ( ClSubSp ` W )
Assertion	cssss	|- ( S e. C -> S C_ V )

Proof

Step	Hyp	Ref	Expression
1		cssss.v	|- V = ( Base ` W )
2		cssss.c	|- C = ( ClSubSp ` W )
3		eqid	|- ( ocv ` W ) = ( ocv ` W )
4	3 2	cssi	|- ( S e. C -> S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) )
5	1 3	ocvss	|- ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) C_ V
6	4 5	eqsstrdi	|- ( S e. C -> S C_ V )