Metamath Proof Explorer

Theorem cnheiborlem

Description: Lemma for cnheibor . (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses cnheibor.2 
|- J = ( TopOpen ` CCfld )
cnheibor.3 
|- T = ( J |`t X )
cnheibor.4 
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
cnheibor.5 
|- Y = ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) )
Assertion cnheiborlem 
|- ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> T e. Comp )

Proof

Step Hyp Ref Expression
1 cnheibor.2 
 |-  J = ( TopOpen ` CCfld )
2 cnheibor.3 
 |-  T = ( J |`t X )
3 cnheibor.4 
 |-  F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
4 cnheibor.5 
 |-  Y = ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) )
5 1 cnfldtop 
 |-  J e. Top
6 3 cnref1o 
 |-  F : ( RR X. RR ) -1-1-onto-> CC
7 f1ofn 
 |-  ( F : ( RR X. RR ) -1-1-onto-> CC -> F Fn ( RR X. RR ) )
8 elpreima 
 |-  ( F Fn ( RR X. RR ) -> ( u e. ( `' F " X ) <-> ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) )
9 6 7 8 mp2b 
 |-  ( u e. ( `' F " X ) <-> ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) )
10 1st2nd2 
 |-  ( u e. ( RR X. RR ) -> u = <. ( 1st ` u ) , ( 2nd ` u ) >. )
11 10 ad2antrl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> u = <. ( 1st ` u ) , ( 2nd ` u ) >. )
12 xp1st 
 |-  ( u e. ( RR X. RR ) -> ( 1st ` u ) e. RR )
13 12 ad2antrl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 1st ` u ) e. RR )
14 13 recnd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 1st ` u ) e. CC )
15 14 abscld 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 1st ` u ) ) e. RR )
16 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
17 16 toponunii 
 |-  CC = U. J
18 17 cldss 
 |-  ( X e. ( Clsd ` J ) -> X C_ CC )
19 18 adantr 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> X C_ CC )
20 19 adantr 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> X C_ CC )
21 simprr 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( F ` u ) e. X )
22 20 21 sseldd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( F ` u ) e. CC )
23 22 abscld 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( F ` u ) ) e. RR )
24 simplrl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> R e. RR )
25 simprl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> u e. ( RR X. RR ) )
26 f1ocnvfv1 
 |-  ( ( F : ( RR X. RR ) -1-1-onto-> CC /\ u e. ( RR X. RR ) ) -> ( `' F ` ( F ` u ) ) = u )
27 6 25 26 sylancr 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( `' F ` ( F ` u ) ) = u )
28 fveq2 
 |-  ( z = ( F ` u ) -> ( Re ` z ) = ( Re ` ( F ` u ) ) )
29 fveq2 
 |-  ( z = ( F ` u ) -> ( Im ` z ) = ( Im ` ( F ` u ) ) )
30 28 29 opeq12d 
 |-  ( z = ( F ` u ) -> <. ( Re ` z ) , ( Im ` z ) >. = <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. )
31 3 cnrecnv 
 |-  `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )
32 opex 
 |-  <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. e. _V
33 30 31 32 fvmpt 
 |-  ( ( F ` u ) e. CC -> ( `' F ` ( F ` u ) ) = <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. )
34 22 33 syl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( `' F ` ( F ` u ) ) = <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. )
35 27 34 eqtr3d 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> u = <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. )
36 35 fveq2d 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 1st ` u ) = ( 1st ` <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. ) )
37 fvex 
 |-  ( Re ` ( F ` u ) ) e. _V
38 fvex 
 |-  ( Im ` ( F ` u ) ) e. _V
39 37 38 op1st 
 |-  ( 1st ` <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. ) = ( Re ` ( F ` u ) )
40 36 39 eqtrdi 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 1st ` u ) = ( Re ` ( F ` u ) ) )
41 40 fveq2d 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 1st ` u ) ) = ( abs ` ( Re ` ( F ` u ) ) ) )
42 absrele 
 |-  ( ( F ` u ) e. CC -> ( abs ` ( Re ` ( F ` u ) ) ) <_ ( abs ` ( F ` u ) ) )
43 22 42 syl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( Re ` ( F ` u ) ) ) <_ ( abs ` ( F ` u ) ) )
44 41 43 eqbrtrd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 1st ` u ) ) <_ ( abs ` ( F ` u ) ) )
45 fveq2 
 |-  ( z = ( F ` u ) -> ( abs ` z ) = ( abs ` ( F ` u ) ) )
46 45 breq1d 
 |-  ( z = ( F ` u ) -> ( ( abs ` z ) <_ R <-> ( abs ` ( F ` u ) ) <_ R ) )
47 simplrr 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> A. z e. X ( abs ` z ) <_ R )
48 46 47 21 rspcdva 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( F ` u ) ) <_ R )
49 15 23 24 44 48 letrd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 1st ` u ) ) <_ R )
50 13 24 absled 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( ( abs ` ( 1st ` u ) ) <_ R <-> ( -u R <_ ( 1st ` u ) /\ ( 1st ` u ) <_ R ) ) )
51 49 50 mpbid 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( -u R <_ ( 1st ` u ) /\ ( 1st ` u ) <_ R ) )
52 51 simpld 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> -u R <_ ( 1st ` u ) )
53 51 simprd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 1st ` u ) <_ R )
54 renegcl 
 |-  ( R e. RR -> -u R e. RR )
55 24 54 syl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> -u R e. RR )
56 elicc2 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( ( 1st ` u ) e. ( -u R [,] R ) <-> ( ( 1st ` u ) e. RR /\ -u R <_ ( 1st ` u ) /\ ( 1st ` u ) <_ R ) ) )
57 55 24 56 syl2anc 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( ( 1st ` u ) e. ( -u R [,] R ) <-> ( ( 1st ` u ) e. RR /\ -u R <_ ( 1st ` u ) /\ ( 1st ` u ) <_ R ) ) )
58 13 52 53 57 mpbir3and 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 1st ` u ) e. ( -u R [,] R ) )
59 xp2nd 
 |-  ( u e. ( RR X. RR ) -> ( 2nd ` u ) e. RR )
60 59 ad2antrl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 2nd ` u ) e. RR )
61 60 recnd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 2nd ` u ) e. CC )
62 61 abscld 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 2nd ` u ) ) e. RR )
63 35 fveq2d 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 2nd ` u ) = ( 2nd ` <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. ) )
64 37 38 op2nd 
 |-  ( 2nd ` <. ( Re ` ( F ` u ) ) , ( Im ` ( F ` u ) ) >. ) = ( Im ` ( F ` u ) )
65 63 64 eqtrdi 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 2nd ` u ) = ( Im ` ( F ` u ) ) )
66 65 fveq2d 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 2nd ` u ) ) = ( abs ` ( Im ` ( F ` u ) ) ) )
67 absimle 
 |-  ( ( F ` u ) e. CC -> ( abs ` ( Im ` ( F ` u ) ) ) <_ ( abs ` ( F ` u ) ) )
68 22 67 syl 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( Im ` ( F ` u ) ) ) <_ ( abs ` ( F ` u ) ) )
69 66 68 eqbrtrd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 2nd ` u ) ) <_ ( abs ` ( F ` u ) ) )
70 62 23 24 69 48 letrd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( abs ` ( 2nd ` u ) ) <_ R )
71 60 24 absled 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( ( abs ` ( 2nd ` u ) ) <_ R <-> ( -u R <_ ( 2nd ` u ) /\ ( 2nd ` u ) <_ R ) ) )
72 70 71 mpbid 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( -u R <_ ( 2nd ` u ) /\ ( 2nd ` u ) <_ R ) )
73 72 simpld 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> -u R <_ ( 2nd ` u ) )
74 72 simprd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 2nd ` u ) <_ R )
75 elicc2 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( ( 2nd ` u ) e. ( -u R [,] R ) <-> ( ( 2nd ` u ) e. RR /\ -u R <_ ( 2nd ` u ) /\ ( 2nd ` u ) <_ R ) ) )
76 55 24 75 syl2anc 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( ( 2nd ` u ) e. ( -u R [,] R ) <-> ( ( 2nd ` u ) e. RR /\ -u R <_ ( 2nd ` u ) /\ ( 2nd ` u ) <_ R ) ) )
77 60 73 74 76 mpbir3and 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> ( 2nd ` u ) e. ( -u R [,] R ) )
78 58 77 opelxpd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> <. ( 1st ` u ) , ( 2nd ` u ) >. e. ( ( -u R [,] R ) X. ( -u R [,] R ) ) )
79 11 78 eqeltrd 
 |-  ( ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) /\ ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) ) -> u e. ( ( -u R [,] R ) X. ( -u R [,] R ) ) )
80 79 ex 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( ( u e. ( RR X. RR ) /\ ( F ` u ) e. X ) -> u e. ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) )
81 9 80 biimtrid 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( u e. ( `' F " X ) -> u e. ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) )
82 81 ssrdv 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( `' F " X ) C_ ( ( -u R [,] R ) X. ( -u R [,] R ) ) )
83 f1ofun 
 |-  ( F : ( RR X. RR ) -1-1-onto-> CC -> Fun F )
84 6 83 ax-mp 
 |-  Fun F
85 f1ofo 
 |-  ( F : ( RR X. RR ) -1-1-onto-> CC -> F : ( RR X. RR ) -onto-> CC )
86 forn 
 |-  ( F : ( RR X. RR ) -onto-> CC -> ran F = CC )
87 6 85 86 mp2b 
 |-  ran F = CC
88 19 87 sseqtrrdi 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> X C_ ran F )
89 funimass1 
 |-  ( ( Fun F /\ X C_ ran F ) -> ( ( `' F " X ) C_ ( ( -u R [,] R ) X. ( -u R [,] R ) ) -> X C_ ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) ) )
90 84 88 89 sylancr 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( ( `' F " X ) C_ ( ( -u R [,] R ) X. ( -u R [,] R ) ) -> X C_ ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) ) )
91 82 90 mpd 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> X C_ ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) )
92 91 4 sseqtrrdi 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> X C_ Y )
93 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
94 3 93 1 cnrehmeo 
 |-  F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J )
95 imaexg 
 |-  ( F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J ) -> ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) e. _V )
96 94 95 ax-mp 
 |-  ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) e. _V
97 4 96 eqeltri 
 |-  Y e. _V
98 97 a1i 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> Y e. _V )
99 restabs 
 |-  ( ( J e. Top /\ X C_ Y /\ Y e. _V ) -> ( ( J |`t Y ) |`t X ) = ( J |`t X ) )
100 5 92 98 99 mp3an2i 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( ( J |`t Y ) |`t X ) = ( J |`t X ) )
101 100 2 eqtr4di 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( ( J |`t Y ) |`t X ) = T )
102 4 oveq2i 
 |-  ( J |`t Y ) = ( J |`t ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) )
103 ishmeo 
 |-  ( F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Homeo J ) <-> ( F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) /\ `' F e. ( J Cn ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) ) ) )
104 94 103 mpbi 
 |-  ( F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) /\ `' F e. ( J Cn ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) ) )
105 104 simpli 
 |-  F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J )
106 iccssre 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( -u R [,] R ) C_ RR )
107 54 106 mpancom 
 |-  ( R e. RR -> ( -u R [,] R ) C_ RR )
108 1 93 rerest 
 |-  ( ( -u R [,] R ) C_ RR -> ( J |`t ( -u R [,] R ) ) = ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) )
109 107 108 syl 
 |-  ( R e. RR -> ( J |`t ( -u R [,] R ) ) = ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) )
110 109 109 oveq12d 
 |-  ( R e. RR -> ( ( J |`t ( -u R [,] R ) ) tX ( J |`t ( -u R [,] R ) ) ) = ( ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) tX ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) ) )
111 retop 
 |-  ( topGen ` ran (,) ) e. Top
112 ovex 
 |-  ( -u R [,] R ) e. _V
113 txrest 
 |-  ( ( ( ( topGen ` ran (,) ) e. Top /\ ( topGen ` ran (,) ) e. Top ) /\ ( ( -u R [,] R ) e. _V /\ ( -u R [,] R ) e. _V ) ) -> ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) |`t ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) = ( ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) tX ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) ) )
114 111 111 112 112 113 mp4an 
 |-  ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) |`t ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) = ( ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) tX ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) )
115 110 114 eqtr4di 
 |-  ( R e. RR -> ( ( J |`t ( -u R [,] R ) ) tX ( J |`t ( -u R [,] R ) ) ) = ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) |`t ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) )
116 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) = ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) )
117 93 116 icccmp 
 |-  ( ( -u R e. RR /\ R e. RR ) -> ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) e. Comp )
118 54 117 mpancom 
 |-  ( R e. RR -> ( ( topGen ` ran (,) ) |`t ( -u R [,] R ) ) e. Comp )
119 109 118 eqeltrd 
 |-  ( R e. RR -> ( J |`t ( -u R [,] R ) ) e. Comp )
120 txcmp 
 |-  ( ( ( J |`t ( -u R [,] R ) ) e. Comp /\ ( J |`t ( -u R [,] R ) ) e. Comp ) -> ( ( J |`t ( -u R [,] R ) ) tX ( J |`t ( -u R [,] R ) ) ) e. Comp )
121 119 119 120 syl2anc 
 |-  ( R e. RR -> ( ( J |`t ( -u R [,] R ) ) tX ( J |`t ( -u R [,] R ) ) ) e. Comp )
122 115 121 eqeltrrd 
 |-  ( R e. RR -> ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) |`t ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) e. Comp )
123 imacmp 
 |-  ( ( F e. ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) Cn J ) /\ ( ( ( topGen ` ran (,) ) tX ( topGen ` ran (,) ) ) |`t ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) e. Comp ) -> ( J |`t ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) ) e. Comp )
124 105 122 123 sylancr 
 |-  ( R e. RR -> ( J |`t ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) ) e. Comp )
125 102 124 eqeltrid 
 |-  ( R e. RR -> ( J |`t Y ) e. Comp )
126 125 ad2antrl 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( J |`t Y ) e. Comp )
127 imassrn 
 |-  ( F " ( ( -u R [,] R ) X. ( -u R [,] R ) ) ) C_ ran F
128 4 127 eqsstri 
 |-  Y C_ ran F
129 f1of 
 |-  ( F : ( RR X. RR ) -1-1-onto-> CC -> F : ( RR X. RR ) --> CC )
130 frn 
 |-  ( F : ( RR X. RR ) --> CC -> ran F C_ CC )
131 6 129 130 mp2b 
 |-  ran F C_ CC
132 128 131 sstri 
 |-  Y C_ CC
133 simpl 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> X e. ( Clsd ` J ) )
134 17 restcldi 
 |-  ( ( Y C_ CC /\ X e. ( Clsd ` J ) /\ X C_ Y ) -> X e. ( Clsd ` ( J |`t Y ) ) )
135 132 133 92 134 mp3an2i 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> X e. ( Clsd ` ( J |`t Y ) ) )
136 cmpcld 
 |-  ( ( ( J |`t Y ) e. Comp /\ X e. ( Clsd ` ( J |`t Y ) ) ) -> ( ( J |`t Y ) |`t X ) e. Comp )
137 126 135 136 syl2anc 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> ( ( J |`t Y ) |`t X ) e. Comp )
138 101 137 eqeltrrd 
 |-  ( ( X e. ( Clsd ` J ) /\ ( R e. RR /\ A. z e. X ( abs ` z ) <_ R ) ) -> T e. Comp )