Theorem maxlp

Description: A point is a limit point of the whole space iff the singleton of the point is not open. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	lpfval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	maxlp	⊢ ( 𝐽 ∈ Top → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ¬ { 𝑃 } ∈ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2		ssid	⊢ 𝑋 ⊆ 𝑋
3	1	lpss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
4	2 3	mpan2	⊢ ( 𝐽 ∈ Top → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
5	4	sseld	⊢ ( 𝐽 ∈ Top → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) → 𝑃 ∈ 𝑋 ) )
6	5	pm4.71rd	⊢ ( 𝐽 ∈ Top → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ) )
7		simpl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → 𝐽 ∈ Top )
8	1	islp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ { 𝑃 } ) ) ) )
9	7 2 8	sylancl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ { 𝑃 } ) ) ) )
10		snssi	⊢ ( 𝑃 ∈ 𝑋 → { 𝑃 } ⊆ 𝑋 )
11	1	clsdif	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ { 𝑃 } ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
12	10 11	sylan2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ { 𝑃 } ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
13	12	eleq2d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋 ∖ { 𝑃 } ) ) ↔ 𝑃 ∈ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) ) )
14		eldif	⊢ ( 𝑃 ∈ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) ↔ ( 𝑃 ∈ 𝑋 ∧ ¬ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
15	14	baib	⊢ ( 𝑃 ∈ 𝑋 → ( 𝑃 ∈ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) ↔ ¬ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
16	15	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) ↔ ¬ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) )
17		snssi	⊢ ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) → { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) )
18	17	adantl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) → { 𝑃 } ⊆ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) )
19	1	ntrss2	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ⊆ { 𝑃 } )
20	10 19	sylan2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ⊆ { 𝑃 } )
21	20	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ⊆ { 𝑃 } )
22	18 21	eqssd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) → { 𝑃 } = ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) )
23	1	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ 𝐽 )
24	10 23	sylan2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ 𝐽 )
25	24	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ 𝐽 )
26	22 25	eqeltrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) → { 𝑃 } ∈ 𝐽 )
27		snidg	⊢ ( 𝑃 ∈ 𝑋 → 𝑃 ∈ { 𝑃 } )
28	27	ad2antlr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ { 𝑃 } ∈ 𝐽 ) → 𝑃 ∈ { 𝑃 } )
29		isopn3i	⊢ ( ( 𝐽 ∈ Top ∧ { 𝑃 } ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) = { 𝑃 } )
30	29	adantlr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ { 𝑃 } ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) = { 𝑃 } )
31	28 30	eleqtrrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) ∧ { 𝑃 } ∈ 𝐽 ) → 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) )
32	26 31	impbida	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ { 𝑃 } ∈ 𝐽 ) )
33	32	notbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( ¬ 𝑃 ∈ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ¬ { 𝑃 } ∈ 𝐽 ) )
34	16 33	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ { 𝑃 } ) ) ↔ ¬ { 𝑃 } ∈ 𝐽 ) )
35	9 13 34	3bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ¬ { 𝑃 } ∈ 𝐽 ) )
36	35	pm5.32da	⊢ ( 𝐽 ∈ Top → ( ( 𝑃 ∈ 𝑋 ∧ 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ↔ ( 𝑃 ∈ 𝑋 ∧ ¬ { 𝑃 } ∈ 𝐽 ) ) )
37	6 36	bitrd	⊢ ( 𝐽 ∈ Top → ( 𝑃 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ¬ { 𝑃 } ∈ 𝐽 ) ) )