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

Metamath Proof Explorer

Theorem sscls

Description: A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007)

		Ref	Expression
	Hypothesis	clscld.1	$⊢ X = ⋃ J$
	Assertion	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		ssintub	$⊢ S \subseteq ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
3	1	clsval	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = ⋂ \{x \in Clsd (J) \| S \subseteq x\}$
4	2 3	sseqtrrid	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$