Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  icccncfext Structured version   Unicode version

Theorem icccncfext 31549
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.)
Hypotheses
Ref Expression
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.  ( ( Jt  ( A [,] B
) )  Cn  K
) )
Assertion
Ref Expression
icccncfext  |-  ( ph  ->  ( G  e.  ( J  Cn  ( Kt  ran 
F ) )  /\  ( G  |`  ( A [,] B ) )  =  F ) )
Distinct variable groups:    x, A    x, B    ph, x
Allowed substitution hints:    F( x)    G( x)    J( x)    K( x)    Y( x)

Proof of Theorem icccncfext
Dummy variables  t  w  y  z  v  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 icccncfext.2 . . . . . . . . . . . . . . . . . 18  |-  J  =  ( topGen `  ran  (,) )
2 retopon 21138 . . . . . . . . . . . . . . . . . 18  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
31, 2eqeltri 2551 . . . . . . . . . . . . . . . . 17  |-  J  e.  (TopOn `  RR )
43a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  J  e.  (TopOn `  RR ) )
5 icccncfext.5 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR )
6 icccncfext.6 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR )
75, 6jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
8 iccssre 11618 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
97, 8syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A [,] B
)  C_  RR )
104, 9jca 532 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( J  e.  (TopOn `  RR )  /\  ( A [,] B )  C_  RR ) )
11 resttopon 19530 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  (TopOn `  RR )  /\  ( A [,] B )  C_  RR )  ->  ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) ) )
1210, 11syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) ) )
13 icccncfext.8 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  Top )
14 icccncfext.3 . . . . . . . . . . . . . . . 16  |-  Y  = 
U. K
1513, 14jctir 538 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( K  e.  Top  /\  Y  =  U. K
) )
16 istopon 19295 . . . . . . . . . . . . . . 15  |-  ( K  e.  (TopOn `  Y
)  <->  ( K  e. 
Top  /\  Y  =  U. K ) )
1715, 16sylibr 212 . . . . . . . . . . . . . 14  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
18 icccncfext.9 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ( ( Jt  ( A [,] B
) )  Cn  K
) )
1912, 17, 183jca 1176 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) )  /\  K  e.  (TopOn `  Y )  /\  F  e.  ( ( Jt  ( A [,] B ) )  Cn  K ) ) )
20 cnf2 19618 . . . . . . . . . . . . 13  |-  ( ( ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) )  /\  K  e.  (TopOn `  Y
)  /\  F  e.  ( ( Jt  ( A [,] B ) )  Cn  K ) )  ->  F : ( A [,] B ) --> Y )
2119, 20syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( A [,] B ) --> Y )
22 ffn 5737 . . . . . . . . . . . 12  |-  ( F : ( A [,] B ) --> Y  ->  F  Fn  ( A [,] B ) )
2321, 22syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F  Fn  ( A [,] B ) )
24 dffn3 5744 . . . . . . . . . . 11  |-  ( F  Fn  ( A [,] B )  <->  F :
( A [,] B
) --> ran  F )
2523, 24sylib 196 . . . . . . . . . 10  |-  ( ph  ->  F : ( A [,] B ) --> ran 
F )
2625ffvelrnda 6032 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  y )  e.  ran  F )
27 fnfun 5684 . . . . . . . . . . . . . . 15  |-  ( F  Fn  ( A [,] B )  ->  Fun  F )
2823, 27syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Fun  F )
295rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  RR* )
306rexrd 9655 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  RR* )
31 icccncfext.7 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  <_  B )
3229, 30, 313jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B ) )
33 lbicc2 11648 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
3432, 33syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  ( A [,] B ) )
35 fndm 5686 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  ( A [,] B )  ->  dom  F  =  ( A [,] B ) )
3623, 35syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  F  =  ( A [,] B ) )
3736eqcomd 2475 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A [,] B
)  =  dom  F
)
3834, 37eleqtrd 2557 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  dom  F
)
3928, 38jca 532 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Fun  F  /\  A  e.  dom  F ) )
40 fvelrn 6025 . . . . . . . . . . . . 13  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( F `  A
)  e.  ran  F
)
4139, 40syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( F `  A
)  e.  ran  F
)
42 ubicc2 11649 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  B  e.  ( A [,] B
) )
4332, 42syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  ( A [,] B ) )
4443, 37eleqtrd 2557 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  dom  F
)
4528, 44jca 532 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Fun  F  /\  B  e.  dom  F ) )
46 fvelrn 6025 . . . . . . . . . . . . 13  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( F `  B
)  e.  ran  F
)
4745, 46syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( F `  B
)  e.  ran  F
)
4841, 47jca 532 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F `  A )  e.  ran  F  /\  ( F `  B )  e.  ran  F ) )
49 ifcl 3987 . . . . . . . . . . 11  |-  ( ( ( F `  A
)  e.  ran  F  /\  ( F `  B
)  e.  ran  F
)  ->  if (
y  <  A , 
( F `  A
) ,  ( F `
 B ) )  e.  ran  F )
5048, 49syl 16 . . . . . . . . . 10  |-  ( ph  ->  if ( y  < 
A ,  ( F `
 A ) ,  ( F `  B
) )  e.  ran  F )
5150adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  -.  y  e.  ( A [,] B
) )  ->  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )  e.  ran  F
)
5226, 51ifclda 3977 . . . . . . . 8  |-  ( ph  ->  if ( y  e.  ( A [,] B
) ,  ( F `
 y ) ,  if ( y  < 
A ,  ( F `
 A ) ,  ( F `  B
) ) )  e. 
ran  F )
5352adantr 465 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  if ( y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  ran  F
)
5453ralrimiva 2881 . . . . . 6  |-  ( ph  ->  A. y  e.  RR  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )  e.  ran  F )
55 icccncfext.4 . . . . . . . 8  |-  G  =  ( x  e.  RR  |->  if ( x  e.  ( A [,] B ) ,  ( F `  x ) ,  if ( x  <  A , 
( F `  A
) ,  ( F `
 B ) ) ) )
56 nfcv 2629 . . . . . . . . . . 11  |-  F/_ y
x
57 nfcv 2629 . . . . . . . . . . 11  |-  F/_ y
( A [,] B
)
5856, 57nfel 2642 . . . . . . . . . 10  |-  F/ y  x  e.  ( A [,] B )
59 nfcv 2629 . . . . . . . . . 10  |-  F/_ y
( F `  x
)
60 nfcv 2629 . . . . . . . . . 10  |-  F/_ y if ( x  <  A ,  ( F `  A ) ,  ( F `  B ) )
6158, 59, 60nfif 3974 . . . . . . . . 9  |-  F/_ y if ( x  e.  ( A [,] B ) ,  ( F `  x ) ,  if ( x  <  A , 
( F `  A
) ,  ( F `
 B ) ) )
62 nfcv 2629 . . . . . . . . . . 11  |-  F/_ x
y
63 nfcv 2629 . . . . . . . . . . 11  |-  F/_ x
( A [,] B
)
6462, 63nfel 2642 . . . . . . . . . 10  |-  F/ x  y  e.  ( A [,] B )
65 icccncfext.1 . . . . . . . . . . 11  |-  F/_ x F
6665, 62nffv 5879 . . . . . . . . . 10  |-  F/_ x
( F `  y
)
67 nfv 1683 . . . . . . . . . . 11  |-  F/ x  y  <  A
68 nfcv 2629 . . . . . . . . . . . 12  |-  F/_ x A
6965, 68nffv 5879 . . . . . . . . . . 11  |-  F/_ x
( F `  A
)
70 nfcv 2629 . . . . . . . . . . . 12  |-  F/_ x B
7165, 70nffv 5879 . . . . . . . . . . 11  |-  F/_ x
( F `  B
)
7267, 69, 71nfif 3974 . . . . . . . . . 10  |-  F/_ x if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )
7364, 66, 72nfif 3974 . . . . . . . . 9  |-  F/_ x if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )
74 eleq1 2539 . . . . . . . . . 10  |-  ( x  =  y  ->  (
x  e.  ( A [,] B )  <->  y  e.  ( A [,] B ) ) )
75 fveq2 5872 . . . . . . . . . 10  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
76 breq1 4456 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  <  A  <->  y  <  A ) )
7776ifbid 3967 . . . . . . . . . 10  |-  ( x  =  y  ->  if ( x  <  A , 
( F `  A
) ,  ( F `
 B ) )  =  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )
7874, 75, 77ifbieq12d 3972 . . . . . . . . 9  |-  ( 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 ) ) ) )
7961, 73, 78cbvmpt 4543 . . . . . . . 8  |-  ( 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 ) ) ) )
8055, 79eqtri 2496 . . . . . . 7  |-  G  =  ( y  e.  RR  |->  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
8180fmpt 6053 . . . . . 6  |-  ( A. y  e.  RR  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )  e.  ran  F  <-> 
G : RR --> ran  F
)
8254, 81sylib 196 . . . . 5  |-  ( ph  ->  G : RR --> ran  F
)
8382adantr 465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  G : RR
--> ran  F )
84 simplll 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  ->  ph )
85 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  ->  u  e.  ( Kt  ran  F ) )
8684, 85jca 532 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( ph  /\  u  e.  ( Kt  ran  F ) ) )
87 ssid 3528 . . . . . . . . . . . . . . . . . . 19  |-  ran  F  C_ 
ran  F
8887a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ran  F  C_  ran  F )
89 frn 5743 . . . . . . . . . . . . . . . . . . 19  |-  ( F : ( A [,] B ) --> Y  ->  ran  F  C_  Y )
9021, 89syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ran  F  C_  Y
)
9117, 88, 903jca 1176 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  ran  F  /\  ran  F  C_  Y )
)
92 cnrest2 19655 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  (TopOn `  Y )  /\  ran  F 
C_  ran  F  /\  ran  F  C_  Y )  ->  ( F  e.  ( ( Jt  ( A [,] B ) )  Cn  K )  <->  F  e.  ( ( Jt  ( A [,] B ) )  Cn  ( Kt  ran  F
) ) ) )
9391, 92syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F  e.  ( ( Jt  ( A [,] B ) )  Cn  K )  <->  F  e.  ( ( Jt  ( A [,] B ) )  Cn  ( Kt  ran  F
) ) ) )
9418, 93mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F  e.  ( ( Jt  ( A [,] B
) )  Cn  ( Kt  ran  F ) ) )
9594adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( Kt  ran  F ) )  ->  F  e.  ( ( Jt  ( A [,] B ) )  Cn  ( Kt  ran  F ) ) )
96 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( Kt  ran  F ) )  ->  u  e.  ( Kt 
ran  F ) )
9795, 96jca 532 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( Kt  ran  F ) )  ->  ( F  e.  ( ( Jt  ( A [,] B ) )  Cn  ( Kt  ran  F
) )  /\  u  e.  ( Kt  ran  F ) ) )
98 cnima 19634 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( ( Jt  ( A [,] B
) )  Cn  ( Kt  ran  F ) )  /\  u  e.  ( Kt  ran  F ) )  ->  ( `' F " u )  e.  ( Jt  ( A [,] B ) ) )
9986, 97, 983syl 20 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( `' F "
u )  e.  ( Jt  ( A [,] B
) ) )
1002topontopi 19301 . . . . . . . . . . . . . . . . 17  |-  ( topGen ` 
ran  (,) )  e.  Top
1011, 100eqeltri 2551 . . . . . . . . . . . . . . . 16  |-  J  e. 
Top
102101a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  Top )
103 reex 9595 . . . . . . . . . . . . . . . . 17  |-  RR  e.  _V
104103a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  RR  e.  _V )
105104, 9ssexd 4600 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A [,] B
)  e.  _V )
106102, 105jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( J  e.  Top  /\  ( A [,] B
)  e.  _V )
)
10784, 106syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( J  e.  Top  /\  ( A [,] B
)  e.  _V )
)
108 elrest 14700 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( A [,] B )  e.  _V )  -> 
( ( `' F " u )  e.  ( Jt  ( A [,] B
) )  <->  E. w  e.  J  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) ) )
109107, 108syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( ( `' F " u )  e.  ( Jt  ( A [,] B
) )  <->  E. w  e.  J  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) ) )
11099, 109mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  ->  E. w  e.  J  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )
111843ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  ph )
112 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
113112ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
y  e.  RR )
1141133ad2ant1 1017 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  y  e.  RR )
115 simp1r 1021 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  ( G `  y )  e.  u
)
116111, 114, 115jca31 534 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  ( ( ph  /\  y  e.  RR )  /\  ( G `  y )  e.  u
) )
117 simp2 997 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  w  e.  J )
118 simp3 998 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )
119116, 117, 1183jca 1176 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  ( (
( ph  /\  y  e.  RR )  /\  ( G `  y )  e.  u )  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) ) )
120 simpll2 1036 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
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 )
121101a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  J  ->  J  e.  Top )
122 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  J  ->  w  e.  J )
123 iooretop 21141 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -oo (,) A )  e.  (
topGen `  ran  (,) )
124123, 1eleqtrri 2554 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -oo (,) A )  e.  J
125 iooretop 21141 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B (,) +oo )  e.  ( topGen `  ran  (,) )
126125, 1eleqtrri 2554 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( B (,) +oo )  e.  J
127 unopn 19281 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( J  e.  Top  /\  ( -oo (,) A )  e.  J  /\  ( B (,) +oo )  e.  J )  ->  (
( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J
)
128101, 124, 126, 127mp3an 1324 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J
129128a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  J  ->  (
( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J
)
130121, 122, 1293jca 1176 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  J  ->  ( J  e.  Top  /\  w  e.  J  /\  (
( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J
) )
131 unopn 19281 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( J  e.  Top  /\  w  e.  J  /\  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J )  -> 
( w  u.  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )  e.  J )
132130, 131syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  J  ->  (
w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  e.  J )
133120, 132syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
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 )
134 simpl1l 1047 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 ) )
135134adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 ) )
136 simpl1r 1048 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 )
137136adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 )
138 simpll3 1037 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 ) ) )
139135, 137, 138jca31 534 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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
)  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) ) )
140 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  y  e.  RR )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ph )
141 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  y  e.  RR )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  -.  y  e.  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )
142 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  y  e.  RR )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  -> 
y  e.  RR )
143140, 141, 142jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  y  e.  RR )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  -> 
( ( ph  /\  -.  y  e.  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )  /\  y  e.  RR )
)
144 difreicc 11664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( RR  \  ( A [,] B ) )  =  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )
1457, 144syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  ( RR  \  ( A [,] B ) )  =  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )
146 eqcom 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( RR  \  ( A [,] B ) )  =  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  <-> 
( ( -oo (,) A )  u.  ( B (,) +oo ) )  =  ( RR  \ 
( A [,] B
) ) )
147146imbi2i 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  ->  ( RR  \ 
( A [,] B
) )  =  ( ( -oo (,) A
)  u.  ( B (,) +oo ) ) )  <->  ( ph  ->  ( ( -oo (,) A
)  u.  ( B (,) +oo ) )  =  ( RR  \ 
( A [,] B
) ) ) )
148145, 147mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ph  ->  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  =  ( RR  \ 
( A [,] B
) ) )
149148eleq2d 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  ( y  e.  ( ( -oo (,) A
)  u.  ( B (,) +oo ) )  <-> 
y  e.  ( RR 
\  ( A [,] B ) ) ) )
150149notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  ( -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  <->  -.  y  e.  ( RR  \  ( A [,] B ) ) ) )
151150biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  ->  -.  y  e.  ( RR  \  ( A [,] B ) ) ) )
152151imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  -.  y  e.  ( RR  \  ( A [,] B ) ) )
153 eldif 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  ( RR  \ 
( A [,] B
) )  <->  ( y  e.  RR  /\  -.  y  e.  ( A [,] B
) ) )
154152, 153sylnib 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  -.  (
y  e.  RR  /\  -.  y  e.  ( A [,] B ) ) )
155 imnan 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( y  e.  RR  ->  -. 
-.  y  e.  ( A [,] B ) )  <->  -.  ( y  e.  RR  /\  -.  y  e.  ( A [,] B
) ) )
156154, 155sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( y  e.  RR  ->  -.  -.  y  e.  ( A [,] B
) ) )
157156imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  /\  y  e.  RR )  ->  -.  -.  y  e.  ( A [,] B
) )
158157notnotrd 113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  /\  y  e.  RR )  ->  y  e.  ( A [,] B ) )
159143, 158syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  y  e.  RR )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  -> 
y  e.  ( A [,] B ) )
160159adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  y  e.  ( A [,] B ) )
161 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ph )
162161, 160jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( ph  /\  y  e.  ( A [,] B ) ) )
1639sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  RR )
16421adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  F :
( A [,] B
) --> Y )
165164ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  y  e.  ( A [,] B
) )  /\  y  e.  ( A [,] B
) )  ->  ( F `  y )  e.  Y )
16621, 34jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ph  ->  ( F : ( A [,] B ) --> Y  /\  A  e.  ( A [,] B
) ) )
167 ffvelrn 6030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( F : ( A [,] B ) --> Y  /\  A  e.  ( A [,] B ) )  ->  ( F `  A )  e.  Y
)
168166, 167syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  ( F `  A
)  e.  Y )
169168ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  y  e.  ( A [,] B ) )  /\  -.  y  e.  ( A [,] B ) )  /\  y  <  A
)  ->  ( F `  A )  e.  Y
)
17090, 47sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  ( F `  B
)  e.  Y )
171170ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  y  e.  ( A [,] B ) )  /\  -.  y  e.  ( A [,] B ) )  /\  -.  y  < 
A )  ->  ( F `  B )  e.  Y )
172169, 171ifclda 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  y  e.  ( A [,] B
) )  /\  -.  y  e.  ( A [,] B ) )  ->  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )  e.  Y )
173165, 172ifclda 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  if (
y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  Y )
174163, 173jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  e.  RR  /\  if ( y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  Y ) )
17580fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 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 ) ) ) )
176174, 175syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( G `  y )  =  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
177 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  ( A [,] B ) )
178 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  ( A [,] B )  ->  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )  =  ( F `  y ) )
179177, 178syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  if (
y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  =  ( F `
 y ) )
180176, 179eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( G `  y )  =  ( F `  y ) )
181180eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  y )  =  ( G `  y ) )
182162, 181syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( F `  y )  =  ( G `  y ) )
183 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( G `  y )  e.  u
)
184182, 183eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( F `  y )  e.  u
)
185160, 184jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( y  e.  ( A [,] B
)  /\  ( F `  y )  e.  u
) )
186161, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  F  Fn  ( A [,] B ) )
187 elpreima 6008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( F  Fn  ( A [,] B )  ->  (
y  e.  ( `' F " u )  <-> 
( y  e.  ( A [,] B )  /\  ( F `  y )  e.  u
) ) )
188186, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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
) ) )
189185, 188mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  y  e.  ( `' F " u ) )
190189adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 ) )
191 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 ) ) )
192190, 191eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 ) ) )
193 elin 3692 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  ( w  i^i  ( A [,] B
) )  <->  ( y  e.  w  /\  y  e.  ( A [,] B
) ) )
194192, 193sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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
) ) )
195194simpld 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 )
196195ex 434 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) )
197196orrd 378 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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
) )
198197orcomd 388 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) ) ) )
199 elun 3650 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  <->  ( y  e.  w  \/  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) )
200198, 199sylibr 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  y  e.  ( w  u.  (
( -oo (,) A )  u.  ( B (,) +oo ) ) ) )
201139, 200syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
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 ) ) ) )
202 imaundi 5424 . . . . . . . . . . . . . . . . . . . . 21  |-  ( G
" ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) )  =  ( ( G " w
)  u.  ( G
" ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) )
203202a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 ) ) ) )  =  ( ( G
" w )  u.  ( G " (
( -oo (,) A )  u.  ( B (,) +oo ) ) ) ) )
204135simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
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 )
2053a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  J  ->  J  e.  (TopOn `  RR )
)
206205, 122jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( w  e.  J  ->  ( J  e.  (TopOn `  RR )  /\  w  e.  J
) )
207 toponss 19299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( J  e.  (TopOn `  RR )  /\  w  e.  J )  ->  w  C_  RR )
208206, 207syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  e.  J  ->  w  C_  RR )
209120, 208syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
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 )
210204, 209jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
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 ) )
211210, 138jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
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
) ) ) )
212 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
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 )
213211, 212jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
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 ) ) )  /\  ( F `
 A )  e.  u ) )
214 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
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 )
215213, 214jca 532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
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 ) ) )  /\  ( F `
 A )  e.  u )  /\  ( F `  B )  e.  u ) )
216 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ y ( ( ( (
ph  /\  w  C_  RR )  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  /\  ( F `
 A )  e.  u )  /\  ( F `  B )  e.  u )
21755funmpt2 5631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  Fun  G
218217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  Fun  G )
219218ad5antr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
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 )
220 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
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.  ( G " w
) )
221219, 220jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
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  /\  y  e.  ( G " w
) ) )
222 fvelima 5926 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Fun  G  /\  y  e.  ( G " w
) )  ->  E. z  e.  w  ( G `  z )  =  y )
223221, 222syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
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 )
224 eqcom 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( G `  z )  =  y  <->  y  =  ( G `  z ) )
225224biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( G `  z )  =  y  ->  y  =  ( G `  z ) )
2262253ad2ant3 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( 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 ) )
227 simp1ll 1059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( 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 ) )
228 simp1lr 1060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( 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 )
229 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( 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 )
230227, 228, 229jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( ( 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 )  /\  ( F `  B )  e.  u )  /\  z  e.  w )
)
231 simp-5l 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( 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 ) )
232 simp-5r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( 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 ) ) )
233 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( 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
)
234231, 232, 233jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( 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 ) )
235 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( 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.  ( A [,] B ) )
236234, 235jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( 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 )  /\  z  e.  ( A [,] B ) ) )
237 simp-4l 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ph )
238 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )
239 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  z  e.  w )
240237, 238, 239jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  (
( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )
)
241 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  z  e.  ( A [,] B
) )
242240, 241jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  (
( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) ) )
243 simplll 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ph )
244 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( A [,] B ) )
245243, 244jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ( ph  /\  z  e.  ( A [,] B ) ) )
246 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ y ( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( G `  z
)  =  ( F `
 z ) )
247 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  z  ->  (
y  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
248247anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  z  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
249 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  z  ->  ( G `  y )  =  ( G `  z ) )
250 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  z  ->  ( F `  y )  =  ( F `  z ) )
251249, 250eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  z  ->  (
( G `  y
)  =  ( F `
 y )  <->  ( G `  z )  =  ( F `  z ) ) )
252248, 251imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( G `  y
)  =  ( F `
 y ) )  <-> 
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( G `  z
)  =  ( F `
 z ) ) ) )
253246, 252, 180chvar 1982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( G `  z )  =  ( F `  z ) )
254245, 253syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ( G `  z )  =  ( F `  z ) )
255242, 254syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( G `  z )  =  ( F `  z ) )
256 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  w  C_  RR )
257 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  w
)
258257, 244jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ( z  e.  w  /\  z  e.  ( A [,] B
) ) )
259 elin 3692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z  e.  ( w  i^i  ( A [,] B
) )  <->  ( z  e.  w  /\  z  e.  ( A [,] B
) ) )
260258, 259sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( w  i^i  ( A [,] B ) ) )
261 eqcom 2476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( `' F " u )  =  ( w  i^i  ( A [,] B
) )  <->  ( w  i^i  ( A [,] B
) )  =  ( `' F " u ) )
262261biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( `' F " u )  =  ( w  i^i  ( A [,] B
) )  ->  (
w  i^i  ( A [,] B ) )  =  ( `' F "
u ) )
263262ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ( w  i^i  ( A [,] B
) )  =  ( `' F " u ) )
264260, 263eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( `' F " u ) )
265242, 264syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  z  e.  ( `' F "
u ) )
266237, 256, 265jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  (
( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) ) )
267 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
z  e.  ( `' F " u ) )
26823ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  ->  F  Fn  ( A [,] B ) )
269 elpreima 6008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( F  Fn  ( A [,] B )  ->  (
z  e.  ( `' F " u )  <-> 
( z  e.  ( A [,] B )  /\  ( F `  z )  e.  u
) ) )
270268, 269syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
( z  e.  ( `' F " u )  <-> 
( z  e.  ( A [,] B )  /\  ( F `  z )  e.  u
) ) )
271267, 270mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
( z  e.  ( A [,] B )  /\  ( F `  z )  e.  u
) )
272271simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
( F `  z
)  e.  u )
273266, 272syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( F `  z )  e.  u )
274255, 273eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( G `  z )  e.  u )
275236, 274syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( 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
)
276 simp-6l 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( 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 )
277 simp-6r 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( 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 ) )  ->  w  C_  RR )
278 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( 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 `  A )  e.  u
)
279276, 277, 278jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( 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 `  A )  e.  u
) )
280 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( 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 `  B )  e.  u
)
281 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( 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 )
282279, 280, 281jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( 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 `  A )  e.  u )  /\  ( F `  B )  e.  u )  /\  z  e.  w )
)
283 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( ( 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.  ( A [,] B
) )
284282, 283jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( ( 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 `  A
)  e.  u )  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) ) )
285 simp-5l 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  ->  ph )
286 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( F `  A
)  e.  u )
287285, 286jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( ph  /\  ( F `  A )  e.  u ) )
288 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( F `  B
)  e.  u )
289 simp-5r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  ->  w  C_  RR )
290 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
z  e.  w )
291289, 290jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( w  C_  RR  /\  z  e.  w ) )
292 ssel2 3504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( w  C_  RR  /\  z  e.  w )  ->  z  e.  RR )
293291, 292syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
z  e.  RR )
294287, 288, 293jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
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 ) )
295 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  ->  -.  z  e.  ( A [,] B ) )
296294, 295jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
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 )  /\  -.  z  e.  ( A [,] B
) ) )
29780a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( 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 ) ) ) ) )
298 breq1 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  =  z  ->  (
y  <  A  <->  z  <  A ) )
299 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  =  z  ->  ( F `  A )  =  ( F `  A ) )
300 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  =  z  ->  ( F `  B )  =  ( F `  B ) )
301298, 299, 300ifeq123d 31337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  z  ->  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )  =  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )
302247, 250, 301ifeq123d 31337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 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 ) ) ) )
303302adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( (
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 ) ) ) )
304 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  ( F `  A
)  e.  u )  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  ->  z  e.  RR )
305 iffalse 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( -.  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 ) ) )
306305adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( 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 ) ) )
307 simp-5r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( (
ph  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  /\  z  <  A )  ->  ( F `  A )  e.  u )
308 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( (
ph  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  /\  -.  z  <  A )  -> 
( F `  B
)  e.  u )
309307, 308ifclda 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( 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 )
310306, 309eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( 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
)
311310idi 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( 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
)
312297, 303, 304, 311fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( 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
) ) ) )
313312, 306eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( 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
) ) )
314313, 309eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  ( F `  A
)  e.  u )  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  ->  ( G `  z )  e.  u )
315296, 314syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( G `  z
)  e.  u )
316284, 315syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( 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
)
317275, 316pm2.61dan 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
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 )
318230, 317syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( 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 )
319226, 318eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( 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 )
3203193exp 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
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
) ) )
321320rexlimdv 2957 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
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 ) )
322223, 321mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
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 )
323322ex 434 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 ) )
324216, 323alrimi 1825 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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
) )
325215, 324syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
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 ) )
326 dfss2 3498 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( G " w ) 
C_  u  <->  A. y
( y  e.  ( G " w )  ->  y  e.  u
) )
327325, 326sylibr 212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 )
328204, 212, 214jca31 534 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
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  /\  ( F `  A )  e.  u )  /\  ( F `  B )  e.  u ) )
329 imaundi 5424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G
" ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  =  ( ( G " ( -oo (,) A ) )  u.  ( G " ( B (,) +oo ) ) )
330 nfv 1683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/ t
ph
331217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  Fun  G )
332 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  t  e.  ( G " ( -oo (,) A ) ) )
333331, 332jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  ( Fun  G  /\  t  e.  ( G " ( -oo (,) A ) ) ) )
334 fvelima 5926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( Fun  G  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  E. z  e.  ( -oo (,) A
) ( G `  z )  =  t )
335333, 334syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  E. z  e.  ( -oo (,) A ) ( G `  z
)  =  t )
336 simp1l 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  ph )
337 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  z  e.  ( -oo (,) A ) )
338336, 337jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  ( ph  /\  z  e.  ( -oo (,) A ) ) )
339 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  ( G `  z )  =  t )
340338, 339jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  ( ( ph  /\  z  e.  ( -oo (,) A ) )  /\  ( G `
 z )  =  t ) )
341 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  -> 
( G `  z
)  =  t )
342341eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  -> 
t  =  ( G `
 z ) )
34380a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  G  =  ( y  e.  RR  |->  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) ) )
344302adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( 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 ) ) ) )
345 elioore 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( z  e.  ( -oo (,) A )  ->  z  e.  RR )
346345adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  z  e.  RR )
347 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( z  e.  ( -oo (,) A )  <->  ( ( -oo  e.  RR*  /\  A  e. 
RR*  /\  z  e.  RR* )  /\  ( -oo  <  z  /\  z  < 
A ) ) )
348347biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( z  e.  ( -oo (,) A )  ->  (
( -oo  e.  RR*  /\  A  e.  RR*  /\  z  e. 
RR* )  /\  ( -oo  <  z  /\  z  <  A ) ) )
349348simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( z  e.  ( -oo (,) A )  ->  ( -oo  <  z  /\  z  <  A ) )
350349simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( z  e.  ( -oo (,) A )  ->  z  <  A )
351350adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  z  <  A )
3525, 345anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( z  e.  RR  /\  A  e.  RR ) )
353 ltnle 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( z  e.  RR  /\  A  e.  RR )  ->  ( z  <  A  <->  -.  A  <_  z )
)
354352, 353syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( z  <  A  <->  -.  A  <_  z ) )
355351, 354mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  -.  A  <_  z )
356 3mix2 1166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( -.  A  <_  z  ->  ( -.  z  e.  RR  \/  -.  A  <_  z  \/  -.  z  <_  B
) )
357 3ianor 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( -.  ( z  e.  RR  /\  A  <_  z  /\  z  <_  B )  <->  ( -.  z  e.  RR  \/  -.  A  <_  z  \/ 
-.  z  <_  B
) )
358356, 357sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( -.  A  <_  z  ->  -.  ( z  e.  RR  /\  A  <_  z  /\  z  <_  B ) )
359355, 358syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  -.  (
z  e.  RR  /\  A  <_  z  /\  z  <_  B ) )
3607adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( A  e.  RR  /\  B  e.  RR ) )
361 elicc2 11601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( z  e.  ( A [,] B )  <-> 
( z  e.  RR  /\  A  <_  z  /\  z  <_  B ) ) )
362360, 361syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( z  e.  ( A [,] B
)  <->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) ) )
363359, 362mtbird 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  -.  z  e.  ( A [,] B
) )
364363, 305syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
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 ) ) )
365 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( z  <  A  ->  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) )  =  ( F `
 A ) )
366350, 365syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( z  e.  ( -oo (,) A )  ->  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) )  =  ( F `
 A ) )
367366adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  if (
z  <  A , 
( F `  A
) ,  ( F `
 B ) )  =  ( F `  A ) )
368364, 367eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  if (
z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  =  ( F `
 A ) )
369168adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( F `  A )  e.  Y
)
370368, 369eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  if (
z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  Y )
371343, 344, 346, 370fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( G `  z )  =  if ( z  e.  ( A [,] B ) ,  ( F `  z ) ,  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
372371adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  -> 
( G `  z
)  =  if ( z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B )