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={\mathrm{Base}}_W$$
	cssss.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
Assertion	cssss	$$⊢S\in C\to S\subseteq V$$

Proof

Step	Hyp	Ref	Expression
1		cssss.v	$$⊢V={\mathrm{Base}}_W$$
2		cssss.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
3		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
4	3 2	cssi	$$⊢S\in C\to S=\mathrm{ocv}\left(W\right)\left(\mathrm{ocv}\left(W\right)\left(S\right)\right)$$
5	1 3	ocvss	$$⊢\mathrm{ocv}\left(W\right)\left(\mathrm{ocv}\left(W\right)\left(S\right)\right)\subseteq V$$
6	4 5	eqsstrdi	$$⊢S\in C\to S\subseteq V$$