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 
|- ( ph -> S C_ CC )
islpcn.p 
|- ( ph -> P e. CC )
Assertion islpcn 
|- ( ph -> ( P e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` S ) <-> A. e e. RR+ E. x e. ( S \ { P } ) ( abs ` ( x - P ) ) < e ) )

Proof

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