Metamath Proof Explorer

Theorem tpr2rico

Description: For any point of an open set of the usual topology on ( RR X. RR ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the ( l ^ +oo ) norm X . (Contributed by Thierry Arnoux, 21-Sep-2017)

Ref Expression
Hypotheses tpr2rico.0 
|- J = ( topGen ` ran (,) )
tpr2rico.1 
|- G = ( u e. RR , v e. RR |-> ( u + ( _i x. v ) ) )
tpr2rico.2 
|- B = ran ( x e. ran (,) , y e. ran (,) |-> ( x X. y ) )
Assertion tpr2rico 
|- ( ( A e. ( J tX J ) /\ X e. A ) -> E. r e. B ( X e. r /\ r C_ A ) )

Proof

Step Hyp Ref Expression
1 tpr2rico.0 
 |-  J = ( topGen ` ran (,) )
2 tpr2rico.1 
 |-  G = ( u e. RR , v e. RR |-> ( u + ( _i x. v ) ) )
3 tpr2rico.2 
 |-  B = ran ( x e. ran (,) , y e. ran (,) |-> ( x X. y ) )
4 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
5 4 ixxf 
 |-  (,) : ( RR* X. RR* ) --> ~P RR*
6 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR* -> (,) Fn ( RR* X. RR* ) )
7 5 6 mp1i 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> (,) Fn ( RR* X. RR* ) )
8 elssuni 
 |-  ( A e. ( J tX J ) -> A C_ U. ( J tX J ) )
9 retop 
 |-  ( topGen ` ran (,) ) e. Top
10 1 9 eqeltri 
 |-  J e. Top
11 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
12 1 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
13 11 12 eqtr4i 
 |-  RR = U. J
14 10 10 13 13 txunii 
 |-  ( RR X. RR ) = U. ( J tX J )
15 8 14 sseqtrrdi 
 |-  ( A e. ( J tX J ) -> A C_ ( RR X. RR ) )
16 15 ad2antrr 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> A C_ ( RR X. RR ) )
17 simplr 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> X e. A )
18 16 17 sseldd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> X e. ( RR X. RR ) )
19 xp1st 
 |-  ( X e. ( RR X. RR ) -> ( 1st ` X ) e. RR )
20 18 19 syl 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 1st ` X ) e. RR )
21 simpr 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> d e. RR+ )
22 21 rpred 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> d e. RR )
23 22 rehalfcld 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( d / 2 ) e. RR )
24 20 23 resubcld 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) - ( d / 2 ) ) e. RR )
25 24 rexrd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) - ( d / 2 ) ) e. RR* )
26 20 23 readdcld 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) + ( d / 2 ) ) e. RR )
27 26 rexrd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) + ( d / 2 ) ) e. RR* )
28 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ ( ( 1st ` X ) - ( d / 2 ) ) e. RR* /\ ( ( 1st ` X ) + ( d / 2 ) ) e. RR* ) -> ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) e. ran (,) )
29 7 25 27 28 syl3anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) e. ran (,) )
30 xp2nd 
 |-  ( X e. ( RR X. RR ) -> ( 2nd ` X ) e. RR )
31 18 30 syl 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 2nd ` X ) e. RR )
32 31 23 resubcld 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) - ( d / 2 ) ) e. RR )
33 32 rexrd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) - ( d / 2 ) ) e. RR* )
34 31 23 readdcld 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) + ( d / 2 ) ) e. RR )
35 34 rexrd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) + ( d / 2 ) ) e. RR* )
36 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ ( ( 2nd ` X ) - ( d / 2 ) ) e. RR* /\ ( ( 2nd ` X ) + ( d / 2 ) ) e. RR* ) -> ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) e. ran (,) )
37 7 33 35 36 syl3anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) e. ran (,) )
38 eqidd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
39 xpeq1 
 |-  ( x = ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) -> ( x X. y ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. y ) )
40 39 eqeq2d 
 |-  ( x = ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) -> ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( x X. y ) <-> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. y ) ) )
41 xpeq2 
 |-  ( y = ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. y ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
42 41 eqeq2d 
 |-  ( y = ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) -> ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. y ) <-> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) )
43 40 42 rspc2ev 
 |-  ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) e. ran (,) /\ ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) e. ran (,) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) -> E. x e. ran (,) E. y e. ran (,) ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( x X. y ) )
44 29 37 38 43 syl3anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> E. x e. ran (,) E. y e. ran (,) ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( x X. y ) )
45 eqid 
 |-  ( x e. ran (,) , y e. ran (,) |-> ( x X. y ) ) = ( x e. ran (,) , y e. ran (,) |-> ( x X. y ) )
46 vex 
 |-  x e. _V
47 vex 
 |-  y e. _V
48 46 47 xpex 
 |-  ( x X. y ) e. _V
49 45 48 elrnmpo 
 |-  ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. ran ( x e. ran (,) , y e. ran (,) |-> ( x X. y ) ) <-> E. x e. ran (,) E. y e. ran (,) ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) = ( x X. y ) )
50 44 49 sylibr 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. ran ( x e. ran (,) , y e. ran (,) |-> ( x X. y ) ) )
51 50 3 eleqtrrdi 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B )
52 51 ralrimiva 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> A. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B )
53 xpss 
 |-  ( RR X. RR ) C_ ( _V X. _V )
54 53 18 sseldi 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> X e. ( _V X. _V ) )
55 20 rexrd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 1st ` X ) e. RR* )
56 21 rphalfcld 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( d / 2 ) e. RR+ )
57 20 56 ltsubrpd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) - ( d / 2 ) ) < ( 1st ` X ) )
58 20 56 ltaddrpd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 1st ` X ) < ( ( 1st ` X ) + ( d / 2 ) ) )
59 elioo1 
 |-  ( ( ( ( 1st ` X ) - ( d / 2 ) ) e. RR* /\ ( ( 1st ` X ) + ( d / 2 ) ) e. RR* ) -> ( ( 1st ` X ) e. ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) <-> ( ( 1st ` X ) e. RR* /\ ( ( 1st ` X ) - ( d / 2 ) ) < ( 1st ` X ) /\ ( 1st ` X ) < ( ( 1st ` X ) + ( d / 2 ) ) ) ) )
60 25 27 59 syl2anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) e. ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) <-> ( ( 1st ` X ) e. RR* /\ ( ( 1st ` X ) - ( d / 2 ) ) < ( 1st ` X ) /\ ( 1st ` X ) < ( ( 1st ` X ) + ( d / 2 ) ) ) ) )
61 55 57 58 60 mpbir3and 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 1st ` X ) e. ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) )
62 31 rexrd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 2nd ` X ) e. RR* )
63 31 56 ltsubrpd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) - ( d / 2 ) ) < ( 2nd ` X ) )
64 31 56 ltaddrpd 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 2nd ` X ) < ( ( 2nd ` X ) + ( d / 2 ) ) )
65 elioo1 
 |-  ( ( ( ( 2nd ` X ) - ( d / 2 ) ) e. RR* /\ ( ( 2nd ` X ) + ( d / 2 ) ) e. RR* ) -> ( ( 2nd ` X ) e. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) <-> ( ( 2nd ` X ) e. RR* /\ ( ( 2nd ` X ) - ( d / 2 ) ) < ( 2nd ` X ) /\ ( 2nd ` X ) < ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
66 33 35 65 syl2anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) e. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) <-> ( ( 2nd ` X ) e. RR* /\ ( ( 2nd ` X ) - ( d / 2 ) ) < ( 2nd ` X ) /\ ( 2nd ` X ) < ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
67 62 63 64 66 mpbir3and 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( 2nd ` X ) e. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) )
68 61 67 jca 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) e. ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) /\ ( 2nd ` X ) e. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
69 elxp7 
 |-  ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) <-> ( X e. ( _V X. _V ) /\ ( ( 1st ` X ) e. ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) /\ ( 2nd ` X ) e. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) )
70 54 68 69 sylanbrc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
71 70 ralrimiva 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> A. d e. RR+ X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) )
72 mnfle 
 |-  ( ( ( 1st ` X ) - ( d / 2 ) ) e. RR* -> -oo <_ ( ( 1st ` X ) - ( d / 2 ) ) )
73 25 72 syl 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> -oo <_ ( ( 1st ` X ) - ( d / 2 ) ) )
74 pnfge 
 |-  ( ( ( 1st ` X ) + ( d / 2 ) ) e. RR* -> ( ( 1st ` X ) + ( d / 2 ) ) <_ +oo )
75 27 74 syl 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 1st ` X ) + ( d / 2 ) ) <_ +oo )
76 mnfxr 
 |-  -oo e. RR*
77 pnfxr 
 |-  +oo e. RR*
78 ioossioo 
 |-  ( ( ( -oo e. RR* /\ +oo e. RR* ) /\ ( -oo <_ ( ( 1st ` X ) - ( d / 2 ) ) /\ ( ( 1st ` X ) + ( d / 2 ) ) <_ +oo ) ) -> ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) C_ ( -oo (,) +oo ) )
79 76 77 78 mpanl12 
 |-  ( ( -oo <_ ( ( 1st ` X ) - ( d / 2 ) ) /\ ( ( 1st ` X ) + ( d / 2 ) ) <_ +oo ) -> ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) C_ ( -oo (,) +oo ) )
80 73 75 79 syl2anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) C_ ( -oo (,) +oo ) )
81 ioomax 
 |-  ( -oo (,) +oo ) = RR
82 80 81 sseqtrdi 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) C_ RR )
83 mnfle 
 |-  ( ( ( 2nd ` X ) - ( d / 2 ) ) e. RR* -> -oo <_ ( ( 2nd ` X ) - ( d / 2 ) ) )
84 33 83 syl 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> -oo <_ ( ( 2nd ` X ) - ( d / 2 ) ) )
85 pnfge 
 |-  ( ( ( 2nd ` X ) + ( d / 2 ) ) e. RR* -> ( ( 2nd ` X ) + ( d / 2 ) ) <_ +oo )
86 35 85 syl 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( 2nd ` X ) + ( d / 2 ) ) <_ +oo )
87 ioossioo 
 |-  ( ( ( -oo e. RR* /\ +oo e. RR* ) /\ ( -oo <_ ( ( 2nd ` X ) - ( d / 2 ) ) /\ ( ( 2nd ` X ) + ( d / 2 ) ) <_ +oo ) ) -> ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) C_ ( -oo (,) +oo ) )
88 76 77 87 mpanl12 
 |-  ( ( -oo <_ ( ( 2nd ` X ) - ( d / 2 ) ) /\ ( ( 2nd ` X ) + ( d / 2 ) ) <_ +oo ) -> ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) C_ ( -oo (,) +oo ) )
89 84 86 88 syl2anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) C_ ( -oo (,) +oo ) )
90 89 81 sseqtrdi 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) C_ RR )
91 xpss12 
 |-  ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) C_ RR /\ ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) C_ RR ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( RR X. RR ) )
92 82 90 91 syl2anc 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( RR X. RR ) )
93 92 sselda 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) -> x e. ( RR X. RR ) )
94 93 expcom 
 |-  ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> x e. ( RR X. RR ) ) )
95 94 ancld 
 |-  ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) ) )
96 95 imdistanri 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) -> ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) )
97 15 adantr 
 |-  ( ( A e. ( J tX J ) /\ ( X e. A /\ d e. RR+ /\ x e. ( RR X. RR ) ) ) -> A C_ ( RR X. RR ) )
98 simpr1 
 |-  ( ( A e. ( J tX J ) /\ ( X e. A /\ d e. RR+ /\ x e. ( RR X. RR ) ) ) -> X e. A )
99 97 98 sseldd 
 |-  ( ( A e. ( J tX J ) /\ ( X e. A /\ d e. RR+ /\ x e. ( RR X. RR ) ) ) -> X e. ( RR X. RR ) )
100 99 3anassrs 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> X e. ( RR X. RR ) )
101 simpr 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> x e. ( RR X. RR ) )
102 simplr 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> d e. RR+ )
103 102 rphalfcld 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( d / 2 ) e. RR+ )
104 2 cnre2csqima 
 |-  ( ( X e. ( RR X. RR ) /\ x e. ( RR X. RR ) /\ ( d / 2 ) e. RR+ ) -> ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) ) )
105 100 101 103 104 syl3anc 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) ) )
106 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
107 2 1 106 cnrehmeo 
 |-  G e. ( ( J tX J ) Homeo ( TopOpen ` CCfld ) )
108 106 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
109 108 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
110 14 109 hmeof1o 
 |-  ( G e. ( ( J tX J ) Homeo ( TopOpen ` CCfld ) ) -> G : ( RR X. RR ) -1-1-onto-> CC )
111 f1of 
 |-  ( G : ( RR X. RR ) -1-1-onto-> CC -> G : ( RR X. RR ) --> CC )
112 107 110 111 mp2b 
 |-  G : ( RR X. RR ) --> CC
113 112 a1i 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> G : ( RR X. RR ) --> CC )
114 113 100 ffvelrnd 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( G ` X ) e. CC )
115 112 a1i 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> G : ( RR X. RR ) --> CC )
116 115 ffvelrnda 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( G ` x ) e. CC )
117 sqsscirc2 
 |-  ( ( ( ( G ` X ) e. CC /\ ( G ` x ) e. CC ) /\ d e. RR+ ) -> ( ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) -> ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) )
118 114 116 102 117 syl21anc 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) -> ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) )
119 118 imp 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) ) -> ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d )
120 102 rpxrd 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> d e. RR* )
121 120 adantr 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> d e. RR* )
122 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
123 121 122 jctil 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( ( abs o. - ) e. ( *Met ` CC ) /\ d e. RR* ) )
124 114 adantr 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( G ` X ) e. CC )
125 116 adantr 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( G ` x ) e. CC )
126 124 125 jca 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( ( G ` X ) e. CC /\ ( G ` x ) e. CC ) )
127 eqid 
 |-  ( abs o. - ) = ( abs o. - )
128 127 cnmetdval 
 |-  ( ( ( G ` x ) e. CC /\ ( G ` X ) e. CC ) -> ( ( G ` x ) ( abs o. - ) ( G ` X ) ) = ( abs ` ( ( G ` x ) - ( G ` X ) ) ) )
129 125 124 128 syl2anc 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( ( G ` x ) ( abs o. - ) ( G ` X ) ) = ( abs ` ( ( G ` x ) - ( G ` X ) ) ) )
130 simpr 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d )
131 129 130 eqbrtrd 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( ( G ` x ) ( abs o. - ) ( G ` X ) ) < d )
132 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ d e. RR* ) /\ ( ( G ` X ) e. CC /\ ( G ` x ) e. CC ) ) -> ( ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) <-> ( ( G ` x ) ( abs o. - ) ( G ` X ) ) < d ) )
133 132 biimpar 
 |-  ( ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ d e. RR* ) /\ ( ( G ` X ) e. CC /\ ( G ` x ) e. CC ) ) /\ ( ( G ` x ) ( abs o. - ) ( G ` X ) ) < d ) -> ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) )
134 123 126 131 133 syl21anc 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( abs ` ( ( G ` x ) - ( G ` X ) ) ) < d ) -> ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) )
135 119 134 syldan 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) ) -> ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) )
136 135 ex 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( ( ( abs ` ( Re ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) /\ ( abs ` ( Im ` ( ( G ` x ) - ( G ` X ) ) ) ) < ( d / 2 ) ) -> ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) )
137 105 136 syld 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) )
138 f1ocnv 
 |-  ( G : ( RR X. RR ) -1-1-onto-> CC -> `' G : CC -1-1-onto-> ( RR X. RR ) )
139 107 110 138 mp2b 
 |-  `' G : CC -1-1-onto-> ( RR X. RR )
140 f1ofun 
 |-  ( `' G : CC -1-1-onto-> ( RR X. RR ) -> Fun `' G )
141 139 140 ax-mp 
 |-  Fun `' G
142 f1odm 
 |-  ( `' G : CC -1-1-onto-> ( RR X. RR ) -> dom `' G = CC )
143 139 142 ax-mp 
 |-  dom `' G = CC
144 116 143 eleqtrrdi 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( G ` x ) e. dom `' G )
145 funfvima 
 |-  ( ( Fun `' G /\ ( G ` x ) e. dom `' G ) -> ( ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) -> ( `' G ` ( G ` x ) ) e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) ) )
146 141 144 145 sylancr 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( ( G ` x ) e. ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) -> ( `' G ` ( G ` x ) ) e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) ) )
147 107 110 mp1i 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> G : ( RR X. RR ) -1-1-onto-> CC )
148 f1ocnvfv1 
 |-  ( ( G : ( RR X. RR ) -1-1-onto-> CC /\ x e. ( RR X. RR ) ) -> ( `' G ` ( G ` x ) ) = x )
149 147 101 148 syl2anc 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( `' G ` ( G ` x ) ) = x )
150 149 eleq1d 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( ( `' G ` ( G ` x ) ) e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) <-> x e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) ) )
151 150 biimpd 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( ( `' G ` ( G ` x ) ) e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) -> x e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) ) )
152 137 146 151 3syld 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) -> ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> x e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) ) )
153 152 imp 
 |-  ( ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( RR X. RR ) ) /\ x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) -> x e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) )
154 96 153 syl 
 |-  ( ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) /\ x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) -> x e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) )
155 154 ex 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( x e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> x e. ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) ) )
156 155 ssrdv 
 |-  ( ( ( A e. ( J tX J ) /\ X e. A ) /\ d e. RR+ ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) )
157 156 ralrimiva 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> A. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) )
158 2 mpofun 
 |-  Fun G
159 158 a1i 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> Fun G )
160 15 sselda 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> X e. ( RR X. RR ) )
161 f1odm 
 |-  ( G : ( RR X. RR ) -1-1-onto-> CC -> dom G = ( RR X. RR ) )
162 107 110 161 mp2b 
 |-  dom G = ( RR X. RR )
163 160 162 eleqtrrdi 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> X e. dom G )
164 simpr 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> X e. A )
165 funfvima 
 |-  ( ( Fun G /\ X e. dom G ) -> ( X e. A -> ( G ` X ) e. ( G " A ) ) )
166 165 imp 
 |-  ( ( ( Fun G /\ X e. dom G ) /\ X e. A ) -> ( G ` X ) e. ( G " A ) )
167 159 163 164 166 syl21anc 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> ( G ` X ) e. ( G " A ) )
168 hmeoima 
 |-  ( ( G e. ( ( J tX J ) Homeo ( TopOpen ` CCfld ) ) /\ A e. ( J tX J ) ) -> ( G " A ) e. ( TopOpen ` CCfld ) )
169 107 168 mpan 
 |-  ( A e. ( J tX J ) -> ( G " A ) e. ( TopOpen ` CCfld ) )
170 106 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
171 170 elmopn2 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> ( ( G " A ) e. ( TopOpen ` CCfld ) <-> ( ( G " A ) C_ CC /\ A. m e. ( G " A ) E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) ) ) )
172 122 171 ax-mp 
 |-  ( ( G " A ) e. ( TopOpen ` CCfld ) <-> ( ( G " A ) C_ CC /\ A. m e. ( G " A ) E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) ) )
173 172 simprbi 
 |-  ( ( G " A ) e. ( TopOpen ` CCfld ) -> A. m e. ( G " A ) E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) )
174 169 173 syl 
 |-  ( A e. ( J tX J ) -> A. m e. ( G " A ) E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) )
175 174 adantr 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> A. m e. ( G " A ) E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) )
176 oveq1 
 |-  ( m = ( G ` X ) -> ( m ( ball ` ( abs o. - ) ) d ) = ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) )
177 176 sseq1d 
 |-  ( m = ( G ` X ) -> ( ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) <-> ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) ) )
178 177 rexbidv 
 |-  ( m = ( G ` X ) -> ( E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) <-> E. d e. RR+ ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) ) )
179 178 rspcva 
 |-  ( ( ( G ` X ) e. ( G " A ) /\ A. m e. ( G " A ) E. d e. RR+ ( m ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) ) -> E. d e. RR+ ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) )
180 167 175 179 syl2anc 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. d e. RR+ ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) )
181 imass2 
 |-  ( ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) -> ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ ( `' G " ( G " A ) ) )
182 f1of1 
 |-  ( G : ( RR X. RR ) -1-1-onto-> CC -> G : ( RR X. RR ) -1-1-> CC )
183 107 110 182 mp2b 
 |-  G : ( RR X. RR ) -1-1-> CC
184 f1imacnv 
 |-  ( ( G : ( RR X. RR ) -1-1-> CC /\ A C_ ( RR X. RR ) ) -> ( `' G " ( G " A ) ) = A )
185 183 15 184 sylancr 
 |-  ( A e. ( J tX J ) -> ( `' G " ( G " A ) ) = A )
186 185 sseq2d 
 |-  ( A e. ( J tX J ) -> ( ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ ( `' G " ( G " A ) ) <-> ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) )
187 181 186 syl5ib 
 |-  ( A e. ( J tX J ) -> ( ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) -> ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) )
188 187 reximdv 
 |-  ( A e. ( J tX J ) -> ( E. d e. RR+ ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) -> E. d e. RR+ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) )
189 188 adantr 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> ( E. d e. RR+ ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) C_ ( G " A ) -> E. d e. RR+ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) )
190 180 189 mpd 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. d e. RR+ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A )
191 r19.29 
 |-  ( ( A. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) /\ E. d e. RR+ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) -> E. d e. RR+ ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) /\ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) )
192 157 190 191 syl2anc 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. d e. RR+ ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) /\ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) )
193 sstr 
 |-  ( ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) /\ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) -> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A )
194 193 reximi 
 |-  ( E. d e. RR+ ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) /\ ( `' G " ( ( G ` X ) ( ball ` ( abs o. - ) ) d ) ) C_ A ) -> E. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A )
195 192 194 syl 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A )
196 r19.29 
 |-  ( ( A. d e. RR+ X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ E. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) -> E. d e. RR+ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) )
197 71 195 196 syl2anc 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. d e. RR+ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) )
198 r19.29 
 |-  ( ( A. d e. RR+ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B /\ E. d e. RR+ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) ) -> E. d e. RR+ ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B /\ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) ) )
199 52 197 198 syl2anc 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. d e. RR+ ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B /\ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) ) )
200 eleq2 
 |-  ( r = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( X e. r <-> X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) ) )
201 sseq1 
 |-  ( r = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( r C_ A <-> ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) )
202 200 201 anbi12d 
 |-  ( r = ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) -> ( ( X e. r /\ r C_ A ) <-> ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) ) )
203 202 rspcev 
 |-  ( ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B /\ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) ) -> E. r e. B ( X e. r /\ r C_ A ) )
204 203 rexlimivw 
 |-  ( E. d e. RR+ ( ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) e. B /\ ( X e. ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) /\ ( ( ( ( 1st ` X ) - ( d / 2 ) ) (,) ( ( 1st ` X ) + ( d / 2 ) ) ) X. ( ( ( 2nd ` X ) - ( d / 2 ) ) (,) ( ( 2nd ` X ) + ( d / 2 ) ) ) ) C_ A ) ) -> E. r e. B ( X e. r /\ r C_ A ) )
205 199 204 syl 
 |-  ( ( A e. ( J tX J ) /\ X e. A ) -> E. r e. B ( X e. r /\ r C_ A ) )