Metamath Proof Explorer

Theorem dvcnvrelem2

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 19-Feb-2015) (Revised by Mario Carneiro, 8-Sep-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 )
dvcnvre.c 
|- ( ph -> C e. X )
dvcnvre.r 
|- ( ph -> R e. RR+ )
dvcnvre.s 
|- ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ X )
dvcnvre.t 
|- T = ( topGen ` ran (,) )
dvcnvre.j 
|- J = ( TopOpen ` CCfld )
dvcnvre.m 
|- M = ( J |`t X )
dvcnvre.n 
|- N = ( J |`t Y )
Assertion dvcnvrelem2 
|- ( ph -> ( ( F ` C ) e. ( ( int ` T ) ` Y ) /\ `' F e. ( ( N CnP M ) ` ( F ` C ) ) ) )

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 dvcnvre.c 
 |-  ( ph -> C e. X )
6 dvcnvre.r 
 |-  ( ph -> R e. RR+ )
7 dvcnvre.s 
 |-  ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ X )
8 dvcnvre.t 
 |-  T = ( topGen ` ran (,) )
9 dvcnvre.j 
 |-  J = ( TopOpen ` CCfld )
10 dvcnvre.m 
 |-  M = ( J |`t X )
11 dvcnvre.n 
 |-  N = ( J |`t Y )
12 retop 
 |-  ( topGen ` ran (,) ) e. Top
13 8 12 eqeltri 
 |-  T e. Top
14 f1ofo 
 |-  ( F : X -1-1-onto-> Y -> F : X -onto-> Y )
15 forn 
 |-  ( F : X -onto-> Y -> ran F = Y )
16 4 14 15 3syl 
 |-  ( ph -> ran F = Y )
17 cncff 
 |-  ( F e. ( X -cn-> RR ) -> F : X --> RR )
18 frn 
 |-  ( F : X --> RR -> ran F C_ RR )
19 1 17 18 3syl 
 |-  ( ph -> ran F C_ RR )
20 16 19 eqsstrrd 
 |-  ( ph -> Y C_ RR )
21 imassrn 
 |-  ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ ran F
22 21 16 sseqtrid 
 |-  ( ph -> ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ Y )
23 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
24 8 unieqi 
 |-  U. T = U. ( topGen ` ran (,) )
25 23 24 eqtr4i 
 |-  RR = U. T
26 25 ntrss 
 |-  ( ( T e. Top /\ Y C_ RR /\ ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ Y ) -> ( ( int ` T ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) C_ ( ( int ` T ) ` Y ) )
27 13 20 22 26 mp3an2i 
 |-  ( ph -> ( ( int ` T ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) C_ ( ( int ` T ) ` Y ) )
28 1 2 3 4 5 6 7 dvcnvrelem1 
 |-  ( ph -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
29 8 fveq2i 
 |-  ( int ` T ) = ( int ` ( topGen ` ran (,) ) )
30 29 fveq1i 
 |-  ( ( int ` T ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) )
31 28 30 eleqtrrdi 
 |-  ( ph -> ( F ` C ) e. ( ( int ` T ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
32 27 31 sseldd 
 |-  ( ph -> ( F ` C ) e. ( ( int ` T ) ` Y ) )
33 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
34 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
35 4 33 34 3syl 
 |-  ( ph -> `' F : Y --> X )
36 ffun 
 |-  ( `' F : Y --> X -> Fun `' F )
37 funcnvres 
 |-  ( Fun `' F -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( `' F |` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
38 35 36 37 3syl 
 |-  ( ph -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( `' F |` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
39 dvbsss 
 |-  dom ( RR _D F ) C_ RR
40 2 39 eqsstrrdi 
 |-  ( ph -> X C_ RR )
41 ax-resscn 
 |-  RR C_ CC
42 40 41 sstrdi 
 |-  ( ph -> X C_ CC )
43 cncfss 
 |-  ( ( ( ( C - R ) [,] ( C + R ) ) C_ X /\ X C_ CC ) -> ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> ( ( C - R ) [,] ( C + R ) ) ) C_ ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> X ) )
44 7 42 43 syl2anc 
 |-  ( ph -> ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> ( ( C - R ) [,] ( C + R ) ) ) C_ ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> X ) )
45 f1of1 
 |-  ( F : X -1-1-onto-> Y -> F : X -1-1-> Y )
46 4 45 syl 
 |-  ( ph -> F : X -1-1-> Y )
47 f1ores 
 |-  ( ( F : X -1-1-> Y /\ ( ( C - R ) [,] ( C + R ) ) C_ X ) -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) -1-1-onto-> ( F " ( ( C - R ) [,] ( C + R ) ) ) )
48 46 7 47 syl2anc 
 |-  ( ph -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) -1-1-onto-> ( F " ( ( C - R ) [,] ( C + R ) ) ) )
49 9 tgioo2 
 |-  ( topGen ` ran (,) ) = ( J |`t RR )
50 8 49 eqtri 
 |-  T = ( J |`t RR )
51 50 oveq1i 
 |-  ( T |`t ( ( C - R ) [,] ( C + R ) ) ) = ( ( J |`t RR ) |`t ( ( C - R ) [,] ( C + R ) ) )
52 9 cnfldtop 
 |-  J e. Top
53 7 40 sstrd 
 |-  ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ RR )
54 reex 
 |-  RR e. _V
55 54 a1i 
 |-  ( ph -> RR e. _V )
56 restabs 
 |-  ( ( J e. Top /\ ( ( C - R ) [,] ( C + R ) ) C_ RR /\ RR e. _V ) -> ( ( J |`t RR ) |`t ( ( C - R ) [,] ( C + R ) ) ) = ( J |`t ( ( C - R ) [,] ( C + R ) ) ) )
57 52 53 55 56 mp3an2i 
 |-  ( ph -> ( ( J |`t RR ) |`t ( ( C - R ) [,] ( C + R ) ) ) = ( J |`t ( ( C - R ) [,] ( C + R ) ) ) )
58 51 57 eqtrid 
 |-  ( ph -> ( T |`t ( ( C - R ) [,] ( C + R ) ) ) = ( J |`t ( ( C - R ) [,] ( C + R ) ) ) )
59 40 5 sseldd 
 |-  ( ph -> C e. RR )
60 6 rpred 
 |-  ( ph -> R e. RR )
61 59 60 resubcld 
 |-  ( ph -> ( C - R ) e. RR )
62 59 60 readdcld 
 |-  ( ph -> ( C + R ) e. RR )
63 eqid 
 |-  ( T |`t ( ( C - R ) [,] ( C + R ) ) ) = ( T |`t ( ( C - R ) [,] ( C + R ) ) )
64 8 63 icccmp 
 |-  ( ( ( C - R ) e. RR /\ ( C + R ) e. RR ) -> ( T |`t ( ( C - R ) [,] ( C + R ) ) ) e. Comp )
65 61 62 64 syl2anc 
 |-  ( ph -> ( T |`t ( ( C - R ) [,] ( C + R ) ) ) e. Comp )
66 58 65 eqeltrrd 
 |-  ( ph -> ( J |`t ( ( C - R ) [,] ( C + R ) ) ) e. Comp )
67 f1of 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) -1-1-onto-> ( F " ( ( C - R ) [,] ( C + R ) ) ) -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) --> ( F " ( ( C - R ) [,] ( C + R ) ) ) )
68 48 67 syl 
 |-  ( ph -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) --> ( F " ( ( C - R ) [,] ( C + R ) ) ) )
69 19 41 sstrdi 
 |-  ( ph -> ran F C_ CC )
70 21 69 sstrid 
 |-  ( ph -> ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ CC )
71 rescncf 
 |-  ( ( ( C - R ) [,] ( C + R ) ) C_ X -> ( F e. ( X -cn-> RR ) -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> RR ) ) )
72 7 1 71 sylc 
 |-  ( ph -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> RR ) )
73 cncfcdm 
 |-  ( ( ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ CC /\ ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> RR ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> ( F " ( ( C - R ) [,] ( C + R ) ) ) ) <-> ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) --> ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
74 70 72 73 syl2anc 
 |-  ( ph -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> ( F " ( ( C - R ) [,] ( C + R ) ) ) ) <-> ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) --> ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
75 68 74 mpbird 
 |-  ( ph -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
76 eqid 
 |-  ( J |`t ( ( C - R ) [,] ( C + R ) ) ) = ( J |`t ( ( C - R ) [,] ( C + R ) ) )
77 9 76 cncfcnvcn 
 |-  ( ( ( J |`t ( ( C - R ) [,] ( C + R ) ) ) e. Comp /\ ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> ( F " ( ( C - R ) [,] ( C + R ) ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) -1-1-onto-> ( F " ( ( C - R ) [,] ( C + R ) ) ) <-> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> ( ( C - R ) [,] ( C + R ) ) ) ) )
78 66 75 77 syl2anc 
 |-  ( ph -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) : ( ( C - R ) [,] ( C + R ) ) -1-1-onto-> ( F " ( ( C - R ) [,] ( C + R ) ) ) <-> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> ( ( C - R ) [,] ( C + R ) ) ) ) )
79 48 78 mpbid 
 |-  ( ph -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> ( ( C - R ) [,] ( C + R ) ) ) )
80 44 79 sseldd 
 |-  ( ph -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> X ) )
81 eqid 
 |-  ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) )
82 9 81 10 cncfcn 
 |-  ( ( ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ CC /\ X C_ CC ) -> ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> X ) = ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) Cn M ) )
83 70 42 82 syl2anc 
 |-  ( ph -> ( ( F " ( ( C - R ) [,] ( C + R ) ) ) -cn-> X ) = ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) Cn M ) )
84 80 83 eleqtrd 
 |-  ( ph -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) Cn M ) )
85 59 6 ltsubrpd 
 |-  ( ph -> ( C - R ) < C )
86 61 59 85 ltled 
 |-  ( ph -> ( C - R ) <_ C )
87 59 6 ltaddrpd 
 |-  ( ph -> C < ( C + R ) )
88 59 62 87 ltled 
 |-  ( ph -> C <_ ( C + R ) )
89 elicc2 
 |-  ( ( ( C - R ) e. RR /\ ( C + R ) e. RR ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) <-> ( C e. RR /\ ( C - R ) <_ C /\ C <_ ( C + R ) ) ) )
90 61 62 89 syl2anc 
 |-  ( ph -> ( C e. ( ( C - R ) [,] ( C + R ) ) <-> ( C e. RR /\ ( C - R ) <_ C /\ C <_ ( C + R ) ) ) )
91 59 86 88 90 mpbir3and 
 |-  ( ph -> C e. ( ( C - R ) [,] ( C + R ) ) )
92 ffun 
 |-  ( F : X --> RR -> Fun F )
93 1 17 92 3syl 
 |-  ( ph -> Fun F )
94 fdm 
 |-  ( F : X --> RR -> dom F = X )
95 1 17 94 3syl 
 |-  ( ph -> dom F = X )
96 7 95 sseqtrrd 
 |-  ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ dom F )
97 funfvima2 
 |-  ( ( Fun F /\ ( ( C - R ) [,] ( C + R ) ) C_ dom F ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( F ` C ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
98 93 96 97 syl2anc 
 |-  ( ph -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( F ` C ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
99 91 98 mpd 
 |-  ( ph -> ( F ` C ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) )
100 9 cnfldtopon 
 |-  J e. ( TopOn ` CC )
101 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ CC ) -> ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( TopOn ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
102 100 70 101 sylancr 
 |-  ( ph -> ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( TopOn ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
103 toponuni 
 |-  ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( TopOn ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F " ( ( C - R ) [,] ( C + R ) ) ) = U. ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
104 102 103 syl 
 |-  ( ph -> ( F " ( ( C - R ) [,] ( C + R ) ) ) = U. ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
105 99 104 eleqtrd 
 |-  ( ph -> ( F ` C ) e. U. ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
106 eqid 
 |-  U. ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = U. ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) )
107 106 cncnpi 
 |-  ( ( `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) Cn M ) /\ ( F ` C ) e. U. ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) ) -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) )
108 84 105 107 syl2anc 
 |-  ( ph -> `' ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) )
109 38 108 eqeltrrd 
 |-  ( ph -> ( `' F |` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) )
110 11 oveq1i 
 |-  ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( J |`t Y ) |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) )
111 ssexg 
 |-  ( ( Y C_ RR /\ RR e. _V ) -> Y e. _V )
112 20 54 111 sylancl 
 |-  ( ph -> Y e. _V )
113 restabs 
 |-  ( ( J e. Top /\ ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ Y /\ Y e. _V ) -> ( ( J |`t Y ) |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
114 52 22 112 113 mp3an2i 
 |-  ( ph -> ( ( J |`t Y ) |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
115 110 114 eqtrid 
 |-  ( ph -> ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
116 115 oveq1d 
 |-  ( ph -> ( ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) = ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) )
117 116 fveq1d 
 |-  ( ph -> ( ( ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) = ( ( ( J |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) )
118 109 117 eleqtrrd 
 |-  ( ph -> ( `' F |` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( ( ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) )
119 20 41 sstrdi 
 |-  ( ph -> Y C_ CC )
120 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ Y C_ CC ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
121 100 119 120 sylancr 
 |-  ( ph -> ( J |`t Y ) e. ( TopOn ` Y ) )
122 11 121 eqeltrid 
 |-  ( ph -> N e. ( TopOn ` Y ) )
123 topontop 
 |-  ( N e. ( TopOn ` Y ) -> N e. Top )
124 122 123 syl 
 |-  ( ph -> N e. Top )
125 toponuni 
 |-  ( N e. ( TopOn ` Y ) -> Y = U. N )
126 122 125 syl 
 |-  ( ph -> Y = U. N )
127 22 126 sseqtrd 
 |-  ( ph -> ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ U. N )
128 22 20 sstrd 
 |-  ( ph -> ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ RR )
129 difssd 
 |-  ( ph -> ( RR \ Y ) C_ RR )
130 128 129 unssd 
 |-  ( ph -> ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) C_ RR )
131 ssun1 
 |-  ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) )
132 131 a1i 
 |-  ( ph -> ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) )
133 25 ntrss 
 |-  ( ( T e. Top /\ ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) C_ RR /\ ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) -> ( ( int ` T ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) C_ ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) )
134 13 130 132 133 mp3an2i 
 |-  ( ph -> ( ( int ` T ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) C_ ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) )
135 134 31 sseldd 
 |-  ( ph -> ( F ` C ) e. ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) )
136 f1of 
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
137 4 136 syl 
 |-  ( ph -> F : X --> Y )
138 137 5 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. Y )
139 135 138 elind 
 |-  ( ph -> ( F ` C ) e. ( ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) i^i Y ) )
140 eqid 
 |-  ( T |`t Y ) = ( T |`t Y )
141 25 140 restntr 
 |-  ( ( T e. Top /\ Y C_ RR /\ ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ Y ) -> ( ( int ` ( T |`t Y ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) i^i Y ) )
142 13 20 22 141 mp3an2i 
 |-  ( ph -> ( ( int ` ( T |`t Y ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) i^i Y ) )
143 restabs 
 |-  ( ( J e. Top /\ Y C_ RR /\ RR e. _V ) -> ( ( J |`t RR ) |`t Y ) = ( J |`t Y ) )
144 52 20 55 143 mp3an2i 
 |-  ( ph -> ( ( J |`t RR ) |`t Y ) = ( J |`t Y ) )
145 50 oveq1i 
 |-  ( T |`t Y ) = ( ( J |`t RR ) |`t Y )
146 144 145 11 3eqtr4g 
 |-  ( ph -> ( T |`t Y ) = N )
147 146 fveq2d 
 |-  ( ph -> ( int ` ( T |`t Y ) ) = ( int ` N ) )
148 147 fveq1d 
 |-  ( ph -> ( ( int ` ( T |`t Y ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( int ` N ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
149 142 148 eqtr3d 
 |-  ( ph -> ( ( ( int ` T ) ` ( ( F " ( ( C - R ) [,] ( C + R ) ) ) u. ( RR \ Y ) ) ) i^i Y ) = ( ( int ` N ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
150 139 149 eleqtrd 
 |-  ( ph -> ( F ` C ) e. ( ( int ` N ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
151 126 feq2d 
 |-  ( ph -> ( `' F : Y --> X <-> `' F : U. N --> X ) )
152 35 151 mpbid 
 |-  ( ph -> `' F : U. N --> X )
153 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ X C_ CC ) -> ( J |`t X ) e. ( TopOn ` X ) )
154 100 42 153 sylancr 
 |-  ( ph -> ( J |`t X ) e. ( TopOn ` X ) )
155 10 154 eqeltrid 
 |-  ( ph -> M e. ( TopOn ` X ) )
156 toponuni 
 |-  ( M e. ( TopOn ` X ) -> X = U. M )
157 feq3 
 |-  ( X = U. M -> ( `' F : U. N --> X <-> `' F : U. N --> U. M ) )
158 155 156 157 3syl 
 |-  ( ph -> ( `' F : U. N --> X <-> `' F : U. N --> U. M ) )
159 152 158 mpbid 
 |-  ( ph -> `' F : U. N --> U. M )
160 eqid 
 |-  U. N = U. N
161 eqid 
 |-  U. M = U. M
162 160 161 cnprest 
 |-  ( ( ( N e. Top /\ ( F " ( ( C - R ) [,] ( C + R ) ) ) C_ U. N ) /\ ( ( F ` C ) e. ( ( int ` N ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) /\ `' F : U. N --> U. M ) ) -> ( `' F e. ( ( N CnP M ) ` ( F ` C ) ) <-> ( `' F |` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( ( ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) ) )
163 124 127 150 159 162 syl22anc 
 |-  ( ph -> ( `' F e. ( ( N CnP M ) ` ( F ` C ) ) <-> ( `' F |` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) e. ( ( ( N |`t ( F " ( ( C - R ) [,] ( C + R ) ) ) ) CnP M ) ` ( F ` C ) ) ) )
164 118 163 mpbird 
 |-  ( ph -> `' F e. ( ( N CnP M ) ` ( F ` C ) ) )
165 32 164 jca 
 |-  ( ph -> ( ( F ` C ) e. ( ( int ` T ) ` Y ) /\ `' F e. ( ( N CnP M ) ` ( F ` C ) ) ) )