Metamath Proof Explorer


Theorem cnllycmp

Description: The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypothesis cnllycmp.1
|- J = ( TopOpen ` CCfld )
Assertion cnllycmp
|- J e. N-Locally Comp

Proof

Step Hyp Ref Expression
1 cnllycmp.1
 |-  J = ( TopOpen ` CCfld )
2 1 cnfldtop
 |-  J e. Top
3 cnxmet
 |-  ( abs o. - ) e. ( *Met ` CC )
4 1 cnfldtopn
 |-  J = ( MetOpen ` ( abs o. - ) )
5 4 mopni2
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ x e. J /\ y e. x ) -> E. r e. RR+ ( y ( ball ` ( abs o. - ) ) r ) C_ x )
6 3 5 mp3an1
 |-  ( ( x e. J /\ y e. x ) -> E. r e. RR+ ( y ( ball ` ( abs o. - ) ) r ) C_ x )
7 2 a1i
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> J e. Top )
8 3 a1i
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
9 elssuni
 |-  ( x e. J -> x C_ U. J )
10 9 ad2antrr
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> x C_ U. J )
11 1 cnfldtopon
 |-  J e. ( TopOn ` CC )
12 11 toponunii
 |-  CC = U. J
13 10 12 sseqtrrdi
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> x C_ CC )
14 simplr
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> y e. x )
15 13 14 sseldd
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> y e. CC )
16 rphalfcl
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
17 16 ad2antrl
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( r / 2 ) e. RR+ )
18 17 rpxrd
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( r / 2 ) e. RR* )
19 4 blopn
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ ( r / 2 ) e. RR* ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) e. J )
20 8 15 18 19 syl3anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) e. J )
21 blcntr
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ ( r / 2 ) e. RR+ ) -> y e. ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) )
22 8 15 17 21 syl3anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> y e. ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) )
23 opnneip
 |-  ( ( J e. Top /\ ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) e. J /\ y e. ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) e. ( ( nei ` J ) ` { y } ) )
24 7 20 22 23 syl3anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) e. ( ( nei ` J ) ` { y } ) )
25 blssm
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ ( r / 2 ) e. RR* ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ CC )
26 8 15 18 25 syl3anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ CC )
27 12 sscls
 |-  ( ( J e. Top /\ ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ CC ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) )
28 7 26 27 syl2anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) )
29 rpxr
 |-  ( r e. RR+ -> r e. RR* )
30 29 ad2antrl
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> r e. RR* )
31 rphalflt
 |-  ( r e. RR+ -> ( r / 2 ) < r )
32 31 ad2antrl
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( r / 2 ) < r )
33 4 blsscls
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC ) /\ ( ( r / 2 ) e. RR* /\ r e. RR* /\ ( r / 2 ) < r ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ ( y ( ball ` ( abs o. - ) ) r ) )
34 8 15 18 30 32 33 syl23anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ ( y ( ball ` ( abs o. - ) ) r ) )
35 simprr
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( y ( ball ` ( abs o. - ) ) r ) C_ x )
36 34 35 sstrd
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ x )
37 36 13 sstrd
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ CC )
38 12 ssnei2
 |-  ( ( ( J e. Top /\ ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) e. ( ( nei ` J ) ` { y } ) ) /\ ( ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) /\ ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ CC ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( ( nei ` J ) ` { y } ) )
39 7 24 28 37 38 syl22anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( ( nei ` J ) ` { y } ) )
40 vex
 |-  x e. _V
41 40 elpw2
 |-  ( ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ~P x <-> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ x )
42 36 41 sylibr
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ~P x )
43 39 42 elind
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) )
44 12 clscld
 |-  ( ( J e. Top /\ ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) C_ CC ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( Clsd ` J ) )
45 7 26 44 syl2anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( Clsd ` J ) )
46 15 abscld
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( abs ` y ) e. RR )
47 17 rpred
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( r / 2 ) e. RR )
48 46 47 readdcld
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( abs ` y ) + ( r / 2 ) ) e. RR )
49 eqid
 |-  { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } = { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) }
50 4 49 blcls
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ ( r / 2 ) e. RR* ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } )
51 8 15 18 50 syl3anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } )
52 simpr
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> z e. CC )
53 15 adantr
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> y e. CC )
54 52 53 abs2difd
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( abs ` z ) - ( abs ` y ) ) <_ ( abs ` ( z - y ) ) )
55 52 abscld
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( abs ` z ) e. RR )
56 46 adantr
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( abs ` y ) e. RR )
57 55 56 resubcld
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( abs ` z ) - ( abs ` y ) ) e. RR )
58 52 53 subcld
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( z - y ) e. CC )
59 58 abscld
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( abs ` ( z - y ) ) e. RR )
60 47 adantr
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( r / 2 ) e. RR )
61 letr
 |-  ( ( ( ( abs ` z ) - ( abs ` y ) ) e. RR /\ ( abs ` ( z - y ) ) e. RR /\ ( r / 2 ) e. RR ) -> ( ( ( ( abs ` z ) - ( abs ` y ) ) <_ ( abs ` ( z - y ) ) /\ ( abs ` ( z - y ) ) <_ ( r / 2 ) ) -> ( ( abs ` z ) - ( abs ` y ) ) <_ ( r / 2 ) ) )
62 57 59 60 61 syl3anc
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( ( ( abs ` z ) - ( abs ` y ) ) <_ ( abs ` ( z - y ) ) /\ ( abs ` ( z - y ) ) <_ ( r / 2 ) ) -> ( ( abs ` z ) - ( abs ` y ) ) <_ ( r / 2 ) ) )
63 54 62 mpand
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( abs ` ( z - y ) ) <_ ( r / 2 ) -> ( ( abs ` z ) - ( abs ` y ) ) <_ ( r / 2 ) ) )
64 52 53 abssubd
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
65 eqid
 |-  ( abs o. - ) = ( abs o. - )
66 65 cnmetdval
 |-  ( ( y e. CC /\ z e. CC ) -> ( y ( abs o. - ) z ) = ( abs ` ( y - z ) ) )
67 15 66 sylan
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( y ( abs o. - ) z ) = ( abs ` ( y - z ) ) )
68 64 67 eqtr4d
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( abs ` ( z - y ) ) = ( y ( abs o. - ) z ) )
69 68 breq1d
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( abs ` ( z - y ) ) <_ ( r / 2 ) <-> ( y ( abs o. - ) z ) <_ ( r / 2 ) ) )
70 55 56 60 lesubadd2d
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( ( abs ` z ) - ( abs ` y ) ) <_ ( r / 2 ) <-> ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) ) )
71 63 69 70 3imtr3d
 |-  ( ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) /\ z e. CC ) -> ( ( y ( abs o. - ) z ) <_ ( r / 2 ) -> ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) ) )
72 71 ralrimiva
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> A. z e. CC ( ( y ( abs o. - ) z ) <_ ( r / 2 ) -> ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) ) )
73 oveq2
 |-  ( w = z -> ( y ( abs o. - ) w ) = ( y ( abs o. - ) z ) )
74 73 breq1d
 |-  ( w = z -> ( ( y ( abs o. - ) w ) <_ ( r / 2 ) <-> ( y ( abs o. - ) z ) <_ ( r / 2 ) ) )
75 74 ralrab
 |-  ( A. z e. { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) <-> A. z e. CC ( ( y ( abs o. - ) z ) <_ ( r / 2 ) -> ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) ) )
76 72 75 sylibr
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> A. z e. { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) )
77 ssralv
 |-  ( ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } -> ( A. z e. { w e. CC | ( y ( abs o. - ) w ) <_ ( r / 2 ) } ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) -> A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) ) )
78 51 76 77 sylc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) )
79 brralrspcev
 |-  ( ( ( ( abs ` y ) + ( r / 2 ) ) e. RR /\ A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ ( ( abs ` y ) + ( r / 2 ) ) ) -> E. s e. RR A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ s )
80 48 78 79 syl2anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> E. s e. RR A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ s )
81 eqid
 |-  ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) = ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) )
82 1 81 cnheibor
 |-  ( ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) C_ CC -> ( ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) e. Comp <-> ( ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( Clsd ` J ) /\ E. s e. RR A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ s ) ) )
83 37 82 syl
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) e. Comp <-> ( ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( Clsd ` J ) /\ E. s e. RR A. z e. ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ( abs ` z ) <_ s ) ) )
84 45 80 83 mpbir2and
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) e. Comp )
85 oveq2
 |-  ( u = ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) -> ( J |`t u ) = ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) )
86 85 eleq1d
 |-  ( u = ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) -> ( ( J |`t u ) e. Comp <-> ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) e. Comp ) )
87 86 rspcev
 |-  ( ( ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) /\ ( J |`t ( ( cls ` J ) ` ( y ( ball ` ( abs o. - ) ) ( r / 2 ) ) ) ) e. Comp ) -> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. Comp )
88 43 84 87 syl2anc
 |-  ( ( ( x e. J /\ y e. x ) /\ ( r e. RR+ /\ ( y ( ball ` ( abs o. - ) ) r ) C_ x ) ) -> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. Comp )
89 6 88 rexlimddv
 |-  ( ( x e. J /\ y e. x ) -> E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. Comp )
90 89 rgen2
 |-  A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. Comp
91 isnlly
 |-  ( J e. N-Locally Comp <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. Comp ) )
92 2 90 91 mpbir2an
 |-  J e. N-Locally Comp