Metamath Proof Explorer

Theorem dvcnvre

Description: The derivative rule for inverse functions. If F is a continuous and differentiable bijective function from X to Y which never has derivative 0 , then ` ``' F is also differentiable, and its derivative is the reciprocal of the derivative of F ` . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvcnvre.f 
|- ( ph -> F e. ( X -cn-> RR ) )
dvcnvre.d 
|- ( ph -> dom ( RR _D F ) = X )
dvcnvre.z 
|- ( ph -> -. 0 e. ran ( RR _D F ) )
dvcnvre.1 
|- ( ph -> F : X -1-1-onto-> Y )
Assertion dvcnvre 
|- ( ph -> ( RR _D `' F ) = ( x e. Y |-> ( 1 / ( ( RR _D F ) ` ( `' F ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvcnvre.f 
 |-  ( ph -> F e. ( X -cn-> RR ) )
2 dvcnvre.d 
 |-  ( ph -> dom ( RR _D F ) = X )
3 dvcnvre.z 
 |-  ( ph -> -. 0 e. ran ( RR _D F ) )
4 dvcnvre.1 
 |-  ( ph -> F : X -1-1-onto-> Y )
5 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
6 5 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
7 reelprrecn 
 |-  RR e. { RR , CC }
8 7 a1i 
 |-  ( ph -> RR e. { RR , CC } )
9 retop 
 |-  ( topGen ` ran (,) ) e. Top
10 f1ofo 
 |-  ( F : X -1-1-onto-> Y -> F : X -onto-> Y )
11 forn 
 |-  ( F : X -onto-> Y -> ran F = Y )
12 4 10 11 3syl 
 |-  ( ph -> ran F = Y )
13 cncff 
 |-  ( F e. ( X -cn-> RR ) -> F : X --> RR )
14 frn 
 |-  ( F : X --> RR -> ran F C_ RR )
15 1 13 14 3syl 
 |-  ( ph -> ran F C_ RR )
16 12 15 eqsstrrd 
 |-  ( ph -> Y C_ RR )
17 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
18 17 ntrss2 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ Y C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` Y ) C_ Y )
19 9 16 18 sylancr 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` Y ) C_ Y )
20 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
21 4 20 sylan 
 |-  ( ( ph /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
22 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
23 22 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
24 dvbsss 
 |-  dom ( RR _D F ) C_ RR
25 24 a1i 
 |-  ( ph -> dom ( RR _D F ) C_ RR )
26 2 25 eqsstrrd 
 |-  ( ph -> X C_ RR )
27 17 ntrss2 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ X C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` X ) C_ X )
28 9 26 27 sylancr 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` X ) C_ X )
29 ax-resscn 
 |-  RR C_ CC
30 29 a1i 
 |-  ( ph -> RR C_ CC )
31 1 13 syl 
 |-  ( ph -> F : X --> RR )
32 fss 
 |-  ( ( F : X --> RR /\ RR C_ CC ) -> F : X --> CC )
33 31 29 32 sylancl 
 |-  ( ph -> F : X --> CC )
34 30 33 26 6 5 dvbssntr 
 |-  ( ph -> dom ( RR _D F ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` X ) )
35 2 34 eqsstrrd 
 |-  ( ph -> X C_ ( ( int ` ( topGen ` ran (,) ) ) ` X ) )
36 28 35 eqssd 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` X ) = X )
37 17 isopn3 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ X C_ RR ) -> ( X e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` X ) = X ) )
38 9 26 37 sylancr 
 |-  ( ph -> ( X e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` X ) = X ) )
39 36 38 mpbird 
 |-  ( ph -> X e. ( topGen ` ran (,) ) )
40 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
41 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
42 4 40 41 3syl 
 |-  ( ph -> `' F : Y --> X )
43 42 ffvelrnda 
 |-  ( ( ph /\ x e. Y ) -> ( `' F ` x ) e. X )
44 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
45 22 44 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
46 45 mopni2 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ X e. ( topGen ` ran (,) ) /\ ( `' F ` x ) e. X ) -> E. r e. RR+ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X )
47 23 39 43 46 mp3an2ani 
 |-  ( ( ph /\ x e. Y ) -> E. r e. RR+ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X )
48 1 ad2antrr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> F e. ( X -cn-> RR ) )
49 2 ad2antrr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> dom ( RR _D F ) = X )
50 3 ad2antrr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> -. 0 e. ran ( RR _D F ) )
51 4 ad2antrr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> F : X -1-1-onto-> Y )
52 43 adantr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( `' F ` x ) e. X )
53 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
54 53 ad2antrl 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( r / 2 ) e. RR+ )
55 26 ad2antrr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> X C_ RR )
56 55 52 sseldd 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( `' F ` x ) e. RR )
57 54 rpred 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( r / 2 ) e. RR )
58 56 57 resubcld 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( `' F ` x ) - ( r / 2 ) ) e. RR )
59 56 57 readdcld 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( `' F ` x ) + ( r / 2 ) ) e. RR )
60 elicc2 
 |-  ( ( ( ( `' F ` x ) - ( r / 2 ) ) e. RR /\ ( ( `' F ` x ) + ( r / 2 ) ) e. RR ) -> ( y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) <-> ( y e. RR /\ ( ( `' F ` x ) - ( r / 2 ) ) <_ y /\ y <_ ( ( `' F ` x ) + ( r / 2 ) ) ) ) )
61 58 59 60 syl2anc 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) <-> ( y e. RR /\ ( ( `' F ` x ) - ( r / 2 ) ) <_ y /\ y <_ ( ( `' F ` x ) + ( r / 2 ) ) ) ) )
62 61 biimpa 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( y e. RR /\ ( ( `' F ` x ) - ( r / 2 ) ) <_ y /\ y <_ ( ( `' F ` x ) + ( r / 2 ) ) ) )
63 62 simp1d 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> y e. RR )
64 56 adantr 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( `' F ` x ) e. RR )
65 simplrl 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> r e. RR+ )
66 65 rpred 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> r e. RR )
67 64 66 resubcld 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) - r ) e. RR )
68 58 adantr 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) - ( r / 2 ) ) e. RR )
69 65 53 syl 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( r / 2 ) e. RR+ )
70 69 rpred 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( r / 2 ) e. RR )
71 rphalflt 
 |-  ( r e. RR+ -> ( r / 2 ) < r )
72 65 71 syl 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( r / 2 ) < r )
73 70 66 64 72 ltsub2dd 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) - r ) < ( ( `' F ` x ) - ( r / 2 ) ) )
74 62 simp2d 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) - ( r / 2 ) ) <_ y )
75 67 68 63 73 74 ltletrd 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) - r ) < y )
76 59 adantr 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) + ( r / 2 ) ) e. RR )
77 64 66 readdcld 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) + r ) e. RR )
78 62 simp3d 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> y <_ ( ( `' F ` x ) + ( r / 2 ) ) )
79 70 66 64 72 ltadd2dd 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) + ( r / 2 ) ) < ( ( `' F ` x ) + r ) )
80 63 76 77 78 79 lelttrd 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> y < ( ( `' F ` x ) + r ) )
81 67 rexrd 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) - r ) e. RR* )
82 77 rexrd 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( ( `' F ` x ) + r ) e. RR* )
83 elioo2 
 |-  ( ( ( ( `' F ` x ) - r ) e. RR* /\ ( ( `' F ` x ) + r ) e. RR* ) -> ( y e. ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) <-> ( y e. RR /\ ( ( `' F ` x ) - r ) < y /\ y < ( ( `' F ` x ) + r ) ) ) )
84 81 82 83 syl2anc 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> ( y e. ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) <-> ( y e. RR /\ ( ( `' F ` x ) - r ) < y /\ y < ( ( `' F ` x ) + r ) ) ) )
85 63 75 80 84 mpbir3and 
 |-  ( ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) /\ y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) ) -> y e. ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) )
86 85 ex 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( y e. ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) -> y e. ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) ) )
87 86 ssrdv 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) C_ ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) )
88 rpre 
 |-  ( r e. RR+ -> r e. RR )
89 88 ad2antrl 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> r e. RR )
90 22 bl2ioo 
 |-  ( ( ( `' F ` x ) e. RR /\ r e. RR ) -> ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) )
91 56 89 90 syl2anc 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( ( `' F ` x ) - r ) (,) ( ( `' F ` x ) + r ) ) )
92 87 91 sseqtrrd 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) C_ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) )
93 simprr 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X )
94 92 93 sstrd 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( ( `' F ` x ) - ( r / 2 ) ) [,] ( ( `' F ` x ) + ( r / 2 ) ) ) C_ X )
95 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
96 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t X ) = ( ( TopOpen ` CCfld ) |`t X )
97 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t Y ) = ( ( TopOpen ` CCfld ) |`t Y )
98 48 49 50 51 52 54 94 95 5 96 97 dvcnvrelem2 
 |-  ( ( ( ph /\ x e. Y ) /\ ( r e. RR+ /\ ( ( `' F ` x ) ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ X ) ) -> ( ( F ` ( `' F ` x ) ) e. ( ( int ` ( topGen ` ran (,) ) ) ` Y ) /\ `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` ( F ` ( `' F ` x ) ) ) ) )
99 47 98 rexlimddv 
 |-  ( ( ph /\ x e. Y ) -> ( ( F ` ( `' F ` x ) ) e. ( ( int ` ( topGen ` ran (,) ) ) ` Y ) /\ `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` ( F ` ( `' F ` x ) ) ) ) )
100 99 simpld 
 |-  ( ( ph /\ x e. Y ) -> ( F ` ( `' F ` x ) ) e. ( ( int ` ( topGen ` ran (,) ) ) ` Y ) )
101 21 100 eqeltrrd 
 |-  ( ( ph /\ x e. Y ) -> x e. ( ( int ` ( topGen ` ran (,) ) ) ` Y ) )
102 19 101 eqelssd 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` Y ) = Y )
103 17 isopn3 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ Y C_ RR ) -> ( Y e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` Y ) = Y ) )
104 9 16 103 sylancr 
 |-  ( ph -> ( Y e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` Y ) = Y ) )
105 102 104 mpbird 
 |-  ( ph -> Y e. ( topGen ` ran (,) ) )
106 99 simprd 
 |-  ( ( ph /\ x e. Y ) -> `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` ( F ` ( `' F ` x ) ) ) )
107 21 fveq2d 
 |-  ( ( ph /\ x e. Y ) -> ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` ( F ` ( `' F ` x ) ) ) = ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` x ) )
108 106 107 eleqtrd 
 |-  ( ( ph /\ x e. Y ) -> `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` x ) )
109 108 ralrimiva 
 |-  ( ph -> A. x e. Y `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` x ) )
110 5 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
111 16 29 sstrdi 
 |-  ( ph -> Y C_ CC )
112 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ Y C_ CC ) -> ( ( TopOpen ` CCfld ) |`t Y ) e. ( TopOn ` Y ) )
113 110 111 112 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t Y ) e. ( TopOn ` Y ) )
114 26 29 sstrdi 
 |-  ( ph -> X C_ CC )
115 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ X C_ CC ) -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) )
116 110 114 115 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) )
117 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t Y ) e. ( TopOn ` Y ) /\ ( ( TopOpen ` CCfld ) |`t X ) e. ( TopOn ` X ) ) -> ( `' F e. ( ( ( TopOpen ` CCfld ) |`t Y ) Cn ( ( TopOpen ` CCfld ) |`t X ) ) <-> ( `' F : Y --> X /\ A. x e. Y `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` x ) ) ) )
118 113 116 117 syl2anc 
 |-  ( ph -> ( `' F e. ( ( ( TopOpen ` CCfld ) |`t Y ) Cn ( ( TopOpen ` CCfld ) |`t X ) ) <-> ( `' F : Y --> X /\ A. x e. Y `' F e. ( ( ( ( TopOpen ` CCfld ) |`t Y ) CnP ( ( TopOpen ` CCfld ) |`t X ) ) ` x ) ) ) )
119 42 109 118 mpbir2and 
 |-  ( ph -> `' F e. ( ( ( TopOpen ` CCfld ) |`t Y ) Cn ( ( TopOpen ` CCfld ) |`t X ) ) )
120 5 97 96 cncfcn 
 |-  ( ( Y C_ CC /\ X C_ CC ) -> ( Y -cn-> X ) = ( ( ( TopOpen ` CCfld ) |`t Y ) Cn ( ( TopOpen ` CCfld ) |`t X ) ) )
121 111 114 120 syl2anc 
 |-  ( ph -> ( Y -cn-> X ) = ( ( ( TopOpen ` CCfld ) |`t Y ) Cn ( ( TopOpen ` CCfld ) |`t X ) ) )
122 119 121 eleqtrrd 
 |-  ( ph -> `' F e. ( Y -cn-> X ) )
123 5 6 8 105 4 122 2 3 dvcnv 
 |-  ( ph -> ( RR _D `' F ) = ( x e. Y |-> ( 1 / ( ( RR _D F ) ` ( `' F ` x ) ) ) ) )