Metamath Proof Explorer

Theorem dvcnvrelem1

Description: Lemma for dvcnvre . (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 )
dvcnvre.c 
|- ( ph -> C e. X )
dvcnvre.r 
|- ( ph -> R e. RR+ )
dvcnvre.s 
|- ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ X )
Assertion dvcnvrelem1 
|- ( ph -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )

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 dvbsss 
 |-  dom ( RR _D F ) C_ RR
9 2 8 eqsstrrdi 
 |-  ( ph -> X C_ RR )
10 9 5 sseldd 
 |-  ( ph -> C e. RR )
11 6 rpred 
 |-  ( ph -> R e. RR )
12 10 11 resubcld 
 |-  ( ph -> ( C - R ) e. RR )
13 10 11 readdcld 
 |-  ( ph -> ( C + R ) e. RR )
14 10 6 ltsubrpd 
 |-  ( ph -> ( C - R ) < C )
15 10 6 ltaddrpd 
 |-  ( ph -> C < ( C + R ) )
16 12 10 13 14 15 lttrd 
 |-  ( ph -> ( C - R ) < ( C + R ) )
17 12 13 16 ltled 
 |-  ( ph -> ( C - R ) <_ ( C + R ) )
18 rescncf 
 |-  ( ( ( C - R ) [,] ( C + R ) ) C_ X -> ( F e. ( X -cn-> RR ) -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> RR ) ) )
19 7 1 18 sylc 
 |-  ( ph -> ( F |` ( ( C - R ) [,] ( C + R ) ) ) e. ( ( ( C - R ) [,] ( C + R ) ) -cn-> RR ) )
20 12 13 17 19 evthicc2 
 |-  ( ph -> E. x e. RR E. y e. RR ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) )
21 cncff 
 |-  ( F e. ( X -cn-> RR ) -> F : X --> RR )
22 1 21 syl 
 |-  ( ph -> F : X --> RR )
23 22 5 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. RR )
24 23 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` C ) e. RR )
25 12 rexrd 
 |-  ( ph -> ( C - R ) e. RR* )
26 13 rexrd 
 |-  ( ph -> ( C + R ) e. RR* )
27 lbicc2 
 |-  ( ( ( C - R ) e. RR* /\ ( C + R ) e. RR* /\ ( C - R ) <_ ( C + R ) ) -> ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) )
28 25 26 17 27 syl3anc 
 |-  ( ph -> ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) )
29 28 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) )
30 12 10 14 ltled 
 |-  ( ph -> ( C - R ) <_ C )
31 10 13 15 ltled 
 |-  ( ph -> C <_ ( C + R ) )
32 elicc2 
 |-  ( ( ( C - R ) e. RR /\ ( C + R ) e. RR ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) <-> ( C e. RR /\ ( C - R ) <_ C /\ C <_ ( C + R ) ) ) )
33 12 13 32 syl2anc 
 |-  ( ph -> ( C e. ( ( C - R ) [,] ( C + R ) ) <-> ( C e. RR /\ ( C - R ) <_ C /\ C <_ ( C + R ) ) ) )
34 10 30 31 33 mpbir3and 
 |-  ( ph -> C e. ( ( C - R ) [,] ( C + R ) ) )
35 34 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> C e. ( ( C - R ) [,] ( C + R ) ) )
36 14 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( C - R ) < C )
37 isorel 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) /\ C e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( C - R ) < C <-> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) )
38 37 biimpd 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) /\ C e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( C - R ) < C -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) )
39 38 exp32 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C - R ) < C -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) ) ) )
40 39 com4l 
 |-  ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C - R ) < C -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) ) ) )
41 29 35 36 40 syl3c 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) )
42 29 fvresd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) = ( F ` ( C - R ) ) )
43 35 fvresd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) = ( F ` C ) )
44 42 43 breq12d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) <-> ( F ` ( C - R ) ) < ( F ` C ) ) )
45 41 44 sylibd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F ` ( C - R ) ) < ( F ` C ) ) )
46 22 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> F : X --> RR )
47 46 ffund 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> Fun F )
48 7 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( C - R ) [,] ( C + R ) ) C_ X )
49 46 fdmd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> dom F = X )
50 48 49 sseqtrrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( C - R ) [,] ( C + R ) ) C_ dom F )
51 funfvima2 
 |-  ( ( Fun F /\ ( ( C - R ) [,] ( C + R ) ) C_ dom F ) -> ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( F ` ( C - R ) ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
52 47 50 51 syl2anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( F ` ( C - R ) ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
53 29 52 mpd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C - R ) ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) )
54 df-ima 
 |-  ( F " ( ( C - R ) [,] ( C + R ) ) ) = ran ( F |` ( ( C - R ) [,] ( C + R ) ) )
55 simprr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) )
56 54 55 eqtrid 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F " ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) )
57 53 56 eleqtrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C - R ) ) e. ( x [,] y ) )
58 elicc2 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( F ` ( C - R ) ) e. ( x [,] y ) <-> ( ( F ` ( C - R ) ) e. RR /\ x <_ ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) <_ y ) ) )
59 58 ad2antrl 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` ( C - R ) ) e. ( x [,] y ) <-> ( ( F ` ( C - R ) ) e. RR /\ x <_ ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) <_ y ) ) )
60 57 59 mpbid 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` ( C - R ) ) e. RR /\ x <_ ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) <_ y ) )
61 60 simp2d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> x <_ ( F ` ( C - R ) ) )
62 simprll 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> x e. RR )
63 7 28 sseldd 
 |-  ( ph -> ( C - R ) e. X )
64 22 63 ffvelcdmd 
 |-  ( ph -> ( F ` ( C - R ) ) e. RR )
65 64 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C - R ) ) e. RR )
66 lelttr 
 |-  ( ( x e. RR /\ ( F ` ( C - R ) ) e. RR /\ ( F ` C ) e. RR ) -> ( ( x <_ ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) < ( F ` C ) ) -> x < ( F ` C ) ) )
67 62 65 24 66 syl3anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( x <_ ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) < ( F ` C ) ) -> x < ( F ` C ) ) )
68 61 67 mpand 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` ( C - R ) ) < ( F ` C ) -> x < ( F ` C ) ) )
69 45 68 syld 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> x < ( F ` C ) ) )
70 ubicc2 
 |-  ( ( ( C - R ) e. RR* /\ ( C + R ) e. RR* /\ ( C - R ) <_ ( C + R ) ) -> ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) )
71 25 26 17 70 syl3anc 
 |-  ( ph -> ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) )
72 71 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) )
73 15 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> C < ( C + R ) )
74 isorel 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( C e. ( ( C - R ) [,] ( C + R ) ) /\ ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( C < ( C + R ) <-> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) )
75 74 biimpd 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( C e. ( ( C - R ) [,] ( C + R ) ) /\ ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( C < ( C + R ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) )
76 75 exp32 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C < ( C + R ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) ) ) )
77 76 com4l 
 |-  ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C < ( C + R ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) ) ) )
78 35 72 73 77 syl3c 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) )
79 fvex 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) e. _V
80 fvex 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) e. _V
81 79 80 brcnv 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) <-> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) )
82 72 fvresd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) = ( F ` ( C + R ) ) )
83 82 43 breq12d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) <-> ( F ` ( C + R ) ) < ( F ` C ) ) )
84 81 83 bitrid 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) <-> ( F ` ( C + R ) ) < ( F ` C ) ) )
85 78 84 sylibd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F ` ( C + R ) ) < ( F ` C ) ) )
86 funfvima2 
 |-  ( ( Fun F /\ ( ( C - R ) [,] ( C + R ) ) C_ dom F ) -> ( ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( F ` ( C + R ) ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
87 47 50 86 syl2anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( F ` ( C + R ) ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
88 72 87 mpd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C + R ) ) e. ( F " ( ( C - R ) [,] ( C + R ) ) ) )
89 88 56 eleqtrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C + R ) ) e. ( x [,] y ) )
90 elicc2 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( F ` ( C + R ) ) e. ( x [,] y ) <-> ( ( F ` ( C + R ) ) e. RR /\ x <_ ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) <_ y ) ) )
91 90 ad2antrl 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` ( C + R ) ) e. ( x [,] y ) <-> ( ( F ` ( C + R ) ) e. RR /\ x <_ ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) <_ y ) ) )
92 89 91 mpbid 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` ( C + R ) ) e. RR /\ x <_ ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) <_ y ) )
93 92 simp2d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> x <_ ( F ` ( C + R ) ) )
94 7 71 sseldd 
 |-  ( ph -> ( C + R ) e. X )
95 22 94 ffvelcdmd 
 |-  ( ph -> ( F ` ( C + R ) ) e. RR )
96 95 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C + R ) ) e. RR )
97 lelttr 
 |-  ( ( x e. RR /\ ( F ` ( C + R ) ) e. RR /\ ( F ` C ) e. RR ) -> ( ( x <_ ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) < ( F ` C ) ) -> x < ( F ` C ) ) )
98 62 96 24 97 syl3anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( x <_ ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) < ( F ` C ) ) -> x < ( F ` C ) ) )
99 93 98 mpand 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` ( C + R ) ) < ( F ` C ) -> x < ( F ` C ) ) )
100 85 99 syld 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> x < ( F ` C ) ) )
101 ax-resscn 
 |-  RR C_ CC
102 101 a1i 
 |-  ( ph -> RR C_ CC )
103 fss 
 |-  ( ( F : X --> RR /\ RR C_ CC ) -> F : X --> CC )
104 22 101 103 sylancl 
 |-  ( ph -> F : X --> CC )
105 7 9 sstrd 
 |-  ( ph -> ( ( C - R ) [,] ( C + R ) ) C_ RR )
106 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
107 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
108 106 107 dvres 
 |-  ( ( ( RR C_ CC /\ F : X --> CC ) /\ ( X C_ RR /\ ( ( C - R ) [,] ( C + R ) ) C_ RR ) ) -> ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( C - R ) [,] ( C + R ) ) ) ) )
109 102 104 9 105 108 syl22anc 
 |-  ( ph -> ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( C - R ) [,] ( C + R ) ) ) ) )
110 iccntr 
 |-  ( ( ( C - R ) e. RR /\ ( C + R ) e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( C - R ) [,] ( C + R ) ) ) = ( ( C - R ) (,) ( C + R ) ) )
111 12 13 110 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( C - R ) [,] ( C + R ) ) ) = ( ( C - R ) (,) ( C + R ) ) )
112 111 reseq2d 
 |-  ( ph -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( RR _D F ) |` ( ( C - R ) (,) ( C + R ) ) ) )
113 109 112 eqtrd 
 |-  ( ph -> ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( RR _D F ) |` ( ( C - R ) (,) ( C + R ) ) ) )
114 113 dmeqd 
 |-  ( ph -> dom ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) = dom ( ( RR _D F ) |` ( ( C - R ) (,) ( C + R ) ) ) )
115 dmres 
 |-  dom ( ( RR _D F ) |` ( ( C - R ) (,) ( C + R ) ) ) = ( ( ( C - R ) (,) ( C + R ) ) i^i dom ( RR _D F ) )
116 ioossicc 
 |-  ( ( C - R ) (,) ( C + R ) ) C_ ( ( C - R ) [,] ( C + R ) )
117 116 7 sstrid 
 |-  ( ph -> ( ( C - R ) (,) ( C + R ) ) C_ X )
118 117 2 sseqtrrd 
 |-  ( ph -> ( ( C - R ) (,) ( C + R ) ) C_ dom ( RR _D F ) )
119 dfss2 
 |-  ( ( ( C - R ) (,) ( C + R ) ) C_ dom ( RR _D F ) <-> ( ( ( C - R ) (,) ( C + R ) ) i^i dom ( RR _D F ) ) = ( ( C - R ) (,) ( C + R ) ) )
120 118 119 sylib 
 |-  ( ph -> ( ( ( C - R ) (,) ( C + R ) ) i^i dom ( RR _D F ) ) = ( ( C - R ) (,) ( C + R ) ) )
121 115 120 eqtrid 
 |-  ( ph -> dom ( ( RR _D F ) |` ( ( C - R ) (,) ( C + R ) ) ) = ( ( C - R ) (,) ( C + R ) ) )
122 114 121 eqtrd 
 |-  ( ph -> dom ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( C - R ) (,) ( C + R ) ) )
123 resss 
 |-  ( ( RR _D F ) |` ( ( C - R ) (,) ( C + R ) ) ) C_ ( RR _D F )
124 113 123 eqsstrdi 
 |-  ( ph -> ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) C_ ( RR _D F ) )
125 rnss 
 |-  ( ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) C_ ( RR _D F ) -> ran ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) C_ ran ( RR _D F ) )
126 124 125 syl 
 |-  ( ph -> ran ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) C_ ran ( RR _D F ) )
127 126 3 ssneldd 
 |-  ( ph -> -. 0 e. ran ( RR _D ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) )
128 12 13 19 122 127 dvne0 
 |-  ( ph -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) \/ ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) ) )
129 128 adantr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) \/ ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) ) )
130 69 100 129 mpjaod 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> x < ( F ` C ) )
131 isorel 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( C e. ( ( C - R ) [,] ( C + R ) ) /\ ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( C < ( C + R ) <-> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) )
132 131 biimpd 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( C e. ( ( C - R ) [,] ( C + R ) ) /\ ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( C < ( C + R ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) )
133 132 exp32 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C < ( C + R ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) ) ) )
134 133 com4l 
 |-  ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C + R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C < ( C + R ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) ) ) )
135 35 72 73 134 syl3c 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) ) )
136 43 82 breq12d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C + R ) ) <-> ( F ` C ) < ( F ` ( C + R ) ) ) )
137 135 136 sylibd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F ` C ) < ( F ` ( C + R ) ) ) )
138 92 simp3d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C + R ) ) <_ y )
139 simprlr 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> y e. RR )
140 ltletr 
 |-  ( ( ( F ` C ) e. RR /\ ( F ` ( C + R ) ) e. RR /\ y e. RR ) -> ( ( ( F ` C ) < ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) <_ y ) -> ( F ` C ) < y ) )
141 24 96 139 140 syl3anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F ` C ) < ( F ` ( C + R ) ) /\ ( F ` ( C + R ) ) <_ y ) -> ( F ` C ) < y ) )
142 138 141 mpan2d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` C ) < ( F ` ( C + R ) ) -> ( F ` C ) < y ) )
143 137 142 syld 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F ` C ) < y ) )
144 isorel 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) /\ C e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( C - R ) < C <-> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) )
145 144 biimpd 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) /\ ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) /\ C e. ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( C - R ) < C -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) )
146 145 exp32 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C - R ) < C -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) ) ) )
147 146 com4l 
 |-  ( ( C - R ) e. ( ( C - R ) [,] ( C + R ) ) -> ( C e. ( ( C - R ) [,] ( C + R ) ) -> ( ( C - R ) < C -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) ) ) )
148 29 35 36 147 syl3c 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) ) )
149 fvex 
 |-  ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) e. _V
150 149 79 brcnv 
 |-  ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) <-> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) )
151 43 42 breq12d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) <-> ( F ` C ) < ( F ` ( C - R ) ) ) )
152 150 151 bitrid 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` ( C - R ) ) `' < ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) ` C ) <-> ( F ` C ) < ( F ` ( C - R ) ) ) )
153 148 152 sylibd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F ` C ) < ( F ` ( C - R ) ) ) )
154 60 simp3d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` ( C - R ) ) <_ y )
155 ltletr 
 |-  ( ( ( F ` C ) e. RR /\ ( F ` ( C - R ) ) e. RR /\ y e. RR ) -> ( ( ( F ` C ) < ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) <_ y ) -> ( F ` C ) < y ) )
156 24 65 139 155 syl3anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( ( F ` C ) < ( F ` ( C - R ) ) /\ ( F ` ( C - R ) ) <_ y ) -> ( F ` C ) < y ) )
157 154 156 mpan2d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` C ) < ( F ` ( C - R ) ) -> ( F ` C ) < y ) )
158 153 157 syld 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F |` ( ( C - R ) [,] ( C + R ) ) ) Isom < , `' < ( ( ( C - R ) [,] ( C + R ) ) , ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) ) -> ( F ` C ) < y ) )
159 143 158 129 mpjaod 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` C ) < y )
160 62 rexrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> x e. RR* )
161 139 rexrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> y e. RR* )
162 elioo2 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( ( F ` C ) e. ( x (,) y ) <-> ( ( F ` C ) e. RR /\ x < ( F ` C ) /\ ( F ` C ) < y ) ) )
163 160 161 162 syl2anc 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( F ` C ) e. ( x (,) y ) <-> ( ( F ` C ) e. RR /\ x < ( F ` C ) /\ ( F ` C ) < y ) ) )
164 24 130 159 163 mpbir3and 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` C ) e. ( x (,) y ) )
165 56 fveq2d 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) )
166 iccntr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) = ( x (,) y ) )
167 166 ad2antrl 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) = ( x (,) y ) )
168 165 167 eqtrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) = ( x (,) y ) )
169 164 168 eleqtrrd 
 |-  ( ( ph /\ ( ( x e. RR /\ y e. RR ) /\ ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) ) ) -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )
170 169 expr 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) ) )
171 170 rexlimdvva 
 |-  ( ph -> ( E. x e. RR E. y e. RR ran ( F |` ( ( C - R ) [,] ( C + R ) ) ) = ( x [,] y ) -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) ) )
172 20 171 mpd 
 |-  ( ph -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) )