Metamath Proof Explorer

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 ⊢X=⋃J
Assertion maxlp ⊢J∈Top→P∈limPt⁡J⁡X↔P∈X∧¬P∈J

Proof

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