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 C S V


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 C S = ocv W ocv W S
5 1 3 ocvss ocv W ocv W S V
6 4 5 eqsstrdi S C S V