This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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