lpcls

Description: The limit points of the closure of a subset are the same as the limit points of the set in a T_1 space. (Contributed by Mario Carneiro, 26-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lpcls.1	$⊢ X = ⋃ J$
2		t1top	$⊢ J \in Fre \to J \in Top$
3	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
4	3	ssdifssd	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) ∖ \{x\} \subseteq X$
5	1	clsss3	$⊢ (J \in Top \land cls (J) (S) ∖ \{x\} \subseteq X) \to cls (J) (cls (J) (S) ∖ \{x\}) \subseteq X$
6	4 5	syldan	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (cls (J) (S) ∖ \{x\}) \subseteq X$
7	2 6	sylan	$⊢ (J \in Fre \land S \subseteq X) \to cls (J) (cls (J) (S) ∖ \{x\}) \subseteq X$
8	7	sseld	$⊢ (J \in Fre \land S \subseteq X) \to (x \in cls (J) (cls (J) (S) ∖ \{x\}) \to x \in X)$
9		ssdifss	$⊢ S \subseteq X \to S ∖ \{x\} \subseteq X$
10	1	clscld	$⊢ (J \in Top \land S ∖ \{x\} \subseteq X) \to cls (J) (S ∖ \{x\}) \in Clsd (J)$
11	2 9 10	syl2an	$⊢ (J \in Fre \land S \subseteq X) \to cls (J) (S ∖ \{x\}) \in Clsd (J)$
12	11	adantr	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to cls (J) (S ∖ \{x\}) \in Clsd (J)$
13	1	t1sncld	$⊢ (J \in Fre \land x \in X) \to \{x\} \in Clsd (J)$
14	13	adantlr	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to \{x\} \in Clsd (J)$
15		uncld	$⊢ (\{x\} \in Clsd (J) \land cls (J) (S ∖ \{x\}) \in Clsd (J)) \to \{x\} \cup cls (J) (S ∖ \{x\}) \in Clsd (J)$
16	14 12 15	syl2anc	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to \{x\} \cup cls (J) (S ∖ \{x\}) \in Clsd (J)$
17	1	sscls	$⊢ (J \in Top \land S ∖ \{x\} \subseteq X) \to S ∖ \{x\} \subseteq cls (J) (S ∖ \{x\})$
18	2 9 17	syl2an	$⊢ (J \in Fre \land S \subseteq X) \to S ∖ \{x\} \subseteq cls (J) (S ∖ \{x\})$
19		ssundif	$⊢ S \subseteq \{x\} \cup cls (J) (S ∖ \{x\}) \leftrightarrow S ∖ \{x\} \subseteq cls (J) (S ∖ \{x\})$
20	18 19	sylibr	$⊢ (J \in Fre \land S \subseteq X) \to S \subseteq \{x\} \cup cls (J) (S ∖ \{x\})$
21	20	adantr	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to S \subseteq \{x\} \cup cls (J) (S ∖ \{x\})$
22	1	clsss2	$⊢ (\{x\} \cup cls (J) (S ∖ \{x\}) \in Clsd (J) \land S \subseteq \{x\} \cup cls (J) (S ∖ \{x\})) \to cls (J) (S) \subseteq \{x\} \cup cls (J) (S ∖ \{x\})$
23	16 21 22	syl2anc	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to cls (J) (S) \subseteq \{x\} \cup cls (J) (S ∖ \{x\})$
24		ssundif	$⊢ cls (J) (S) \subseteq \{x\} \cup cls (J) (S ∖ \{x\}) \leftrightarrow cls (J) (S) ∖ \{x\} \subseteq cls (J) (S ∖ \{x\})$
25	23 24	sylib	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to cls (J) (S) ∖ \{x\} \subseteq cls (J) (S ∖ \{x\})$
26	1	clsss2	$⊢ (cls (J) (S ∖ \{x\}) \in Clsd (J) \land cls (J) (S) ∖ \{x\} \subseteq cls (J) (S ∖ \{x\})) \to cls (J) (cls (J) (S) ∖ \{x\}) \subseteq cls (J) (S ∖ \{x\})$
27	12 25 26	syl2anc	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to cls (J) (cls (J) (S) ∖ \{x\}) \subseteq cls (J) (S ∖ \{x\})$
28	27	sseld	$⊢ ((J \in Fre \land S \subseteq X) \land x \in X) \to (x \in cls (J) (cls (J) (S) ∖ \{x\}) \to x \in cls (J) (S ∖ \{x\}))$
29	28	ex	$⊢ (J \in Fre \land S \subseteq X) \to (x \in X \to (x \in cls (J) (cls (J) (S) ∖ \{x\}) \to x \in cls (J) (S ∖ \{x\})))$
30	29	com23	$⊢ (J \in Fre \land S \subseteq X) \to (x \in cls (J) (cls (J) (S) ∖ \{x\}) \to (x \in X \to x \in cls (J) (S ∖ \{x\})))$
31	8 30	mpdd	$⊢ (J \in Fre \land S \subseteq X) \to (x \in cls (J) (cls (J) (S) ∖ \{x\}) \to x \in cls (J) (S ∖ \{x\}))$
32	2	adantr	$⊢ (J \in Fre \land S \subseteq X) \to J \in Top$
33	2 3	sylan	$⊢ (J \in Fre \land S \subseteq X) \to cls (J) (S) \subseteq X$
34	33	ssdifssd	$⊢ (J \in Fre \land S \subseteq X) \to cls (J) (S) ∖ \{x\} \subseteq X$
35	1	sscls	$⊢ (J \in Top \land S \subseteq X) \to S \subseteq cls (J) (S)$
36	2 35	sylan	$⊢ (J \in Fre \land S \subseteq X) \to S \subseteq cls (J) (S)$
37	36	ssdifd	$⊢ (J \in Fre \land S \subseteq X) \to S ∖ \{x\} \subseteq cls (J) (S) ∖ \{x\}$
38	1	clsss	$⊢ (J \in Top \land cls (J) (S) ∖ \{x\} \subseteq X \land S ∖ \{x\} \subseteq cls (J) (S) ∖ \{x\}) \to cls (J) (S ∖ \{x\}) \subseteq cls (J) (cls (J) (S) ∖ \{x\})$
39	32 34 37 38	syl3anc	$⊢ (J \in Fre \land S \subseteq X) \to cls (J) (S ∖ \{x\}) \subseteq cls (J) (cls (J) (S) ∖ \{x\})$
40	39	sseld	$⊢ (J \in Fre \land S \subseteq X) \to (x \in cls (J) (S ∖ \{x\}) \to x \in cls (J) (cls (J) (S) ∖ \{x\}))$
41	31 40	impbid	$⊢ (J \in Fre \land S \subseteq X) \to (x \in cls (J) (cls (J) (S) ∖ \{x\}) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
42	1	islp	$⊢ (J \in Top \land cls (J) (S) \subseteq X) \to (x \in limPt (J) (cls (J) (S)) \leftrightarrow x \in cls (J) (cls (J) (S) ∖ \{x\}))$
43	3 42	syldan	$⊢ (J \in Top \land S \subseteq X) \to (x \in limPt (J) (cls (J) (S)) \leftrightarrow x \in cls (J) (cls (J) (S) ∖ \{x\}))$
44	2 43	sylan	$⊢ (J \in Fre \land S \subseteq X) \to (x \in limPt (J) (cls (J) (S)) \leftrightarrow x \in cls (J) (cls (J) (S) ∖ \{x\}))$
45	1	islp	$⊢ (J \in Top \land S \subseteq X) \to (x \in limPt (J) (S) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
46	2 45	sylan	$⊢ (J \in Fre \land S \subseteq X) \to (x \in limPt (J) (S) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
47	41 44 46	3bitr4d	$⊢ (J \in Fre \land S \subseteq X) \to (x \in limPt (J) (cls (J) (S)) \leftrightarrow x \in limPt (J) (S))$
48	47	eqrdv	$⊢ (J \in Fre \land S \subseteq X) \to limPt (J) (cls (J) (S)) = limPt (J) (S)$

Metamath Proof Explorer

Theorem lpcls

Proof