This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem icccncfext

Description: A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses icccncfext.1 
|- F/_ x F
icccncfext.2 
|- J = ( topGen ` ran (,) )
icccncfext.3 
|- Y = U. K
icccncfext.4 
|- G = ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) )
icccncfext.5 
|- ( ph -> A e. RR )
icccncfext.6 
|- ( ph -> B e. RR )
icccncfext.7 
|- ( ph -> A <_ B )
icccncfext.8 
|- ( ph -> K e. Top )
icccncfext.9 
|- ( ph -> F e. ( ( J |`t ( A [,] B ) ) Cn K ) )
Assertion icccncfext 
|- ( ph -> ( G e. ( J Cn ( K |`t ran F ) ) /\ ( G |` ( A [,] B ) ) = F ) )

Proof

Step Hyp Ref Expression
1 icccncfext.1 
 |-  F/_ x F
2 icccncfext.2 
 |-  J = ( topGen ` ran (,) )
3 icccncfext.3 
 |-  Y = U. K
4 icccncfext.4 
 |-  G = ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) )
5 icccncfext.5 
 |-  ( ph -> A e. RR )
6 icccncfext.6 
 |-  ( ph -> B e. RR )
7 icccncfext.7 
 |-  ( ph -> A <_ B )
8 icccncfext.8 
 |-  ( ph -> K e. Top )
9 icccncfext.9 
 |-  ( ph -> F e. ( ( J |`t ( A [,] B ) ) Cn K ) )
10 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
11 2 10 eqeltri 
 |-  J e. ( TopOn ` RR )
12 5 6 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
13 resttopon 
 |-  ( ( J e. ( TopOn ` RR ) /\ ( A [,] B ) C_ RR ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
14 11 12 13 sylancr 
 |-  ( ph -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
15 8 3 jctir 
 |-  ( ph -> ( K e. Top /\ Y = U. K ) )
16 istopon 
 |-  ( K e. ( TopOn ` Y ) <-> ( K e. Top /\ Y = U. K ) )
17 15 16 sylibr 
 |-  ( ph -> K e. ( TopOn ` Y ) )
18 cnf2 
 |-  ( ( ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J |`t ( A [,] B ) ) Cn K ) ) -> F : ( A [,] B ) --> Y )
19 14 17 9 18 syl3anc 
 |-  ( ph -> F : ( A [,] B ) --> Y )
20 19 ffnd 
 |-  ( ph -> F Fn ( A [,] B ) )
21 dffn3 
 |-  ( F Fn ( A [,] B ) <-> F : ( A [,] B ) --> ran F )
22 20 21 sylib 
 |-  ( ph -> F : ( A [,] B ) --> ran F )
23 22 ffvelcdmda 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` y ) e. ran F )
24 fnfun 
 |-  ( F Fn ( A [,] B ) -> Fun F )
25 20 24 syl 
 |-  ( ph -> Fun F )
26 5 rexrd 
 |-  ( ph -> A e. RR* )
27 6 rexrd 
 |-  ( ph -> B e. RR* )
28 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
29 26 27 7 28 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
30 20 fndmd 
 |-  ( ph -> dom F = ( A [,] B ) )
31 30 eqcomd 
 |-  ( ph -> ( A [,] B ) = dom F )
32 29 31 eleqtrd 
 |-  ( ph -> A e. dom F )
33 fvelrn 
 |-  ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
34 25 32 33 syl2anc 
 |-  ( ph -> ( F ` A ) e. ran F )
35 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
36 26 27 7 35 syl3anc 
 |-  ( ph -> B e. ( A [,] B ) )
37 36 31 eleqtrd 
 |-  ( ph -> B e. dom F )
38 fvelrn 
 |-  ( ( Fun F /\ B e. dom F ) -> ( F ` B ) e. ran F )
39 25 37 38 syl2anc 
 |-  ( ph -> ( F ` B ) e. ran F )
40 34 39 ifcld 
 |-  ( ph -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
41 40 adantr 
 |-  ( ( ph /\ -. y e. ( A [,] B ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
42 23 41 ifclda 
 |-  ( ph -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
43 42 adantr 
 |-  ( ( ph /\ y e. RR ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
44 nfv 
 |-  F/ y x e. ( A [,] B )
45 nfcv 
 |-  F/_ y ( F ` x )
46 nfcv 
 |-  F/_ y if ( x < A , ( F ` A ) , ( F ` B ) )
47 44 45 46 nfif 
 |-  F/_ y if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) )
48 nfv 
 |-  F/ x y e. ( A [,] B )
49 nfcv 
 |-  F/_ x y
50 1 49 nffv 
 |-  F/_ x ( F ` y )
51 nfv 
 |-  F/ x y < A
52 nfcv 
 |-  F/_ x A
53 1 52 nffv 
 |-  F/_ x ( F ` A )
54 nfcv 
 |-  F/_ x B
55 1 54 nffv 
 |-  F/_ x ( F ` B )
56 51 53 55 nfif 
 |-  F/_ x if ( y < A , ( F ` A ) , ( F ` B ) )
57 48 50 56 nfif 
 |-  F/_ x if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) )
58 eleq1 
 |-  ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
59 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
60 breq1 
 |-  ( x = y -> ( x < A <-> y < A ) )
61 60 ifbid 
 |-  ( x = y -> if ( x < A , ( F ` A ) , ( F ` B ) ) = if ( y < A , ( F ` A ) , ( F ` B ) ) )
62 58 59 61 ifbieq12d 
 |-  ( x = y -> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
63 47 57 62 cbvmpt 
 |-  ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) ) = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
64 4 63 eqtri 
 |-  G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
65 43 64 fmptd 
 |-  ( ph -> G : RR --> ran F )
66 65 adantr 
 |-  ( ( ph /\ y e. RR ) -> G : RR --> ran F )
67 simplll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> ph )
68 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> u e. ( K |`t ran F ) )
69 67 68 jca 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> ( ph /\ u e. ( K |`t ran F ) ) )
70 ssidd 
 |-  ( ph -> ran F C_ ran F )
71 19 frnd 
 |-  ( ph -> ran F C_ Y )
72 cnrest2 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ ran F /\ ran F C_ Y ) -> ( F e. ( ( J |`t ( A [,] B ) ) Cn K ) <-> F e. ( ( J |`t ( A [,] B ) ) Cn ( K |`t ran F ) ) ) )
73 17 70 71 72 syl3anc 
 |-  ( ph -> ( F e. ( ( J |`t ( A [,] B ) ) Cn K ) <-> F e. ( ( J |`t ( A [,] B ) ) Cn ( K |`t ran F ) ) ) )
74 9 73 mpbid 
 |-  ( ph -> F e. ( ( J |`t ( A [,] B ) ) Cn ( K |`t ran F ) ) )
75 74 anim1i 
 |-  ( ( ph /\ u e. ( K |`t ran F ) ) -> ( F e. ( ( J |`t ( A [,] B ) ) Cn ( K |`t ran F ) ) /\ u e. ( K |`t ran F ) ) )
76 cnima 
 |-  ( ( F e. ( ( J |`t ( A [,] B ) ) Cn ( K |`t ran F ) ) /\ u e. ( K |`t ran F ) ) -> ( `' F " u ) e. ( J |`t ( A [,] B ) ) )
77 69 75 76 3syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> ( `' F " u ) e. ( J |`t ( A [,] B ) ) )
78 retop 
 |-  ( topGen ` ran (,) ) e. Top
79 2 78 eqeltri 
 |-  J e. Top
80 79 a1i 
 |-  ( ph -> J e. Top )
81 reex 
 |-  RR e. _V
82 81 a1i 
 |-  ( ph -> RR e. _V )
83 82 12 ssexd 
 |-  ( ph -> ( A [,] B ) e. _V )
84 80 83 jca 
 |-  ( ph -> ( J e. Top /\ ( A [,] B ) e. _V ) )
85 67 84 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> ( J e. Top /\ ( A [,] B ) e. _V ) )
86 elrest 
 |-  ( ( J e. Top /\ ( A [,] B ) e. _V ) -> ( ( `' F " u ) e. ( J |`t ( A [,] B ) ) <-> E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
87 85 86 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> ( ( `' F " u ) e. ( J |`t ( A [,] B ) ) <-> E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
88 77 87 mpbid 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) )
89 67 3ad2ant1 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ph )
90 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> y e. RR )
91 90 3ad2ant1 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> y e. RR )
92 simp1r 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( G ` y ) e. u )
93 89 91 92 jca31 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) )
94 simpll2 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> w e. J )
95 iooretop 
 |-  ( -oo (,) A ) e. ( topGen ` ran (,) )
96 95 2 eleqtrri 
 |-  ( -oo (,) A ) e. J
97 iooretop 
 |-  ( B (,) +oo ) e. ( topGen ` ran (,) )
98 97 2 eleqtrri 
 |-  ( B (,) +oo ) e. J
99 unopn 
 |-  ( ( J e. Top /\ ( -oo (,) A ) e. J /\ ( B (,) +oo ) e. J ) -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J )
100 79 96 98 99 mp3an 
 |-  ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J
101 unopn 
 |-  ( ( J e. Top /\ w e. J /\ ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J ) -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
102 79 100 101 mp3an13 
 |-  ( w e. J -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
103 94 102 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
104 simpl1l 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( ph /\ y e. RR ) )
105 104 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ph /\ y e. RR ) )
106 simpl1r 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( G ` y ) e. u )
107 106 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G ` y ) e. u )
108 simpll3 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
109 difreicc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
110 5 6 109 syl2anc 
 |-  ( ph -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
111 110 eqcomd 
 |-  ( ph -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) = ( RR \ ( A [,] B ) ) )
112 111 eleq2d 
 |-  ( ph -> ( y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> y e. ( RR \ ( A [,] B ) ) ) )
113 112 notbid 
 |-  ( ph -> ( -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> -. y e. ( RR \ ( A [,] B ) ) ) )
114 113 biimpa 
 |-  ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. y e. ( RR \ ( A [,] B ) ) )
115 eldif 
 |-  ( y e. ( RR \ ( A [,] B ) ) <-> ( y e. RR /\ -. y e. ( A [,] B ) ) )
116 114 115 sylnib 
 |-  ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. ( y e. RR /\ -. y e. ( A [,] B ) ) )
117 imnan 
 |-  ( ( y e. RR -> -. -. y e. ( A [,] B ) ) <-> -. ( y e. RR /\ -. y e. ( A [,] B ) ) )
118 116 117 sylibr 
 |-  ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. RR -> -. -. y e. ( A [,] B ) ) )
119 118 imp 
 |-  ( ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) -> -. -. y e. ( A [,] B ) )
120 119 notnotrd 
 |-  ( ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) -> y e. ( A [,] B ) )
121 120 an32s 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( A [,] B ) )
122 121 adantlr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( A [,] B ) )
123 simplll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ph )
124 12 sselda 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y e. RR )
125 19 adantr 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> F : ( A [,] B ) --> Y )
126 125 ffvelcdmda 
 |-  ( ( ( ph /\ y e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. Y )
127 19 29 ffvelcdmd 
 |-  ( ph -> ( F ` A ) e. Y )
128 127 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) /\ y < A ) -> ( F ` A ) e. Y )
129 19 36 ffvelcdmd 
 |-  ( ph -> ( F ` B ) e. Y )
130 129 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) /\ -. y < A ) -> ( F ` B ) e. Y )
131 128 130 ifclda 
 |-  ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. Y )
132 126 131 ifclda 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
133 64 fvmpt2 
 |-  ( ( y e. RR /\ if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y ) -> ( G ` y ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
134 124 132 133 syl2anc 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
135 simpr 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
136 135 iftrued 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` y ) )
137 134 136 eqtrd 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) )
138 137 eqcomd 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` y ) = ( G ` y ) )
139 123 122 138 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( F ` y ) = ( G ` y ) )
140 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( G ` y ) e. u )
141 139 140 eqeltrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( F ` y ) e. u )
142 123 20 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> F Fn ( A [,] B ) )
143 elpreima 
 |-  ( F Fn ( A [,] B ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
144 142 143 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
145 122 141 144 mpbir2and 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( `' F " u ) )
146 145 adantlr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( `' F " u ) )
147 simplr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
148 146 147 eleqtrd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( w i^i ( A [,] B ) ) )
149 elin 
 |-  ( y e. ( w i^i ( A [,] B ) ) <-> ( y e. w /\ y e. ( A [,] B ) ) )
150 148 149 sylib 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. w /\ y e. ( A [,] B ) ) )
151 150 simpld 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. w )
152 151 ex 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) -> y e. w ) )
153 152 orrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) \/ y e. w ) )
154 153 orcomd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( y e. w \/ y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
155 elun 
 |-  ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) <-> ( y e. w \/ y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
156 154 155 sylibr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
157 105 107 108 156 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
158 imaundi 
 |-  ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) = ( ( G " w ) u. ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
159 105 simpld 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ph )
160 toponss 
 |-  ( ( J e. ( TopOn ` RR ) /\ w e. J ) -> w C_ RR )
161 11 94 160 sylancr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> w C_ RR )
162 159 161 108 jca31 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
163 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( F ` A ) e. u )
164 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( F ` B ) e. u )
165 4 funmpt2 
 |-  Fun G
166 165 a1i 
 |-  ( ph -> Fun G )
167 166 ad5antr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> Fun G )
168 fvelima 
 |-  ( ( Fun G /\ y e. ( G " w ) ) -> E. z e. w ( G ` z ) = y )
169 167 168 sylancom 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> E. z e. w ( G ` z ) = y )
170 eqcom 
 |-  ( ( G ` z ) = y <-> y = ( G ` z ) )
171 170 biimpi 
 |-  ( ( G ` z ) = y -> y = ( G ` z ) )
172 171 3ad2ant3 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> y = ( G ` z ) )
173 simp1ll 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) )
174 simp1lr 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( F ` B ) e. u )
175 simp2 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> z e. w )
176 simp-5l 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ph /\ w C_ RR ) )
177 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
178 simplr 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. w )
179 176 177 178 jca31 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) )
180 eleq1 
 |-  ( y = z -> ( y e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
181 180 anbi2d 
 |-  ( y = z -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
182 fveq2 
 |-  ( y = z -> ( G ` y ) = ( G ` z ) )
183 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
184 182 183 eqeq12d 
 |-  ( y = z -> ( ( G ` y ) = ( F ` y ) <-> ( G ` z ) = ( F ` z ) ) )
185 181 184 imbi12d 
 |-  ( y = z -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) ) ) )
186 185 137 chvarvv 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
187 186 ad4ant14 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
188 187 adantl3r 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
189 simp-4l 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ph )
190 simp-4r 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> w C_ RR )
191 simplr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. w )
192 simpr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
193 191 192 elind 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( w i^i ( A [,] B ) ) )
194 eqcom 
 |-  ( ( `' F " u ) = ( w i^i ( A [,] B ) ) <-> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
195 194 biimpi 
 |-  ( ( `' F " u ) = ( w i^i ( A [,] B ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
196 195 ad3antlr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
197 193 196 eleqtrd 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( `' F " u ) )
198 197 adantl3r 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( `' F " u ) )
199 simpr 
 |-  ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> z e. ( `' F " u ) )
200 20 ad2antrr 
 |-  ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> F Fn ( A [,] B ) )
201 elpreima 
 |-  ( F Fn ( A [,] B ) -> ( z e. ( `' F " u ) <-> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) ) )
202 200 201 syl 
 |-  ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( z e. ( `' F " u ) <-> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) ) )
203 199 202 mpbid 
 |-  ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) )
204 203 simprd 
 |-  ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( F ` z ) e. u )
205 189 190 198 204 syl21anc 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( F ` z ) e. u )
206 188 205 eqeltrd 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) e. u )
207 179 206 sylancom 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) e. u )
208 simp-5l 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ph )
209 simp-4r 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` A ) e. u )
210 208 209 jca 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ph /\ ( F ` A ) e. u ) )
211 simpllr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` B ) e. u )
212 simp-5r 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> w C_ RR )
213 simplr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. w )
214 212 213 sseldd 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. RR )
215 210 211 214 jca31 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) )
216 64 a1i 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
217 breq1 
 |-  ( y = z -> ( y < A <-> z < A ) )
218 217 ifbid 
 |-  ( y = z -> if ( y < A , ( F ` A ) , ( F ` B ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
219 180 183 218 ifbieq12d 
 |-  ( y = z -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
220 219 adantl 
 |-  ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ y = z ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
221 simplr 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> z e. RR )
222 iffalse 
 |-  ( -. z e. ( A [,] B ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
223 222 adantl 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
224 simp-5r 
 |-  ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ z < A ) -> ( F ` A ) e. u )
225 simp-4r 
 |-  ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ -. z < A ) -> ( F ` B ) e. u )
226 224 225 ifclda 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) e. u )
227 223 226 eqeltrd 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. u )
228 216 220 221 227 fvmptd 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
229 228 223 eqtrd 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
230 229 226 eqeltrd 
 |-  ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
231 215 230 sylancom 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
232 231 adantl4r 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
233 207 232 pm2.61dan 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) -> ( G ` z ) e. u )
234 173 174 175 233 syl21anc 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( G ` z ) e. u )
235 172 234 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> y e. u )
236 235 rexlimdv3a 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> ( E. z e. w ( G ` z ) = y -> y e. u ) )
237 169 236 mpd 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> y e. u )
238 237 ex 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( y e. ( G " w ) -> y e. u ) )
239 238 alrimiv 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> A. y ( y e. ( G " w ) -> y e. u ) )
240 162 163 164 239 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> A. y ( y e. ( G " w ) -> y e. u ) )
241 df-ss 
 |-  ( ( G " w ) C_ u <-> A. y ( y e. ( G " w ) -> y e. u ) )
242 240 241 sylibr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " w ) C_ u )
243 imaundi 
 |-  ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) = ( ( G " ( -oo (,) A ) ) u. ( G " ( B (,) +oo ) ) )
244 165 a1i 
 |-  ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> Fun G )
245 fvelima 
 |-  ( ( Fun G /\ t e. ( G " ( -oo (,) A ) ) ) -> E. z e. ( -oo (,) A ) ( G ` z ) = t )
246 244 245 sylancom 
 |-  ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> E. z e. ( -oo (,) A ) ( G ` z ) = t )
247 simp1l 
 |-  ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ph )
248 simp2 
 |-  ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> z e. ( -oo (,) A ) )
249 simp3 
 |-  ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
250 64 a1i 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
251 219 adantl 
 |-  ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ y = z ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
252 elioore 
 |-  ( z e. ( -oo (,) A ) -> z e. RR )
253 252 adantl 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> z e. RR )
254 elioo3g 
 |-  ( z e. ( -oo (,) A ) <-> ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
255 254 biimpi 
 |-  ( z e. ( -oo (,) A ) -> ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
256 255 simprrd 
 |-  ( z e. ( -oo (,) A ) -> z < A )
257 256 adantl 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> z < A )
258 ltnle 
 |-  ( ( z e. RR /\ A e. RR ) -> ( z < A <-> -. A <_ z ) )
259 252 5 258 syl2anr 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z < A <-> -. A <_ z ) )
260 257 259 mpbid 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> -. A <_ z )
261 260 intn3an2d 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> -. ( z e. RR /\ A <_ z /\ z <_ B ) )
262 5 6 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
263 262 adantr 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> ( A e. RR /\ B e. RR ) )
264 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
265 263 264 syl 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
266 261 265 mtbird 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> -. z e. ( A [,] B ) )
267 266 iffalsed 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
268 256 iftrued 
 |-  ( z e. ( -oo (,) A ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
269 268 adantl 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
270 267 269 eqtrd 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` A ) )
271 127 adantr 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> ( F ` A ) e. Y )
272 270 271 eqeltrd 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
273 250 251 253 272 fvmptd 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
274 273 adantr 
 |-  ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
275 simpr 
 |-  ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
276 270 adantr 
 |-  ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` A ) )
277 274 275 276 3eqtr3d 
 |-  ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> t = ( F ` A ) )
278 247 248 249 277 syl21anc 
 |-  ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> t = ( F ` A ) )
279 278 rexlimdv3a 
 |-  ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> ( E. z e. ( -oo (,) A ) ( G ` z ) = t -> t = ( F ` A ) ) )
280 246 279 mpd 
 |-  ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> t = ( F ` A ) )
281 velsn 
 |-  ( t e. { ( F ` A ) } <-> t = ( F ` A ) )
282 280 281 sylibr 
 |-  ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> t e. { ( F ` A ) } )
283 282 ex 
 |-  ( ph -> ( t e. ( G " ( -oo (,) A ) ) -> t e. { ( F ` A ) } ) )
284 283 ssrdv 
 |-  ( ph -> ( G " ( -oo (,) A ) ) C_ { ( F ` A ) } )
285 284 adantr 
 |-  ( ( ph /\ ( F ` A ) e. u ) -> ( G " ( -oo (,) A ) ) C_ { ( F ` A ) } )
286 simpr 
 |-  ( ( ph /\ ( F ` A ) e. u ) -> ( F ` A ) e. u )
287 286 snssd 
 |-  ( ( ph /\ ( F ` A ) e. u ) -> { ( F ` A ) } C_ u )
288 285 287 sstrd 
 |-  ( ( ph /\ ( F ` A ) e. u ) -> ( G " ( -oo (,) A ) ) C_ u )
289 288 adantr 
 |-  ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( -oo (,) A ) ) C_ u )
290 fvelima 
 |-  ( ( Fun G /\ t e. ( G " ( B (,) +oo ) ) ) -> E. z e. ( B (,) +oo ) ( G ` z ) = t )
291 166 290 sylan 
 |-  ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> E. z e. ( B (,) +oo ) ( G ` z ) = t )
292 simp1l 
 |-  ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> ph )
293 simp2 
 |-  ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> z e. ( B (,) +oo ) )
294 simp3 
 |-  ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
295 64 a1i 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
296 219 adantl 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ y = z ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
297 elioore 
 |-  ( z e. ( B (,) +oo ) -> z e. RR )
298 297 adantl 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> z e. RR )
299 19 ffvelcdmda 
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` z ) e. Y )
300 299 adantlr 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ z e. ( A [,] B ) ) -> ( F ` z ) e. Y )
301 5 adantr 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> A e. RR )
302 6 adantr 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> B e. RR )
303 7 adantr 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> A <_ B )
304 elioo3g 
 |-  ( z e. ( B (,) +oo ) <-> ( ( B e. RR* /\ +oo e. RR* /\ z e. RR* ) /\ ( B < z /\ z < +oo ) ) )
305 304 biimpi 
 |-  ( z e. ( B (,) +oo ) -> ( ( B e. RR* /\ +oo e. RR* /\ z e. RR* ) /\ ( B < z /\ z < +oo ) ) )
306 305 simprld 
 |-  ( z e. ( B (,) +oo ) -> B < z )
307 306 adantl 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> B < z )
308 301 302 298 303 307 lelttrd 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> A < z )
309 301 298 308 ltnsymd 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> -. z < A )
310 309 iffalsed 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` B ) )
311 129 adantr 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> ( F ` B ) e. Y )
312 310 311 eqeltrd 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) e. Y )
313 312 adantr 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ -. z e. ( A [,] B ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) e. Y )
314 300 313 ifclda 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
315 295 296 298 314 fvmptd 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
316 315 adantr 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
317 simpr 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
318 302 298 ltnled 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> ( B < z <-> -. z <_ B ) )
319 307 318 mpbid 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> -. z <_ B )
320 319 intn3an3d 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> -. ( z e. RR /\ A <_ z /\ z <_ B ) )
321 262 adantr 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> ( A e. RR /\ B e. RR ) )
322 321 264 syl 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
323 320 322 mtbird 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> -. z e. ( A [,] B ) )
324 323 iffalsed 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
325 324 310 eqtrd 
 |-  ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` B ) )
326 325 adantr 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` B ) )
327 316 317 326 3eqtr3d 
 |-  ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> t = ( F ` B ) )
328 292 293 294 327 syl21anc 
 |-  ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> t = ( F ` B ) )
329 328 rexlimdv3a 
 |-  ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> ( E. z e. ( B (,) +oo ) ( G ` z ) = t -> t = ( F ` B ) ) )
330 291 329 mpd 
 |-  ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> t = ( F ` B ) )
331 velsn 
 |-  ( t e. { ( F ` B ) } <-> t = ( F ` B ) )
332 330 331 sylibr 
 |-  ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> t e. { ( F ` B ) } )
333 332 ex 
 |-  ( ph -> ( t e. ( G " ( B (,) +oo ) ) -> t e. { ( F ` B ) } ) )
334 333 ssrdv 
 |-  ( ph -> ( G " ( B (,) +oo ) ) C_ { ( F ` B ) } )
335 334 adantr 
 |-  ( ( ph /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ { ( F ` B ) } )
336 simpr 
 |-  ( ( ph /\ ( F ` B ) e. u ) -> ( F ` B ) e. u )
337 336 snssd 
 |-  ( ( ph /\ ( F ` B ) e. u ) -> { ( F ` B ) } C_ u )
338 335 337 sstrd 
 |-  ( ( ph /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ u )
339 338 adantlr 
 |-  ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ u )
340 289 339 unssd 
 |-  ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( G " ( -oo (,) A ) ) u. ( G " ( B (,) +oo ) ) ) C_ u )
341 243 340 eqsstrid 
 |-  ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ u )
342 159 163 164 341 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ u )
343 242 342 unssd 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( G " w ) u. ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u )
344 158 343 eqsstrid 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u )
345 eleq2 
 |-  ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. v <-> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) )
346 imaeq2 
 |-  ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( G " v ) = ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) )
347 346 sseq1d 
 |-  ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( ( G " v ) C_ u <-> ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u ) )
348 345 347 anbi12d 
 |-  ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( ( y e. v /\ ( G " v ) C_ u ) <-> ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u ) ) )
349 348 rspcev 
 |-  ( ( ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J /\ ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
350 103 157 344 349 syl12anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
351 79 a1i 
 |-  ( w e. J -> J e. Top )
352 iooretop 
 |-  ( -oo (,) B ) e. ( topGen ` ran (,) )
353 352 2 eleqtrri 
 |-  ( -oo (,) B ) e. J
354 inopn 
 |-  ( ( J e. Top /\ w e. J /\ ( -oo (,) B ) e. J ) -> ( w i^i ( -oo (,) B ) ) e. J )
355 79 353 354 mp3an13 
 |-  ( w e. J -> ( w i^i ( -oo (,) B ) ) e. J )
356 96 a1i 
 |-  ( w e. J -> ( -oo (,) A ) e. J )
357 unopn 
 |-  ( ( J e. Top /\ ( w i^i ( -oo (,) B ) ) e. J /\ ( -oo (,) A ) e. J ) -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
358 351 355 356 357 syl3anc 
 |-  ( w e. J -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
359 358 3ad2ant2 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
360 359 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
361 simpll1 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) )
362 simpll3 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
363 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> -. ( F ` B ) e. u )
364 simpll 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
365 262 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> ( A e. RR /\ B e. RR ) )
366 eqimss 
 |-  ( ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) -> ( RR \ ( A [,] B ) ) C_ ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
367 109 366 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) C_ ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
368 difcom 
 |-  ( ( RR \ ( A [,] B ) ) C_ ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
369 367 368 sylib 
 |-  ( ( A e. RR /\ B e. RR ) -> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
370 365 369 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
371 370 adantr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
372 simp-4r 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. RR )
373 simpr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> -. y e. ( -oo (,) A ) )
374 elioore 
 |-  ( y e. ( B (,) +oo ) -> y e. RR )
375 374 adantl 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> y e. RR )
376 elioo3g 
 |-  ( y e. ( B (,) +oo ) <-> ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
377 376 biimpi 
 |-  ( y e. ( B (,) +oo ) -> ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
378 377 simprld 
 |-  ( y e. ( B (,) +oo ) -> B < y )
379 378 adantl 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> B < y )
380 6 adantr 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> B e. RR )
381 380 375 ltnled 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( B < y <-> -. y <_ B ) )
382 379 381 mpbid 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> -. y <_ B )
383 382 intn3an3d 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> -. ( y e. RR /\ A <_ y /\ y <_ B ) )
384 262 adantr 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( A e. RR /\ B e. RR ) )
385 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
386 384 385 syl 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
387 383 386 mtbird 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> -. y e. ( A [,] B ) )
388 387 iffalsed 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( y < A , ( F ` A ) , ( F ` B ) ) )
389 5 adantr 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> A e. RR )
390 7 adantr 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> A <_ B )
391 389 380 375 390 379 lelttrd 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> A < y )
392 389 375 391 ltnsymd 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> -. y < A )
393 392 iffalsed 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) = ( F ` B ) )
394 388 393 eqtrd 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` B ) )
395 129 adantr 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( F ` B ) e. Y )
396 394 395 eqeltrd 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
397 375 396 133 syl2anc 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( G ` y ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
398 397 394 eqtrd 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( G ` y ) = ( F ` B ) )
399 398 eqcomd 
 |-  ( ( ph /\ y e. ( B (,) +oo ) ) -> ( F ` B ) = ( G ` y ) )
400 399 adantlr 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( B (,) +oo ) ) -> ( F ` B ) = ( G ` y ) )
401 simplr 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( B (,) +oo ) ) -> ( G ` y ) e. u )
402 400 401 eqeltrd 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( B (,) +oo ) ) -> ( F ` B ) e. u )
403 402 adantllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ y e. ( B (,) +oo ) ) -> ( F ` B ) e. u )
404 403 stoic1a 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> -. y e. ( B (,) +oo ) )
405 404 adantr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> -. y e. ( B (,) +oo ) )
406 ioran 
 |-  ( -. ( y e. ( -oo (,) A ) \/ y e. ( B (,) +oo ) ) <-> ( -. y e. ( -oo (,) A ) /\ -. y e. ( B (,) +oo ) ) )
407 373 405 406 sylanbrc 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> -. ( y e. ( -oo (,) A ) \/ y e. ( B (,) +oo ) ) )
408 elun 
 |-  ( y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> ( y e. ( -oo (,) A ) \/ y e. ( B (,) +oo ) ) )
409 407 408 sylnibr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
410 372 409 eldifd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
411 371 410 sseldd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. ( A [,] B ) )
412 411 adantllr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. ( A [,] B ) )
413 simp-4l 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ph )
414 simpllr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( G ` y ) e. u )
415 simpr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
416 simpr 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
417 138 adantlr 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> ( F ` y ) = ( G ` y ) )
418 simplr 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> ( G ` y ) e. u )
419 417 418 eqeltrd 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. u )
420 20 ad2antrr 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> F Fn ( A [,] B ) )
421 420 143 syl 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
422 416 419 421 mpbir2and 
 |-  ( ( ( ph /\ ( G ` y ) e. u ) /\ y e. ( A [,] B ) ) -> y e. ( `' F " u ) )
423 413 414 415 422 syl21anc 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> y e. ( `' F " u ) )
424 simplr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
425 423 424 eleqtrd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> y e. ( w i^i ( A [,] B ) ) )
426 elinel1 
 |-  ( y e. ( w i^i ( A [,] B ) ) -> y e. w )
427 425 426 syl 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( A [,] B ) ) -> y e. w )
428 364 412 427 syl2anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. w )
429 simp-4l 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> ( ph /\ y e. RR ) )
430 simp-4r 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> ( G ` y ) e. u )
431 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> -. ( F ` B ) e. u )
432 simpl 
 |-  ( ( ph /\ y = B ) -> ph )
433 simpr 
 |-  ( ( ph /\ y = B ) -> y = B )
434 36 adantr 
 |-  ( ( ph /\ y = B ) -> B e. ( A [,] B ) )
435 433 434 eqeltrd 
 |-  ( ( ph /\ y = B ) -> y e. ( A [,] B ) )
436 432 435 137 syl2anc 
 |-  ( ( ph /\ y = B ) -> ( G ` y ) = ( F ` y ) )
437 433 fveq2d 
 |-  ( ( ph /\ y = B ) -> ( F ` y ) = ( F ` B ) )
438 436 437 eqtrd 
 |-  ( ( ph /\ y = B ) -> ( G ` y ) = ( F ` B ) )
439 438 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ y = B ) -> ( G ` y ) = ( F ` B ) )
440 simplll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ph )
441 27 adantr 
 |-  ( ( ph /\ y e. RR ) -> B e. RR* )
442 pnfxr 
 |-  +oo e. RR*
443 442 a1i 
 |-  ( ( ph /\ y e. RR ) -> +oo e. RR* )
444 rexr 
 |-  ( y e. RR -> y e. RR* )
445 444 adantl 
 |-  ( ( ph /\ y e. RR ) -> y e. RR* )
446 441 443 445 3jca 
 |-  ( ( ph /\ y e. RR ) -> ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) )
447 446 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) )
448 mnflt 
 |-  ( y e. RR -> -oo < y )
449 448 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> -oo < y )
450 mnfxr 
 |-  -oo e. RR*
451 450 a1i 
 |-  ( ( ph /\ y e. RR ) -> -oo e. RR* )
452 451 441 445 3jca 
 |-  ( ( ph /\ y e. RR ) -> ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) )
453 elioo3g 
 |-  ( y e. ( -oo (,) B ) <-> ( ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) /\ ( -oo < y /\ y < B ) ) )
454 453 notbii 
 |-  ( -. y e. ( -oo (,) B ) <-> -. ( ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) /\ ( -oo < y /\ y < B ) ) )
455 454 biimpi 
 |-  ( -. y e. ( -oo (,) B ) -> -. ( ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) /\ ( -oo < y /\ y < B ) ) )
456 455 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> -. ( ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) /\ ( -oo < y /\ y < B ) ) )
457 nan 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> -. ( ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) /\ ( -oo < y /\ y < B ) ) ) <-> ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) ) -> -. ( -oo < y /\ y < B ) ) )
458 456 457 mpbi 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ ( -oo e. RR* /\ B e. RR* /\ y e. RR* ) ) -> -. ( -oo < y /\ y < B ) )
459 452 458 mpidan 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> -. ( -oo < y /\ y < B ) )
460 nan 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> -. ( -oo < y /\ y < B ) ) <-> ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -oo < y ) -> -. y < B ) )
461 459 460 mpbi 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -oo < y ) -> -. y < B )
462 449 461 mpdan 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> -. y < B )
463 462 anim1i 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( -. y < B /\ -. y = B ) )
464 pm4.56 
 |-  ( ( -. y < B /\ -. y = B ) <-> -. ( y < B \/ y = B ) )
465 463 464 sylib 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> -. ( y < B \/ y = B ) )
466 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
467 6 adantr 
 |-  ( ( ph /\ y e. RR ) -> B e. RR )
468 466 467 jca 
 |-  ( ( ph /\ y e. RR ) -> ( y e. RR /\ B e. RR ) )
469 468 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( y e. RR /\ B e. RR ) )
470 leloe 
 |-  ( ( y e. RR /\ B e. RR ) -> ( y <_ B <-> ( y < B \/ y = B ) ) )
471 469 470 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( y <_ B <-> ( y < B \/ y = B ) ) )
472 465 471 mtbird 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> -. y <_ B )
473 6 anim1i 
 |-  ( ( ph /\ y e. RR ) -> ( B e. RR /\ y e. RR ) )
474 473 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( B e. RR /\ y e. RR ) )
475 ltnle 
 |-  ( ( B e. RR /\ y e. RR ) -> ( B < y <-> -. y <_ B ) )
476 474 475 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( B < y <-> -. y <_ B ) )
477 472 476 mpbird 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> B < y )
478 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> y e. RR )
479 478 ltpnfd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> y < +oo )
480 477 479 jca 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( B < y /\ y < +oo ) )
481 447 480 376 sylanbrc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> y e. ( B (,) +oo ) )
482 440 481 398 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) /\ -. y = B ) -> ( G ` y ) = ( F ` B ) )
483 439 482 pm2.61dan 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> ( G ` y ) = ( F ` B ) )
484 483 eqcomd 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( -oo (,) B ) ) -> ( F ` B ) = ( G ` y ) )
485 484 adantlr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( -oo (,) B ) ) -> ( F ` B ) = ( G ` y ) )
486 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( -oo (,) B ) ) -> ( G ` y ) e. u )
487 485 486 eqeltrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( -oo (,) B ) ) -> ( F ` B ) e. u )
488 487 stoic1a 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> -. -. y e. ( -oo (,) B ) )
489 488 notnotrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( -oo (,) B ) )
490 429 430 431 489 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. ( -oo (,) B ) )
491 428 490 elind 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. ( w i^i ( -oo (,) B ) ) )
492 491 ex 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) -> ( -. y e. ( -oo (,) A ) -> y e. ( w i^i ( -oo (,) B ) ) ) )
493 492 orrd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) -> ( y e. ( -oo (,) A ) \/ y e. ( w i^i ( -oo (,) B ) ) ) )
494 493 orcomd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) -> ( y e. ( w i^i ( -oo (,) B ) ) \/ y e. ( -oo (,) A ) ) )
495 elun 
 |-  ( y e. ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) <-> ( y e. ( w i^i ( -oo (,) B ) ) \/ y e. ( -oo (,) A ) ) )
496 494 495 sylibr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) -> y e. ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) )
497 361 362 363 496 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) )
498 104 simpld 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ph )
499 498 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ph )
500 simpll2 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> w e. J )
501 11 500 160 sylancr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> w C_ RR )
502 499 501 jca 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ph /\ w C_ RR ) )
503 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( F ` A ) e. u )
504 65 ffnd 
 |-  ( ph -> G Fn RR )
505 504 ad3antrrr 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> G Fn RR )
506 ssinss1 
 |-  ( w C_ RR -> ( w i^i ( -oo (,) B ) ) C_ RR )
507 506 ad3antlr 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( w i^i ( -oo (,) B ) ) C_ RR )
508 ioossre 
 |-  ( -oo (,) A ) C_ RR
509 508 a1i 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( -oo (,) A ) C_ RR )
510 unima 
 |-  ( ( G Fn RR /\ ( w i^i ( -oo (,) B ) ) C_ RR /\ ( -oo (,) A ) C_ RR ) -> ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) = ( ( G " ( w i^i ( -oo (,) B ) ) ) u. ( G " ( -oo (,) A ) ) ) )
511 505 507 509 510 syl3anc 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) = ( ( G " ( w i^i ( -oo (,) B ) ) ) u. ( G " ( -oo (,) A ) ) ) )
512 165 a1i 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ y e. ( G " ( w i^i ( -oo (,) B ) ) ) ) -> Fun G )
513 fvelima 
 |-  ( ( Fun G /\ y e. ( G " ( w i^i ( -oo (,) B ) ) ) ) -> E. z e. ( w i^i ( -oo (,) B ) ) ( G ` z ) = y )
514 512 513 sylancom 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ y e. ( G " ( w i^i ( -oo (,) B ) ) ) ) -> E. z e. ( w i^i ( -oo (,) B ) ) ( G ` z ) = y )
515 171 3ad2ant3 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) /\ ( G ` z ) = y ) -> y = ( G ` z ) )
516 simp-5l 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ z e. ( -oo (,) A ) ) -> ph )
517 simpllr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ z e. ( -oo (,) A ) ) -> ( F ` A ) e. u )
518 simpr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ z e. ( -oo (,) A ) ) -> z e. ( -oo (,) A ) )
519 273 267 269 3eqtrd 
 |-  ( ( ph /\ z e. ( -oo (,) A ) ) -> ( G ` z ) = ( F ` A ) )
520 519 3adant2 
 |-  ( ( ph /\ ( F ` A ) e. u /\ z e. ( -oo (,) A ) ) -> ( G ` z ) = ( F ` A ) )
521 simp2 
 |-  ( ( ph /\ ( F ` A ) e. u /\ z e. ( -oo (,) A ) ) -> ( F ` A ) e. u )
522 520 521 eqeltrd 
 |-  ( ( ph /\ ( F ` A ) e. u /\ z e. ( -oo (,) A ) ) -> ( G ` z ) e. u )
523 516 517 518 522 syl3anc 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ z e. ( -oo (,) A ) ) -> ( G ` z ) e. u )
524 simplll 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ -. z e. ( -oo (,) A ) ) -> ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
525 simp-5l 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ -. z e. ( -oo (,) A ) ) -> ph )
526 simplr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. ( w i^i ( -oo (,) B ) ) )
527 simpr 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ -. z e. ( -oo (,) A ) ) -> -. z e. ( -oo (,) A ) )
528 elinel1 
 |-  ( z e. ( w i^i ( -oo (,) B ) ) -> z e. w )
529 528 3ad2ant2 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. w )
530 elinel2 
 |-  ( z e. ( w i^i ( -oo (,) B ) ) -> z e. ( -oo (,) B ) )
531 elioore 
 |-  ( z e. ( -oo (,) B ) -> z e. RR )
532 530 531 syl 
 |-  ( z e. ( w i^i ( -oo (,) B ) ) -> z e. RR )
533 532 3ad2ant2 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. RR )
534 26 3ad2ant1 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> A e. RR* )
535 533 rexrd 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. RR* )
536 mnflt 
 |-  ( z e. RR -> -oo < z )
537 533 536 syl 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -oo < z )
538 450 a1i 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -oo e. RR* )
539 538 534 535 3jca 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) )
540 simp3 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -. z e. ( -oo (,) A ) )
541 540 254 sylnib 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -. ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
542 nan 
 |-  ( ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -. ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) ) <-> ( ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) /\ ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) ) -> -. ( -oo < z /\ z < A ) ) )
543 541 542 mpbi 
 |-  ( ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) /\ ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) ) -> -. ( -oo < z /\ z < A ) )
544 539 543 mpdan 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -. ( -oo < z /\ z < A ) )
545 nan 
 |-  ( ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -. ( -oo < z /\ z < A ) ) <-> ( ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) /\ -oo < z ) -> -. z < A ) )
546 544 545 mpbi 
 |-  ( ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) /\ -oo < z ) -> -. z < A )
547 537 546 mpdan 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> -. z < A )
548 534 535 547 xrnltled 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> A <_ z )
549 simp1 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> ph )
550 530 3ad2ant2 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. ( -oo (,) B ) )
551 531 adantl 
 |-  ( ( ph /\ z e. ( -oo (,) B ) ) -> z e. RR )
552 6 adantr 
 |-  ( ( ph /\ z e. ( -oo (,) B ) ) -> B e. RR )
553 elioo3g 
 |-  ( z e. ( -oo (,) B ) <-> ( ( -oo e. RR* /\ B e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < B ) ) )
554 553 biimpi 
 |-  ( z e. ( -oo (,) B ) -> ( ( -oo e. RR* /\ B e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < B ) ) )
555 554 simprrd 
 |-  ( z e. ( -oo (,) B ) -> z < B )
556 555 adantl 
 |-  ( ( ph /\ z e. ( -oo (,) B ) ) -> z < B )
557 551 552 556 ltled 
 |-  ( ( ph /\ z e. ( -oo (,) B ) ) -> z <_ B )
558 549 550 557 syl2anc 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z <_ B )
559 262 3ad2ant1 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> ( A e. RR /\ B e. RR ) )
560 559 264 syl 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
561 533 548 558 560 mpbir3and 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. ( A [,] B ) )
562 529 561 elind 
 |-  ( ( ph /\ z e. ( w i^i ( -oo (,) B ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. ( w i^i ( A [,] B ) ) )
563 525 526 527 562 syl3anc 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ -. z e. ( -oo (,) A ) ) -> z e. ( w i^i ( A [,] B ) ) )
564 elinel2 
 |-  ( z e. ( w i^i ( A [,] B ) ) -> z e. ( A [,] B ) )
565 564 anim2i 
 |-  ( ( ph /\ z e. ( w i^i ( A [,] B ) ) ) -> ( ph /\ z e. ( A [,] B ) ) )
566 565 adantlr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> ( ph /\ z e. ( A [,] B ) ) )
567 566 186 syl 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> ( G ` z ) = ( F ` z ) )
568 20 ad2antrr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> F Fn ( A [,] B ) )
569 simpr 
 |-  ( ( ( `' F " u ) = ( w i^i ( A [,] B ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> z e. ( w i^i ( A [,] B ) ) )
570 195 adantr 
 |-  ( ( ( `' F " u ) = ( w i^i ( A [,] B ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
571 569 570 eleqtrd 
 |-  ( ( ( `' F " u ) = ( w i^i ( A [,] B ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> z e. ( `' F " u ) )
572 571 adantll 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> z e. ( `' F " u ) )
573 201 simplbda 
 |-  ( ( F Fn ( A [,] B ) /\ z e. ( `' F " u ) ) -> ( F ` z ) e. u )
574 568 572 573 syl2anc 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> ( F ` z ) e. u )
575 567 574 eqeltrd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> ( G ` z ) e. u )
576 575 adantllr 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. ( w i^i ( A [,] B ) ) ) -> ( G ` z ) e. u )
577 524 563 576 syl2anc 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) /\ -. z e. ( -oo (,) A ) ) -> ( G ` z ) e. u )
578 523 577 pm2.61dan 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) ) -> ( G ` z ) e. u )
579 578 3adant3 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) /\ ( G ` z ) = y ) -> ( G ` z ) e. u )
580 515 579 eqeltrd 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ z e. ( w i^i ( -oo (,) B ) ) /\ ( G ` z ) = y ) -> y e. u )
581 580 3adant1r 
 |-  ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ y e. ( G " ( w i^i ( -oo (,) B ) ) ) ) /\ z e. ( w i^i ( -oo (,) B ) ) /\ ( G ` z ) = y ) -> y e. u )
582 581 rexlimdv3a 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ y e. ( G " ( w i^i ( -oo (,) B ) ) ) ) -> ( E. z e. ( w i^i ( -oo (,) B ) ) ( G ` z ) = y -> y e. u ) )
583 514 582 mpd 
 |-  ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ y e. ( G " ( w i^i ( -oo (,) B ) ) ) ) -> y e. u )
584 583 ex 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( y e. ( G " ( w i^i ( -oo (,) B ) ) ) -> y e. u ) )
585 584 ssrdv 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( G " ( w i^i ( -oo (,) B ) ) ) C_ u )
586 288 ad4ant14 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( G " ( -oo (,) A ) ) C_ u )
587 585 586 unssd 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( ( G " ( w i^i ( -oo (,) B ) ) ) u. ( G " ( -oo (,) A ) ) ) C_ u )
588 511 587 eqsstrd 
 |-  ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) C_ u )
589 502 362 503 588 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) C_ u )
590 eleq2 
 |-  ( v = ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) -> ( y e. v <-> y e. ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) )
591 imaeq2 
 |-  ( v = ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) -> ( G " v ) = ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) )
592 591 sseq1d 
 |-  ( v = ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) -> ( ( G " v ) C_ u <-> ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) C_ u ) )
593 590 592 anbi12d 
 |-  ( v = ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) -> ( ( y e. v /\ ( G " v ) C_ u ) <-> ( y e. ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) /\ ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) C_ u ) ) )
594 593 rspcev 
 |-  ( ( ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J /\ ( y e. ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) /\ ( G " ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) ) C_ u ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
595 360 497 589 594 syl12anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
596 350 595 pm2.61dan 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
597 simpll2 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> w e. J )
598 iooretop 
 |-  ( A (,) +oo ) e. ( topGen ` ran (,) )
599 598 2 eleqtrri 
 |-  ( A (,) +oo ) e. J
600 inopn 
 |-  ( ( J e. Top /\ w e. J /\ ( A (,) +oo ) e. J ) -> ( w i^i ( A (,) +oo ) ) e. J )
601 79 599 600 mp3an13 
 |-  ( w e. J -> ( w i^i ( A (,) +oo ) ) e. J )
602 98 a1i 
 |-  ( w e. J -> ( B (,) +oo ) e. J )
603 unopn 
 |-  ( ( J e. Top /\ ( w i^i ( A (,) +oo ) ) e. J /\ ( B (,) +oo ) e. J ) -> ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) e. J )
604 351 601 602 603 syl3anc 
 |-  ( w e. J -> ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) e. J )
605 597 604 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) e. J )
606 simplll 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) )
607 606 simpld 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ( ph /\ y e. RR ) )
608 607 simpld 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ph )
609 simp-4r 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ( G ` y ) e. u )
610 simp-5r 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. RR )
611 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> -. ( F ` A ) e. u )
612 simpll 
 |-  ( ( ( ph /\ y e. RR ) /\ y < A ) -> ph )
613 26 adantr 
 |-  ( ( ph /\ y e. RR ) -> A e. RR* )
614 451 613 445 3jca 
 |-  ( ( ph /\ y e. RR ) -> ( -oo e. RR* /\ A e. RR* /\ y e. RR* ) )
615 614 adantr 
 |-  ( ( ( ph /\ y e. RR ) /\ y < A ) -> ( -oo e. RR* /\ A e. RR* /\ y e. RR* ) )
616 448 anim1i 
 |-  ( ( y e. RR /\ y < A ) -> ( -oo < y /\ y < A ) )
617 616 adantll 
 |-  ( ( ( ph /\ y e. RR ) /\ y < A ) -> ( -oo < y /\ y < A ) )
618 elioo3g 
 |-  ( y e. ( -oo (,) A ) <-> ( ( -oo e. RR* /\ A e. RR* /\ y e. RR* ) /\ ( -oo < y /\ y < A ) ) )
619 615 617 618 sylanbrc 
 |-  ( ( ( ph /\ y e. RR ) /\ y < A ) -> y e. ( -oo (,) A ) )
620 eleq1 
 |-  ( z = y -> ( z e. ( -oo (,) A ) <-> y e. ( -oo (,) A ) ) )
621 620 anbi2d 
 |-  ( z = y -> ( ( ph /\ z e. ( -oo (,) A ) ) <-> ( ph /\ y e. ( -oo (,) A ) ) ) )
622 fveq2 
 |-  ( z = y -> ( G ` z ) = ( G ` y ) )
623 622 eqeq1d 
 |-  ( z = y -> ( ( G ` z ) = ( F ` A ) <-> ( G ` y ) = ( F ` A ) ) )
624 621 623 imbi12d 
 |-  ( z = y -> ( ( ( ph /\ z e. ( -oo (,) A ) ) -> ( G ` z ) = ( F ` A ) ) <-> ( ( ph /\ y e. ( -oo (,) A ) ) -> ( G ` y ) = ( F ` A ) ) ) )
625 624 519 chvarvv 
 |-  ( ( ph /\ y e. ( -oo (,) A ) ) -> ( G ` y ) = ( F ` A ) )
626 612 619 625 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ y < A ) -> ( G ` y ) = ( F ` A ) )
627 626 eqcomd 
 |-  ( ( ( ph /\ y e. RR ) /\ y < A ) -> ( F ` A ) = ( G ` y ) )
628 627 ad4ant14 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ y < A ) -> ( F ` A ) = ( G ` y ) )
629 simpllr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ y < A ) -> ( G ` y ) e. u )
630 628 629 eqeltrd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ y < A ) -> ( F ` A ) e. u )
631 simplr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ y < A ) -> -. ( F ` A ) e. u )
632 630 631 pm2.65da 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) -> -. y < A )
633 5 anim1i 
 |-  ( ( ph /\ y e. RR ) -> ( A e. RR /\ y e. RR ) )
634 633 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) -> ( A e. RR /\ y e. RR ) )
635 lenlt 
 |-  ( ( A e. RR /\ y e. RR ) -> ( A <_ y <-> -. y < A ) )
636 634 635 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) -> ( A <_ y <-> -. y < A ) )
637 632 636 mpbird 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) -> A <_ y )
638 606 611 637 syl2anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> A <_ y )
639 ltpnf 
 |-  ( y e. RR -> y < +oo )
640 639 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> y < +oo )
641 446 adantr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) )
642 376 notbii 
 |-  ( -. y e. ( B (,) +oo ) <-> -. ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
643 642 biimpi 
 |-  ( -. y e. ( B (,) +oo ) -> -. ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
644 643 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> -. ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
645 imnan 
 |-  ( ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) -> -. ( B < y /\ y < +oo ) ) <-> -. ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
646 644 645 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) -> -. ( B < y /\ y < +oo ) ) )
647 641 646 mpd 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> -. ( B < y /\ y < +oo ) )
648 ancom 
 |-  ( ( B < y /\ y < +oo ) <-> ( y < +oo /\ B < y ) )
649 647 648 sylnib 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> -. ( y < +oo /\ B < y ) )
650 imnan 
 |-  ( ( y < +oo -> -. B < y ) <-> -. ( y < +oo /\ B < y ) )
651 649 650 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> ( y < +oo -> -. B < y ) )
652 640 651 mpd 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> -. B < y )
653 468 adantr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> ( y e. RR /\ B e. RR ) )
654 lenlt 
 |-  ( ( y e. RR /\ B e. RR ) -> ( y <_ B <-> -. B < y ) )
655 653 654 syl 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> ( y <_ B <-> -. B < y ) )
656 652 655 mpbird 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( B (,) +oo ) ) -> y <_ B )
657 607 656 sylancom 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y <_ B )
658 262 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ( A e. RR /\ B e. RR ) )
659 658 385 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
660 610 638 657 659 mpbir3and 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( A [,] B ) )
661 608 609 660 422 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( `' F " u ) )
662 simpllr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
663 661 662 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( w i^i ( A [,] B ) ) )
664 663 426 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. w )
665 fveq2 
 |-  ( y = A -> ( G ` y ) = ( G ` A ) )
666 29 ancli 
 |-  ( ph -> ( ph /\ A e. ( A [,] B ) ) )
667 eleq1 
 |-  ( y = A -> ( y e. ( A [,] B ) <-> A e. ( A [,] B ) ) )
668 667 anbi2d 
 |-  ( y = A -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ A e. ( A [,] B ) ) ) )
669 fveq2 
 |-  ( y = A -> ( F ` y ) = ( F ` A ) )
670 665 669 eqeq12d 
 |-  ( y = A -> ( ( G ` y ) = ( F ` y ) <-> ( G ` A ) = ( F ` A ) ) )
671 668 670 imbi12d 
 |-  ( y = A -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) ) <-> ( ( ph /\ A e. ( A [,] B ) ) -> ( G ` A ) = ( F ` A ) ) ) )
672 671 137 vtoclg 
 |-  ( A e. RR -> ( ( ph /\ A e. ( A [,] B ) ) -> ( G ` A ) = ( F ` A ) ) )
673 5 666 672 sylc 
 |-  ( ph -> ( G ` A ) = ( F ` A ) )
674 665 673 sylan9eqr 
 |-  ( ( ph /\ y = A ) -> ( G ` y ) = ( F ` A ) )
675 674 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ y = A ) -> ( G ` y ) = ( F ` A ) )
676 simplll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> ph )
677 614 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> ( -oo e. RR* /\ A e. RR* /\ y e. RR* ) )
678 448 ad3antlr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> -oo < y )
679 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> y e. RR )
680 676 5 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> A e. RR )
681 445 adantr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> y e. RR* )
682 26 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> A e. RR* )
683 639 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> y < +oo )
684 simpr 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> -. y e. ( A (,) +oo ) )
685 442 a1i 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> +oo e. RR* )
686 682 685 681 3jca 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) )
687 elioo3g 
 |-  ( y e. ( A (,) +oo ) <-> ( ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( A < y /\ y < +oo ) ) )
688 687 notbii 
 |-  ( -. y e. ( A (,) +oo ) <-> -. ( ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( A < y /\ y < +oo ) ) )
689 688 biimpi 
 |-  ( -. y e. ( A (,) +oo ) -> -. ( ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( A < y /\ y < +oo ) ) )
690 nan 
 |-  ( ( -. y e. ( A (,) +oo ) -> -. ( ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( A < y /\ y < +oo ) ) ) <-> ( ( -. y e. ( A (,) +oo ) /\ ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) ) -> -. ( A < y /\ y < +oo ) ) )
691 689 690 mpbi 
 |-  ( ( -. y e. ( A (,) +oo ) /\ ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) ) -> -. ( A < y /\ y < +oo ) )
692 684 686 691 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> -. ( A < y /\ y < +oo ) )
693 ancom 
 |-  ( ( A < y /\ y < +oo ) <-> ( y < +oo /\ A < y ) )
694 692 693 sylnib 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> -. ( y < +oo /\ A < y ) )
695 nan 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> -. ( y < +oo /\ A < y ) ) <-> ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ y < +oo ) -> -. A < y ) )
696 694 695 mpbi 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ y < +oo ) -> -. A < y )
697 683 696 mpdan 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> -. A < y )
698 681 682 697 xrnltled 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> y <_ A )
699 698 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> y <_ A )
700 neqne 
 |-  ( -. y = A -> y =/= A )
701 700 necomd 
 |-  ( -. y = A -> A =/= y )
702 701 adantl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> A =/= y )
703 679 680 699 702 leneltd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> y < A )
704 678 703 jca 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> ( -oo < y /\ y < A ) )
705 677 704 618 sylanbrc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> y e. ( -oo (,) A ) )
706 676 705 625 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) /\ -. y = A ) -> ( G ` y ) = ( F ` A ) )
707 675 706 pm2.61dan 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> ( G ` y ) = ( F ` A ) )
708 707 eqcomd 
 |-  ( ( ( ph /\ y e. RR ) /\ -. y e. ( A (,) +oo ) ) -> ( F ` A ) = ( G ` y ) )
709 708 ad4ant14 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( A (,) +oo ) ) -> ( F ` A ) = ( G ` y ) )
710 simpllr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( A (,) +oo ) ) -> ( G ` y ) e. u )
711 709 710 eqeltrd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( A (,) +oo ) ) -> ( F ` A ) e. u )
712 simplr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( A (,) +oo ) ) -> -. ( F ` A ) e. u )
713 711 712 condan 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) -> y e. ( A (,) +oo ) )
714 606 611 713 syl2anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( A (,) +oo ) )
715 664 714 elind 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( w i^i ( A (,) +oo ) ) )
716 715 adantlr 
 |-  ( ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( w i^i ( A (,) +oo ) ) )
717 pm5.6 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ -. y e. ( B (,) +oo ) ) -> y e. ( w i^i ( A (,) +oo ) ) ) <-> ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( y e. ( B (,) +oo ) \/ y e. ( w i^i ( A (,) +oo ) ) ) ) )
718 716 717 mpbi 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( y e. ( B (,) +oo ) \/ y e. ( w i^i ( A (,) +oo ) ) ) )
719 718 orcomd 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( y e. ( w i^i ( A (,) +oo ) ) \/ y e. ( B (,) +oo ) ) )
720 elun 
 |-  ( y e. ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) <-> ( y e. ( w i^i ( A (,) +oo ) ) \/ y e. ( B (,) +oo ) ) )
721 719 720 sylibr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> y e. ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) )
722 721 3adantll2 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> y e. ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) )
723 simp1ll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ph )
724 723 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ph )
725 simpll3 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
726 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( F ` B ) e. u )
727 504 ad2antrr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> G Fn RR )
728 ioossre 
 |-  ( A (,) +oo ) C_ RR
729 728 olci 
 |-  ( w C_ RR \/ ( A (,) +oo ) C_ RR )
730 inss 
 |-  ( ( w C_ RR \/ ( A (,) +oo ) C_ RR ) -> ( w i^i ( A (,) +oo ) ) C_ RR )
731 729 730 ax-mp 
 |-  ( w i^i ( A (,) +oo ) ) C_ RR
732 731 a1i 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( w i^i ( A (,) +oo ) ) C_ RR )
733 ioossre 
 |-  ( B (,) +oo ) C_ RR
734 733 a1i 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( B (,) +oo ) C_ RR )
735 unima 
 |-  ( ( G Fn RR /\ ( w i^i ( A (,) +oo ) ) C_ RR /\ ( B (,) +oo ) C_ RR ) -> ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) = ( ( G " ( w i^i ( A (,) +oo ) ) ) u. ( G " ( B (,) +oo ) ) ) )
736 727 732 734 735 syl3anc 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) = ( ( G " ( w i^i ( A (,) +oo ) ) ) u. ( G " ( B (,) +oo ) ) ) )
737 simpll 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ph )
738 731 sseli 
 |-  ( y e. ( w i^i ( A (,) +oo ) ) -> y e. RR )
739 738 ad2antlr 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> y e. RR )
740 737 739 446 syl2anc 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) )
741 simpr 
 |-  ( ( y e. ( w i^i ( A (,) +oo ) ) /\ B < y ) -> B < y )
742 738 ltpnfd 
 |-  ( y e. ( w i^i ( A (,) +oo ) ) -> y < +oo )
743 742 adantr 
 |-  ( ( y e. ( w i^i ( A (,) +oo ) ) /\ B < y ) -> y < +oo )
744 741 743 jca 
 |-  ( ( y e. ( w i^i ( A (,) +oo ) ) /\ B < y ) -> ( B < y /\ y < +oo ) )
745 744 adantll 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( B < y /\ y < +oo ) )
746 740 745 376 sylanbrc 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> y e. ( B (,) +oo ) )
747 737 746 398 syl2anc 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( G ` y ) = ( F ` B ) )
748 747 adantllr 
 |-  ( ( ( ( ph /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( G ` y ) = ( F ` B ) )
749 simpllr 
 |-  ( ( ( ( ph /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( F ` B ) e. u )
750 748 749 eqeltrd 
 |-  ( ( ( ( ph /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( G ` y ) e. u )
751 750 adantl3r 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ B < y ) -> ( G ` y ) e. u )
752 simp-4l 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ph )
753 simplr 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y e. ( w i^i ( A (,) +oo ) ) )
754 simpr 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> -. B < y )
755 simpll 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ph )
756 738 adantl 
 |-  ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) -> y e. RR )
757 756 adantr 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y e. RR )
758 5 adantr 
 |-  ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) -> A e. RR )
759 elinel2 
 |-  ( y e. ( w i^i ( A (,) +oo ) ) -> y e. ( A (,) +oo ) )
760 687 biimpi 
 |-  ( y e. ( A (,) +oo ) -> ( ( A e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( A < y /\ y < +oo ) ) )
761 760 simprld 
 |-  ( y e. ( A (,) +oo ) -> A < y )
762 759 761 syl 
 |-  ( y e. ( w i^i ( A (,) +oo ) ) -> A < y )
763 762 adantl 
 |-  ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) -> A < y )
764 758 756 763 ltled 
 |-  ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) -> A <_ y )
765 764 adantr 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> A <_ y )
766 simpr 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> -. B < y )
767 755 757 468 syl2anc 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y e. RR /\ B e. RR ) )
768 767 654 syl 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y <_ B <-> -. B < y ) )
769 766 768 mpbird 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y <_ B )
770 262 ad2antrr 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( A e. RR /\ B e. RR ) )
771 770 385 syl 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
772 757 765 769 771 mpbir3and 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y e. ( A [,] B ) )
773 755 772 137 syl2anc 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( G ` y ) = ( F ` y ) )
774 752 753 754 773 syl21anc 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( G ` y ) = ( F ` y ) )
775 elinel1 
 |-  ( y e. ( w i^i ( A (,) +oo ) ) -> y e. w )
776 775 ad2antlr 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y e. w )
777 776 772 jca 
 |-  ( ( ( ph /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y e. w /\ y e. ( A [,] B ) ) )
778 777 adantllr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y e. w /\ y e. ( A [,] B ) ) )
779 778 149 sylibr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y e. ( w i^i ( A [,] B ) ) )
780 195 ad3antlr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
781 779 780 eleqtrd 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> y e. ( `' F " u ) )
782 20 ad3antrrr 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> F Fn ( A [,] B ) )
783 782 143 syl 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
784 781 783 mpbid 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) )
785 784 simprd 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( F ` y ) e. u )
786 785 adantllr 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( F ` y ) e. u )
787 774 786 eqeltrd 
 |-  ( ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) /\ -. B < y ) -> ( G ` y ) e. u )
788 751 787 pm2.61dan 
 |-  ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) /\ y e. ( w i^i ( A (,) +oo ) ) ) -> ( G ` y ) e. u )
789 788 ralrimiva 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> A. y e. ( w i^i ( A (,) +oo ) ) ( G ` y ) e. u )
790 504 fndmd 
 |-  ( ph -> dom G = RR )
791 731 790 sseqtrrid 
 |-  ( ph -> ( w i^i ( A (,) +oo ) ) C_ dom G )
792 166 791 jca 
 |-  ( ph -> ( Fun G /\ ( w i^i ( A (,) +oo ) ) C_ dom G ) )
793 792 ad2antrr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( Fun G /\ ( w i^i ( A (,) +oo ) ) C_ dom G ) )
794 funimass4 
 |-  ( ( Fun G /\ ( w i^i ( A (,) +oo ) ) C_ dom G ) -> ( ( G " ( w i^i ( A (,) +oo ) ) ) C_ u <-> A. y e. ( w i^i ( A (,) +oo ) ) ( G ` y ) e. u ) )
795 793 794 syl 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( ( G " ( w i^i ( A (,) +oo ) ) ) C_ u <-> A. y e. ( w i^i ( A (,) +oo ) ) ( G ` y ) e. u ) )
796 789 795 mpbird 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( G " ( w i^i ( A (,) +oo ) ) ) C_ u )
797 338 adantlr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ u )
798 796 797 unssd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( ( G " ( w i^i ( A (,) +oo ) ) ) u. ( G " ( B (,) +oo ) ) ) C_ u )
799 736 798 eqsstrd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` B ) e. u ) -> ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) C_ u )
800 724 725 726 799 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) C_ u )
801 eleq2 
 |-  ( v = ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) -> ( y e. v <-> y e. ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) )
802 imaeq2 
 |-  ( v = ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) -> ( G " v ) = ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) )
803 802 sseq1d 
 |-  ( v = ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) -> ( ( G " v ) C_ u <-> ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) C_ u ) )
804 801 803 anbi12d 
 |-  ( v = ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) -> ( ( y e. v /\ ( G " v ) C_ u ) <-> ( y e. ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) /\ ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) C_ u ) ) )
805 804 rspcev 
 |-  ( ( ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) e. J /\ ( y e. ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) /\ ( G " ( ( w i^i ( A (,) +oo ) ) u. ( B (,) +oo ) ) ) C_ u ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
806 605 722 800 805 syl12anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
807 simpll2 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> w e. J )
808 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
809 808 2 eleqtrri 
 |-  ( A (,) B ) e. J
810 inopn 
 |-  ( ( J e. Top /\ w e. J /\ ( A (,) B ) e. J ) -> ( w i^i ( A (,) B ) ) e. J )
811 79 809 810 mp3an13 
 |-  ( w e. J -> ( w i^i ( A (,) B ) ) e. J )
812 807 811 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( w i^i ( A (,) B ) ) e. J )
813 simp-4r 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. RR )
814 637 adantr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> A <_ y )
815 simpll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ph /\ y e. RR ) )
816 815 404 656 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> y <_ B )
817 816 adantlr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y <_ B )
818 simp-4l 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ph )
819 818 262 syl 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( A e. RR /\ B e. RR ) )
820 819 385 syl 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
821 813 814 817 820 mpbir3and 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( A [,] B ) )
822 821 adantllr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( A [,] B ) )
823 818 821 137 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( G ` y ) = ( F ` y ) )
824 823 adantllr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( G ` y ) = ( F ` y ) )
825 simp-4r 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( G ` y ) e. u )
826 824 825 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( F ` y ) e. u )
827 simp-5l 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ph )
828 827 20 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> F Fn ( A [,] B ) )
829 828 143 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
830 822 826 829 mpbir2and 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( `' F " u ) )
831 simpllr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
832 830 831 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( w i^i ( A [,] B ) ) )
833 832 426 syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. w )
834 simp-5r 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. RR )
835 827 834 822 jca31 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) )
836 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> -. ( F ` A ) e. u )
837 826 836 jca 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ( F ` y ) e. u /\ -. ( F ` A ) e. u ) )
838 nelneq 
 |-  ( ( ( F ` y ) e. u /\ -. ( F ` A ) e. u ) -> -. ( F ` y ) = ( F ` A ) )
839 669 necon3bi 
 |-  ( -. ( F ` y ) = ( F ` A ) -> y =/= A )
840 837 838 839 3syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y =/= A )
841 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> -. ( F ` B ) e. u )
842 826 841 jca 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( ( F ` y ) e. u /\ -. ( F ` B ) e. u ) )
843 nelneq 
 |-  ( ( ( F ` y ) e. u /\ -. ( F ` B ) e. u ) -> -. ( F ` y ) = ( F ` B ) )
844 fveq2 
 |-  ( y = B -> ( F ` y ) = ( F ` B ) )
845 844 necon3bi 
 |-  ( -. ( F ` y ) = ( F ` B ) -> y =/= B )
846 842 843 845 3syl 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y =/= B )
847 613 ad3antrrr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> A e. RR* )
848 441 ad3antrrr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> B e. RR* )
849 444 ad4antlr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> y e. RR* )
850 847 848 849 3jca 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> ( A e. RR* /\ B e. RR* /\ y e. RR* ) )
851 simpr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) -> y =/= A )
852 5 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> A e. RR )
853 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> y e. RR )
854 262 adantr 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( A e. RR /\ B e. RR ) )
855 854 385 syl 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
856 135 855 mpbid 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
857 856 simp2d 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> A <_ y )
858 857 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> A <_ y )
859 852 853 858 3jca 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> ( A e. RR /\ y e. RR /\ A <_ y ) )
860 859 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) -> ( A e. RR /\ y e. RR /\ A <_ y ) )
861 leltne 
 |-  ( ( A e. RR /\ y e. RR /\ A <_ y ) -> ( A < y <-> y =/= A ) )
862 860 861 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) -> ( A < y <-> y =/= A ) )
863 851 862 mpbird 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) -> A < y )
864 863 adantr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> A < y )
865 necom 
 |-  ( y =/= B <-> B =/= y )
866 865 biimpi 
 |-  ( y =/= B -> B =/= y )
867 866 adantl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= B ) -> B =/= y )
868 6 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> B e. RR )
869 856 simp3d 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y <_ B )
870 869 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> y <_ B )
871 853 868 870 3jca 
 |-  ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) -> ( y e. RR /\ B e. RR /\ y <_ B ) )
872 871 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= B ) -> ( y e. RR /\ B e. RR /\ y <_ B ) )
873 leltne 
 |-  ( ( y e. RR /\ B e. RR /\ y <_ B ) -> ( y < B <-> B =/= y ) )
874 872 873 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= B ) -> ( y < B <-> B =/= y ) )
875 867 874 mpbird 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= B ) -> y < B )
876 875 adantlr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> y < B )
877 864 876 jca 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> ( A < y /\ y < B ) )
878 elioo3g 
 |-  ( y e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ y e. RR* ) /\ ( A < y /\ y < B ) ) )
879 850 877 878 sylanbrc 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ y e. ( A [,] B ) ) /\ y =/= A ) /\ y =/= B ) -> y e. ( A (,) B ) )
880 835 840 846 879 syl21anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( A (,) B ) )
881 833 880 elind 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( w i^i ( A (,) B ) ) )
882 881 3adantll2 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> y e. ( w i^i ( A (,) B ) ) )
883 165 a1i 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ t e. ( G " ( w i^i ( A (,) B ) ) ) ) -> Fun G )
884 fvelima 
 |-  ( ( Fun G /\ t e. ( G " ( w i^i ( A (,) B ) ) ) ) -> E. y e. ( w i^i ( A (,) B ) ) ( G ` y ) = t )
885 883 884 sylancom 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ t e. ( G " ( w i^i ( A (,) B ) ) ) ) -> E. y e. ( w i^i ( A (,) B ) ) ( G ` y ) = t )
886 simp3 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> ( G ` y ) = t )
887 simp1l 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> ph )
888 inss2 
 |-  ( w i^i ( A (,) B ) ) C_ ( A (,) B )
889 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
890 888 889 sstri 
 |-  ( w i^i ( A (,) B ) ) C_ ( A [,] B )
891 890 sseli 
 |-  ( y e. ( w i^i ( A (,) B ) ) -> y e. ( A [,] B ) )
892 891 3ad2ant2 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> y e. ( A [,] B ) )
893 887 892 137 syl2anc 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> ( G ` y ) = ( F ` y ) )
894 sslin 
 |-  ( ( A (,) B ) C_ ( A [,] B ) -> ( w i^i ( A (,) B ) ) C_ ( w i^i ( A [,] B ) ) )
895 889 894 ax-mp 
 |-  ( w i^i ( A (,) B ) ) C_ ( w i^i ( A [,] B ) )
896 895 sseli 
 |-  ( y e. ( w i^i ( A (,) B ) ) -> y e. ( w i^i ( A [,] B ) ) )
897 896 adantl 
 |-  ( ( ( `' F " u ) = ( w i^i ( A [,] B ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> y e. ( w i^i ( A [,] B ) ) )
898 195 adantr 
 |-  ( ( ( `' F " u ) = ( w i^i ( A [,] B ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
899 897 898 eleqtrd 
 |-  ( ( ( `' F " u ) = ( w i^i ( A [,] B ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> y e. ( `' F " u ) )
900 899 adantll 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> y e. ( `' F " u ) )
901 20 ad2antrr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> F Fn ( A [,] B ) )
902 901 143 syl 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
903 900 902 mpbid 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) )
904 903 simprd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) ) -> ( F ` y ) e. u )
905 904 3adant3 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> ( F ` y ) e. u )
906 893 905 eqeltrd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> ( G ` y ) e. u )
907 886 906 eqeltrrd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ y e. ( w i^i ( A (,) B ) ) /\ ( G ` y ) = t ) -> t e. u )
908 907 3exp 
 |-  ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( y e. ( w i^i ( A (,) B ) ) -> ( ( G ` y ) = t -> t e. u ) ) )
909 908 adantr 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ t e. ( G " ( w i^i ( A (,) B ) ) ) ) -> ( y e. ( w i^i ( A (,) B ) ) -> ( ( G ` y ) = t -> t e. u ) ) )
910 909 rexlimdv 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ t e. ( G " ( w i^i ( A (,) B ) ) ) ) -> ( E. y e. ( w i^i ( A (,) B ) ) ( G ` y ) = t -> t e. u ) )
911 885 910 mpd 
 |-  ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ t e. ( G " ( w i^i ( A (,) B ) ) ) ) -> t e. u )
912 911 ralrimiva 
 |-  ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> A. t e. ( G " ( w i^i ( A (,) B ) ) ) t e. u )
913 dfss3 
 |-  ( ( G " ( w i^i ( A (,) B ) ) ) C_ u <-> A. t e. ( G " ( w i^i ( A (,) B ) ) ) t e. u )
914 912 913 sylibr 
 |-  ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( G " ( w i^i ( A (,) B ) ) ) C_ u )
915 914 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( G " ( w i^i ( A (,) B ) ) ) C_ u )
916 915 3adant2 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( G " ( w i^i ( A (,) B ) ) ) C_ u )
917 916 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> ( G " ( w i^i ( A (,) B ) ) ) C_ u )
918 eleq2 
 |-  ( v = ( w i^i ( A (,) B ) ) -> ( y e. v <-> y e. ( w i^i ( A (,) B ) ) ) )
919 imaeq2 
 |-  ( v = ( w i^i ( A (,) B ) ) -> ( G " v ) = ( G " ( w i^i ( A (,) B ) ) ) )
920 919 sseq1d 
 |-  ( v = ( w i^i ( A (,) B ) ) -> ( ( G " v ) C_ u <-> ( G " ( w i^i ( A (,) B ) ) ) C_ u ) )
921 918 920 anbi12d 
 |-  ( v = ( w i^i ( A (,) B ) ) -> ( ( y e. v /\ ( G " v ) C_ u ) <-> ( y e. ( w i^i ( A (,) B ) ) /\ ( G " ( w i^i ( A (,) B ) ) ) C_ u ) ) )
922 921 rspcev 
 |-  ( ( ( w i^i ( A (,) B ) ) e. J /\ ( y e. ( w i^i ( A (,) B ) ) /\ ( G " ( w i^i ( A (,) B ) ) ) C_ u ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
923 812 882 917 922 syl12anc 
 |-  ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) /\ -. ( F ` B ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
924 806 923 pm2.61dan 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` A ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
925 596 924 pm2.61dan 
 |-  ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
926 93 925 syld3an1 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
927 926 rexlimdv3a 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> ( E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) ) )
928 88 927 mpd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) /\ ( G ` y ) e. u ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
929 928 ex 
 |-  ( ( ( ph /\ y e. RR ) /\ u e. ( K |`t ran F ) ) -> ( ( G ` y ) e. u -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) ) )
930 929 ralrimiva 
 |-  ( ( ph /\ y e. RR ) -> A. u e. ( K |`t ran F ) ( ( G ` y ) e. u -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) ) )
931 11 a1i 
 |-  ( ( ph /\ y e. RR ) -> J e. ( TopOn ` RR ) )
932 resttopon 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran F C_ Y ) -> ( K |`t ran F ) e. ( TopOn ` ran F ) )
933 17 71 932 syl2anc 
 |-  ( ph -> ( K |`t ran F ) e. ( TopOn ` ran F ) )
934 933 adantr 
 |-  ( ( ph /\ y e. RR ) -> ( K |`t ran F ) e. ( TopOn ` ran F ) )
935 iscnp 
 |-  ( ( J e. ( TopOn ` RR ) /\ ( K |`t ran F ) e. ( TopOn ` ran F ) /\ y e. RR ) -> ( G e. ( ( J CnP ( K |`t ran F ) ) ` y ) <-> ( G : RR --> ran F /\ A. u e. ( K |`t ran F ) ( ( G ` y ) e. u -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) ) ) ) )
936 931 934 466 935 syl3anc 
 |-  ( ( ph /\ y e. RR ) -> ( G e. ( ( J CnP ( K |`t ran F ) ) ` y ) <-> ( G : RR --> ran F /\ A. u e. ( K |`t ran F ) ( ( G ` y ) e. u -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) ) ) ) )
937 66 930 936 mpbir2and 
 |-  ( ( ph /\ y e. RR ) -> G e. ( ( J CnP ( K |`t ran F ) ) ` y ) )
938 937 ralrimiva 
 |-  ( ph -> A. y e. RR G e. ( ( J CnP ( K |`t ran F ) ) ` y ) )
939 cncnp 
 |-  ( ( J e. ( TopOn ` RR ) /\ ( K |`t ran F ) e. ( TopOn ` ran F ) ) -> ( G e. ( J Cn ( K |`t ran F ) ) <-> ( G : RR --> ran F /\ A. y e. RR G e. ( ( J CnP ( K |`t ran F ) ) ` y ) ) ) )
940 11 933 939 sylancr 
 |-  ( ph -> ( G e. ( J Cn ( K |`t ran F ) ) <-> ( G : RR --> ran F /\ A. y e. RR G e. ( ( J CnP ( K |`t ran F ) ) ` y ) ) ) )
941 65 938 940 mpbir2and 
 |-  ( ph -> G e. ( J Cn ( K |`t ran F ) ) )
942 fnssres 
 |-  ( ( G Fn RR /\ ( A [,] B ) C_ RR ) -> ( G |` ( A [,] B ) ) Fn ( A [,] B ) )
943 504 12 942 syl2anc 
 |-  ( ph -> ( G |` ( A [,] B ) ) Fn ( A [,] B ) )
944 fvres 
 |-  ( y e. ( A [,] B ) -> ( ( G |` ( A [,] B ) ) ` y ) = ( G ` y ) )
945 944 adantl 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( ( G |` ( A [,] B ) ) ` y ) = ( G ` y ) )
946 945 137 eqtrd 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( ( G |` ( A [,] B ) ) ` y ) = ( F ` y ) )
947 943 20 946 eqfnfvd 
 |-  ( ph -> ( G |` ( A [,] B ) ) = F )
948 941 947 jca 
 |-  ( ph -> ( G e. ( J Cn ( K |`t ran F ) ) /\ ( G |` ( A [,] B ) ) = F ) )