Metamath Proof Explorer

Theorem islpcn

Description: A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses islpcn.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
islpcn.p ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
Assertion islpcn ( 𝜑 → ( 𝑃 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )

Proof

Step Hyp Ref Expression
1 islpcn.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 islpcn.p ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
3 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
4 3 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
5 4 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
6 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
7 6 islp2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ⊆ ℂ ∧ 𝑃 ∈ ℂ ) → ( 𝑃 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
8 5 1 2 7 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
9 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑃 ∈ ℂ )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
13 3 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
14 13 blnei ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑃 ∈ ℂ ∧ 𝑒 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) )
15 10 11 12 14 syl3anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) )
16 15 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
18 ineq1 ⊢ ( 𝑛 = ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) = ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
19 18 neeq1d ⊢ ( 𝑛 = ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) → ( ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ↔ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
20 19 rspcva ⊢ ( ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) → ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
21 16 17 20 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
22 n0 ⊢ ( ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
23 21 22 sylib ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
24 elinel2 ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) )
26 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑆 ⊆ ℂ )
27 24 eldifad ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑥 ∈ 𝑆 )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑥 ∈ 𝑆 )
29 26 28 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑥 ∈ ℂ )
30 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑃 ∈ ℂ )
31 29 30 abssubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( abs ‘ ( 𝑥 − 𝑃 ) ) = ( abs ‘ ( 𝑃 − 𝑥 ) ) )
32 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
33 32 cnmetdval ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑃 − 𝑥 ) ) )
34 30 29 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑃 − 𝑥 ) ) )
35 31 34 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( abs ‘ ( 𝑥 − 𝑃 ) ) = ( 𝑃 ( abs ∘ − ) 𝑥 ) )
36 35 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( abs ‘ ( 𝑥 − 𝑃 ) ) = ( 𝑃 ( abs ∘ − ) 𝑥 ) )
37 elinel1 ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) )
38 37 adantl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) )
39 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
40 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑃 ∈ ℂ )
41 rpxr ⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ* )
42 41 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → 𝑒 ∈ ℝ* )
43 elbl ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑃 ∈ ℂ ∧ 𝑒 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 ) ) )
44 39 40 42 43 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 ) ) )
45 38 44 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( 𝑥 ∈ ℂ ∧ ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 ) )
46 45 simprd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 )
47 36 46 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
48 25 47 jca ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) → ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )
49 48 ex ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) )
50 49 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) )
51 50 eximdv ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑥 𝑥 ∈ ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ∩ ( 𝑆 ∖ { 𝑃 } ) ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) )
52 23 51 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )
53 df-rex ⊢ ( ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )
54 52 53 sylibr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
55 54 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) → ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
56 9 a1i ⊢ ( 𝜑 → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
57 13 neibl ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑃 ∈ ℂ ) → ( 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ↔ ( 𝑛 ⊆ ℂ ∧ ∃ 𝑒 ∈ ℝ+ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ) )
58 56 2 57 syl2anc ⊢ ( 𝜑 → ( 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ↔ ( 𝑛 ⊆ ℂ ∧ ∃ 𝑒 ∈ ℝ+ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ) )
59 58 simplbda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ) → ∃ 𝑒 ∈ ℝ+ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ) → ∃ 𝑒 ∈ ℝ+ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 )
61 nfv ⊢ Ⅎ 𝑒 𝜑
62 nfra1 ⊢ Ⅎ 𝑒 ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒
63 61 62 nfan ⊢ Ⅎ 𝑒 ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
64 nfv ⊢ Ⅎ 𝑒 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } )
65 63 64 nfan ⊢ Ⅎ 𝑒 ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) )
66 nfv ⊢ Ⅎ 𝑒 ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅
67 simp1l ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → 𝜑 )
68 simp2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → 𝑒 ∈ ℝ+ )
69 67 68 jca ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) )
70 rspa ⊢ ( ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
71 70 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
72 71 3adant3 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
73 simp3 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 )
74 53 biimpi ⊢ ( ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 → ∃ 𝑥 ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )
75 74 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )
76 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑒 ∈ ℝ+ )
77 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒
78 76 77 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
79 nfv ⊢ Ⅎ 𝑥 ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛
80 78 79 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 )
81 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 )
82 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑆 ⊆ ℂ )
83 eldifi ⊢ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) → 𝑥 ∈ 𝑆 )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑥 ∈ 𝑆 )
85 82 84 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑥 ∈ ℂ )
86 85 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑥 ∈ ℂ )
87 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → 𝑃 ∈ ℂ )
88 87 85 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑃 − 𝑥 ) ) )
89 87 85 abssubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → ( abs ‘ ( 𝑃 − 𝑥 ) ) = ( abs ‘ ( 𝑥 − 𝑃 ) ) )
90 88 89 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑥 − 𝑃 ) ) )
91 90 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) = ( abs ‘ ( 𝑥 − 𝑃 ) ) )
92 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 )
93 91 92 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 )
94 86 93 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( 𝑥 ∈ ℂ ∧ ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 ) )
95 94 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( 𝑥 ∈ ℂ ∧ ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 ) )
96 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
97 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑃 ∈ ℂ )
98 41 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑒 ∈ ℝ* )
99 96 97 98 43 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑃 ( abs ∘ − ) 𝑥 ) < 𝑒 ) ) )
100 95 99 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) )
101 100 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑥 ∈ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) )
102 81 101 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑥 ∈ 𝑛 )
103 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) )
104 102 103 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) ∧ ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ) → 𝑥 ∈ ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
105 104 ex ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) → 𝑥 ∈ ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) )
106 105 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) → 𝑥 ∈ ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) )
107 80 106 eximd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( ∃ 𝑥 ( 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ∧ ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) → ∃ 𝑥 𝑥 ∈ ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ) )
108 75 107 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ∃ 𝑥 𝑥 ∈ ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
109 n0 ⊢ ( ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) )
110 108 109 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
111 69 72 73 110 syl21anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 ) → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
112 111 3exp ⊢ ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) → ( 𝑒 ∈ ℝ+ → ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ) )
113 112 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ) → ( 𝑒 ∈ ℝ+ → ( ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) ) )
114 65 66 113 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ) → ( ∃ 𝑒 ∈ ℝ+ ( 𝑃 ( ball ‘ ( abs ∘ − ) ) 𝑒 ) ⊆ 𝑛 → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ) )
115 60 114 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) ∧ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ) → ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
116 115 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) → ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ )
117 55 116 impbida ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ( ( nei ‘ ( TopOpen ‘ ℂfld ) ) ‘ { 𝑃 } ) ( 𝑛 ∩ ( 𝑆 ∖ { 𝑃 } ) ) ≠ ∅ ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )
118 8 117 bitrd ⊢ ( 𝜑 → ( 𝑃 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝑆 ) ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ ( 𝑆 ∖ { 𝑃 } ) ( abs ‘ ( 𝑥 − 𝑃 ) ) < 𝑒 ) )