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

Metamath Proof Explorer

Theorem lpss

Description: The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007)

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	lpss	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) \subseteq X$

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	lpsscls	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) \subseteq cls (J) (S)$
3	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
4	2 3	sstrd	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) \subseteq X$