Metamath Proof Explorer


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 )