lpsscls

Description: The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007)

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

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	lpval	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) = \{x \| x \in cls (J) (S ∖ \{x\})\}$
3		difss	$⊢ S ∖ \{x\} \subseteq S$
4	1	clsss	$⊢ (J \in Top \land S \subseteq X \land S ∖ \{x\} \subseteq S) \to cls (J) (S ∖ \{x\}) \subseteq cls (J) (S)$
5	3 4	mp3an3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S ∖ \{x\}) \subseteq cls (J) (S)$
6	5	sseld	$⊢ (J \in Top \land S \subseteq X) \to (x \in cls (J) (S ∖ \{x\}) \to x \in cls (J) (S))$
7	6	abssdv	$⊢ (J \in Top \land S \subseteq X) \to \{x \| x \in cls (J) (S ∖ \{x\})\} \subseteq cls (J) (S)$
8	2 7	eqsstrd	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) \subseteq cls (J) (S)$

Metamath Proof Explorer