clslp

Description: The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	neindisj	$⊢ ((J \in Top \land S \subseteq X) \land (x \in cls (J) (S) \land n \in nei (J) (\{x\}))) \to n \cap S \neq \emptyset$
3	2	expr	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to (n \in nei (J) (\{x\}) \to n \cap S \neq \emptyset)$
4	3	adantr	$⊢ (((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \land \neg x \in S) \to (n \in nei (J) (\{x\}) \to n \cap S \neq \emptyset)$
5		difsn	$⊢ \neg x \in S \to S ∖ \{x\} = S$
6	5	ineq2d	$⊢ \neg x \in S \to n \cap (S ∖ \{x\}) = n \cap S$
7	6	neeq1d	$⊢ \neg x \in S \to (n \cap (S ∖ \{x\}) \neq \emptyset \leftrightarrow n \cap S \neq \emptyset)$
8	7	adantl	$⊢ (((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \land \neg x \in S) \to (n \cap (S ∖ \{x\}) \neq \emptyset \leftrightarrow n \cap S \neq \emptyset)$
9	4 8	sylibrd	$⊢ (((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \land \neg x \in S) \to (n \in nei (J) (\{x\}) \to n \cap (S ∖ \{x\}) \neq \emptyset)$
10	9	ex	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to (\neg x \in S \to (n \in nei (J) (\{x\}) \to n \cap (S ∖ \{x\}) \neq \emptyset))$
11	10	ralrimdv	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to (\neg x \in S \to \forall n \in nei (J) (\{x\}) n \cap (S ∖ \{x\}) \neq \emptyset)$
12		simpll	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to J \in Top$
13		simplr	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to S \subseteq X$
14	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
15	14	sselda	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to x \in X$
16	1	islp2	$⊢ (J \in Top \land S \subseteq X \land x \in X) \to (x \in limPt (J) (S) \leftrightarrow \forall n \in nei (J) (\{x\}) n \cap (S ∖ \{x\}) \neq \emptyset)$
17	12 13 15 16	syl3anc	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to (x \in limPt (J) (S) \leftrightarrow \forall n \in nei (J) (\{x\}) n \cap (S ∖ \{x\}) \neq \emptyset)$
18	11 17	sylibrd	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to (\neg x \in S \to x \in limPt (J) (S))$
19	18	orrd	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to (x \in S \lor x \in limPt (J) (S))$
20		elun	$⊢ x \in (S \cup limPt (J) (S)) \leftrightarrow (x \in S \lor x \in limPt (J) (S))$
21	19 20	sylibr	$⊢ ((J \in Top \land S \subseteq X) \land x \in cls (J) (S)) \to x \in (S \cup limPt (J) (S))$
22	21	ex	$⊢ (J \in Top \land S \subseteq X) \to (x \in cls (J) (S) \to x \in (S \cup limPt (J) (S)))$
23	22	ssrdv	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq S \cup limPt (J) (S)$
24	1	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$
25	1	lpsscls	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) \subseteq cls (J) (S)$
26	24 25	unssd	$⊢ (J \in Top \land S \subseteq X) \to S \cup limPt (J) (S) \subseteq cls (J) (S)$
27	23 26	eqssd	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = S \cup limPt (J) (S)$

Metamath Proof Explorer

Theorem clslp

Proof