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 𝑋 = 𝐽
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 ‘ 𝐽 ) ‘ 𝑋 ) ↔ ( 𝑃𝑋 ∧ ¬ { 𝑃 } ∈ 𝐽 ) ) )