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 = U. J
Assertion maxlp 
|- ( J e. Top -> ( P e. ( ( limPt ` J ) ` X ) <-> ( P e. X /\ -. { P } e. J ) ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 
 |-  X = U. J
2 ssid 
 |-  X C_ X
3 1 lpss 
 |-  ( ( J e. Top /\ X C_ X ) -> ( ( limPt ` J ) ` X ) C_ X )
4 2 3 mpan2 
 |-  ( J e. Top -> ( ( limPt ` J ) ` X ) C_ X )
5 4 sseld 
 |-  ( J e. Top -> ( P e. ( ( limPt ` J ) ` X ) -> P e. X ) )
6 5 pm4.71rd 
 |-  ( J e. Top -> ( P e. ( ( limPt ` J ) ` X ) <-> ( P e. X /\ P e. ( ( limPt ` J ) ` X ) ) ) )
7 simpl 
 |-  ( ( J e. Top /\ P e. X ) -> J e. Top )
8 1 islp 
 |-  ( ( J e. Top /\ X C_ X ) -> ( P e. ( ( limPt ` J ) ` X ) <-> P e. ( ( cls ` J ) ` ( X \ { P } ) ) ) )
9 7 2 8 sylancl 
 |-  ( ( J e. Top /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` X ) <-> P e. ( ( cls ` J ) ` ( X \ { P } ) ) ) )
10 snssi 
 |-  ( P e. X -> { P } C_ X )
11 1 clsdif 
 |-  ( ( J e. Top /\ { P } C_ X ) -> ( ( cls ` J ) ` ( X \ { P } ) ) = ( X \ ( ( int ` J ) ` { P } ) ) )
12 10 11 sylan2 
 |-  ( ( J e. Top /\ P e. X ) -> ( ( cls ` J ) ` ( X \ { P } ) ) = ( X \ ( ( int ` J ) ` { P } ) ) )
13 12 eleq2d 
 |-  ( ( J e. Top /\ P e. X ) -> ( P e. ( ( cls ` J ) ` ( X \ { P } ) ) <-> P e. ( X \ ( ( int ` J ) ` { P } ) ) ) )
14 eldif 
 |-  ( P e. ( X \ ( ( int ` J ) ` { P } ) ) <-> ( P e. X /\ -. P e. ( ( int ` J ) ` { P } ) ) )
15 14 baib 
 |-  ( P e. X -> ( P e. ( X \ ( ( int ` J ) ` { P } ) ) <-> -. P e. ( ( int ` J ) ` { P } ) ) )
16 15 adantl 
 |-  ( ( J e. Top /\ P e. X ) -> ( P e. ( X \ ( ( int ` J ) ` { P } ) ) <-> -. P e. ( ( int ` J ) ` { P } ) ) )
17 snssi 
 |-  ( P e. ( ( int ` J ) ` { P } ) -> { P } C_ ( ( int ` J ) ` { P } ) )
18 17 adantl 
 |-  ( ( ( J e. Top /\ P e. X ) /\ P e. ( ( int ` J ) ` { P } ) ) -> { P } C_ ( ( int ` J ) ` { P } ) )
19 1 ntrss2 
 |-  ( ( J e. Top /\ { P } C_ X ) -> ( ( int ` J ) ` { P } ) C_ { P } )
20 10 19 sylan2 
 |-  ( ( J e. Top /\ P e. X ) -> ( ( int ` J ) ` { P } ) C_ { P } )
21 20 adantr 
 |-  ( ( ( J e. Top /\ P e. X ) /\ P e. ( ( int ` J ) ` { P } ) ) -> ( ( int ` J ) ` { P } ) C_ { P } )
22 18 21 eqssd 
 |-  ( ( ( J e. Top /\ P e. X ) /\ P e. ( ( int ` J ) ` { P } ) ) -> { P } = ( ( int ` J ) ` { P } ) )
23 1 ntropn 
 |-  ( ( J e. Top /\ { P } C_ X ) -> ( ( int ` J ) ` { P } ) e. J )
24 10 23 sylan2 
 |-  ( ( J e. Top /\ P e. X ) -> ( ( int ` J ) ` { P } ) e. J )
25 24 adantr 
 |-  ( ( ( J e. Top /\ P e. X ) /\ P e. ( ( int ` J ) ` { P } ) ) -> ( ( int ` J ) ` { P } ) e. J )
26 22 25 eqeltrd 
 |-  ( ( ( J e. Top /\ P e. X ) /\ P e. ( ( int ` J ) ` { P } ) ) -> { P } e. J )
27 snidg 
 |-  ( P e. X -> P e. { P } )
28 27 ad2antlr 
 |-  ( ( ( J e. Top /\ P e. X ) /\ { P } e. J ) -> P e. { P } )
29 isopn3i 
 |-  ( ( J e. Top /\ { P } e. J ) -> ( ( int ` J ) ` { P } ) = { P } )
30 29 adantlr 
 |-  ( ( ( J e. Top /\ P e. X ) /\ { P } e. J ) -> ( ( int ` J ) ` { P } ) = { P } )
31 28 30 eleqtrrd 
 |-  ( ( ( J e. Top /\ P e. X ) /\ { P } e. J ) -> P e. ( ( int ` J ) ` { P } ) )
32 26 31 impbida 
 |-  ( ( J e. Top /\ P e. X ) -> ( P e. ( ( int ` J ) ` { P } ) <-> { P } e. J ) )
33 32 notbid 
 |-  ( ( J e. Top /\ P e. X ) -> ( -. P e. ( ( int ` J ) ` { P } ) <-> -. { P } e. J ) )
34 16 33 bitrd 
 |-  ( ( J e. Top /\ P e. X ) -> ( P e. ( X \ ( ( int ` J ) ` { P } ) ) <-> -. { P } e. J ) )
35 9 13 34 3bitrd 
 |-  ( ( J e. Top /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` X ) <-> -. { P } e. J ) )
36 35 pm5.32da 
 |-  ( J e. Top -> ( ( P e. X /\ P e. ( ( limPt ` J ) ` X ) ) <-> ( P e. X /\ -. { P } e. J ) ) )
37 6 36 bitrd 
 |-  ( J e. Top -> ( P e. ( ( limPt ` J ) ` X ) <-> ( P e. X /\ -. { P } e. J ) ) )