This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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 ∈ 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