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

Theorem icccncfext 31872
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 . . . . . . . . . . . 12  |-  J  =  ( topGen `  ran  (,) )
2 retopon 21396 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  (TopOn `  RR )
31, 2eqeltri 2541 . . . . . . . . . . 11  |-  J  e.  (TopOn `  RR )
4 icccncfext.5 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  RR )
5 icccncfext.6 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
64, 5iccssred 31721 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] B
)  C_  RR )
7 resttopon 19789 . . . . . . . . . . 11  |-  ( ( J  e.  (TopOn `  RR )  /\  ( A [,] B )  C_  RR )  ->  ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) ) )
83, 6, 7sylancr 663 . . . . . . . . . 10  |-  ( ph  ->  ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) ) )
9 icccncfext.8 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  Top )
10 icccncfext.3 . . . . . . . . . . . 12  |-  Y  = 
U. K
119, 10jctir 538 . . . . . . . . . . 11  |-  ( ph  ->  ( K  e.  Top  /\  Y  =  U. K
) )
12 istopon 19553 . . . . . . . . . . 11  |-  ( K  e.  (TopOn `  Y
)  <->  ( K  e. 
Top  /\  Y  =  U. K ) )
1311, 12sylibr 212 . . . . . . . . . 10  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
14 icccncfext.9 . . . . . . . . . 10  |-  ( ph  ->  F  e.  ( ( Jt  ( A [,] B
) )  Cn  K
) )
15 cnf2 19877 . . . . . . . . . 10  |-  ( ( ( Jt  ( A [,] B ) )  e.  (TopOn `  ( A [,] B ) )  /\  K  e.  (TopOn `  Y
)  /\  F  e.  ( ( Jt  ( A [,] B ) )  Cn  K ) )  ->  F : ( A [,] B ) --> Y )
168, 13, 14, 15syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  F : ( A [,] B ) --> Y )
17 ffn 5737 . . . . . . . . 9  |-  ( F : ( A [,] B ) --> Y  ->  F  Fn  ( A [,] B ) )
1816, 17syl 16 . . . . . . . 8  |-  ( ph  ->  F  Fn  ( A [,] B ) )
19 dffn3 5744 . . . . . . . 8  |-  ( F  Fn  ( A [,] B )  <->  F :
( A [,] B
) --> ran  F )
2018, 19sylib 196 . . . . . . 7  |-  ( ph  ->  F : ( A [,] B ) --> ran 
F )
2120ffvelrnda 6032 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  y )  e.  ran  F )
22 fnfun 5684 . . . . . . . . . 10  |-  ( F  Fn  ( A [,] B )  ->  Fun  F )
2318, 22syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  F )
244rexrd 9660 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR* )
255rexrd 9660 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR* )
26 icccncfext.7 . . . . . . . . . . 11  |-  ( ph  ->  A  <_  B )
27 lbicc2 11661 . . . . . . . . . . 11  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
2824, 25, 26, 27syl3anc 1228 . . . . . . . . . 10  |-  ( ph  ->  A  e.  ( A [,] B ) )
29 fndm 5686 . . . . . . . . . . . 12  |-  ( F  Fn  ( A [,] B )  ->  dom  F  =  ( A [,] B ) )
3018, 29syl 16 . . . . . . . . . . 11  |-  ( ph  ->  dom  F  =  ( A [,] B ) )
3130eqcomd 2465 . . . . . . . . . 10  |-  ( ph  ->  ( A [,] B
)  =  dom  F
)
3228, 31eleqtrd 2547 . . . . . . . . 9  |-  ( ph  ->  A  e.  dom  F
)
33 fvelrn 6025 . . . . . . . . 9  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( F `  A
)  e.  ran  F
)
3423, 32, 33syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( F `  A
)  e.  ran  F
)
35 ubicc2 11662 . . . . . . . . . . 11  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  B  e.  ( A [,] B
) )
3624, 25, 26, 35syl3anc 1228 . . . . . . . . . 10  |-  ( ph  ->  B  e.  ( A [,] B ) )
3736, 31eleqtrd 2547 . . . . . . . . 9  |-  ( ph  ->  B  e.  dom  F
)
38 fvelrn 6025 . . . . . . . . 9  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( F `  B
)  e.  ran  F
)
3923, 37, 38syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( F `  B
)  e.  ran  F
)
4034, 39ifcld 3987 . . . . . . 7  |-  ( ph  ->  if ( y  < 
A ,  ( F `
 A ) ,  ( F `  B
) )  e.  ran  F )
4140adantr 465 . . . . . 6  |-  ( (
ph  /\  -.  y  e.  ( A [,] B
) )  ->  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )  e.  ran  F
)
4221, 41ifclda 3976 . . . . 5  |-  ( ph  ->  if ( y  e.  ( A [,] B
) ,  ( F `
 y ) ,  if ( y  < 
A ,  ( F `
 A ) ,  ( F `  B
) ) )  e. 
ran  F )
4342adantr 465 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  if ( y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  ran  F
)
44 icccncfext.4 . . . . 5  |-  G  =  ( x  e.  RR  |->  if ( x  e.  ( A [,] B ) ,  ( F `  x ) ,  if ( x  <  A , 
( F `  A
) ,  ( F `
 B ) ) ) )
45 nfv 1708 . . . . . . 7  |-  F/ y  x  e.  ( A [,] B )
46 nfcv 2619 . . . . . . 7  |-  F/_ y
( F `  x
)
47 nfcv 2619 . . . . . . 7  |-  F/_ y if ( x  <  A ,  ( F `  A ) ,  ( F `  B ) )
4845, 46, 47nfif 3973 . . . . . 6  |-  F/_ y if ( x  e.  ( A [,] B ) ,  ( F `  x ) ,  if ( x  <  A , 
( F `  A
) ,  ( F `
 B ) ) )
49 nfv 1708 . . . . . . 7  |-  F/ x  y  e.  ( A [,] B )
50 icccncfext.1 . . . . . . . 8  |-  F/_ x F
51 nfcv 2619 . . . . . . . 8  |-  F/_ x
y
5250, 51nffv 5879 . . . . . . 7  |-  F/_ x
( F `  y
)
53 nfv 1708 . . . . . . . 8  |-  F/ x  y  <  A
54 nfcv 2619 . . . . . . . . 9  |-  F/_ x A
5550, 54nffv 5879 . . . . . . . 8  |-  F/_ x
( F `  A
)
56 nfcv 2619 . . . . . . . . 9  |-  F/_ x B
5750, 56nffv 5879 . . . . . . . 8  |-  F/_ x
( F `  B
)
5853, 55, 57nfif 3973 . . . . . . 7  |-  F/_ x if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )
5949, 52, 58nfif 3973 . . . . . 6  |-  F/_ x if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )
60 eleq1 2529 . . . . . . 7  |-  ( x  =  y  ->  (
x  e.  ( A [,] B )  <->  y  e.  ( A [,] B ) ) )
61 fveq2 5872 . . . . . . 7  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
62 breq1 4459 . . . . . . . 8  |-  ( x  =  y  ->  (
x  <  A  <->  y  <  A ) )
6362ifbid 3966 . . . . . . 7  |-  ( x  =  y  ->  if ( x  <  A , 
( F `  A
) ,  ( F `
 B ) )  =  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) )
6460, 61, 63ifbieq12d 3971 . . . . . 6  |-  ( 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 ) ) ) )
6548, 59, 64cbvmpt 4547 . . . . 5  |-  ( 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 ) ) ) )
6644, 65eqtri 2486 . . . 4  |-  G  =  ( y  e.  RR  |->  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
6743, 66fmptd 6056 . . 3  |-  ( ph  ->  G : RR --> ran  F
)
6867adantr 465 . . . . 5  |-  ( (
ph  /\  y  e.  RR )  ->  G : RR
--> ran  F )
69 simplll 759 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  ->  ph )
70 simplr 755 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  ->  u  e.  ( Kt  ran  F ) )
7169, 70jca 532 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( ph  /\  u  e.  ( Kt  ran  F ) ) )
72 ssid 3518 . . . . . . . . . . . . . 14  |-  ran  F  C_ 
ran  F
7372a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  F  C_  ran  F )
74 frn 5743 . . . . . . . . . . . . . 14  |-  ( F : ( A [,] B ) --> Y  ->  ran  F  C_  Y )
7516, 74syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  F  C_  Y
)
76 cnrest2 19914 . . . . . . . . . . . . 13  |-  ( ( 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
) ) ) )
7713, 73, 75, 76syl3anc 1228 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  e.  ( ( Jt  ( A [,] B ) )  Cn  K )  <->  F  e.  ( ( Jt  ( A [,] B ) )  Cn  ( Kt  ran  F
) ) ) )
7814, 77mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( Jt  ( A [,] B
) )  Cn  ( Kt  ran  F ) ) )
7978anim1i 568 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( Kt  ran  F ) )  ->  ( F  e.  ( ( Jt  ( A [,] B ) )  Cn  ( Kt  ran  F
) )  /\  u  e.  ( Kt  ran  F ) ) )
80 cnima 19893 . . . . . . . . . 10  |-  ( ( F  e.  ( ( Jt  ( A [,] B
) )  Cn  ( Kt  ran  F ) )  /\  u  e.  ( Kt  ran  F ) )  ->  ( `' F " u )  e.  ( Jt  ( A [,] B ) ) )
8171, 79, 803syl 20 . . . . . . . . 9  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( `' F "
u )  e.  ( Jt  ( A [,] B
) ) )
82 retop 21394 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
831, 82eqeltri 2541 . . . . . . . . . . . . 13  |-  J  e. 
Top
8483a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  Top )
85 reex 9600 . . . . . . . . . . . . . 14  |-  RR  e.  _V
8685a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  e.  _V )
8786, 6ssexd 4603 . . . . . . . . . . . 12  |-  ( ph  ->  ( A [,] B
)  e.  _V )
8884, 87jca 532 . . . . . . . . . . 11  |-  ( ph  ->  ( J  e.  Top  /\  ( A [,] B
)  e.  _V )
)
8969, 88syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
( J  e.  Top  /\  ( A [,] B
)  e.  _V )
)
90 elrest 14845 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  ( A [,] B )  e.  _V )  -> 
( ( `' F " u )  e.  ( Jt  ( A [,] B
) )  <->  E. w  e.  J  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) ) )
9189, 90syl 16 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) ) )
9281, 91mpbid 210 . . . . . . . 8  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  ->  E. w  e.  J  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )
93693ad2ant1 1017 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt 
ran  F ) )  /\  ( G `  y )  e.  u
)  /\  w  e.  J  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  ph )
94 simpllr 760 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  u  e.  ( Kt  ran  F ) )  /\  ( G `  y )  e.  u )  -> 
y  e.  RR )
95943ad2ant1 1017 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 )
96 simp1r 1021 . . . . . . . . . . 11  |-  ( ( ( ( ( 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
)
9793, 95, 96jca31 534 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) )
98 simpll2 1036 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 )
99 iooretop 21399 . . . . . . . . . . . . . . . . 17  |-  ( -oo (,) A )  e.  (
topGen `  ran  (,) )
10099, 1eleqtrri 2544 . . . . . . . . . . . . . . . 16  |-  ( -oo (,) A )  e.  J
101 iooretop 21399 . . . . . . . . . . . . . . . . 17  |-  ( B (,) +oo )  e.  ( topGen `  ran  (,) )
102101, 1eleqtrri 2544 . . . . . . . . . . . . . . . 16  |-  ( B (,) +oo )  e.  J
103 unopn 19539 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  ( -oo (,) A )  e.  J  /\  ( B (,) +oo )  e.  J )  ->  (
( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J
)
10483, 100, 102, 103mp3an 1324 . . . . . . . . . . . . . . 15  |-  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J
105 unopn 19539 . . . . . . . . . . . . . . 15  |-  ( ( J  e.  Top  /\  w  e.  J  /\  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  e.  J )  -> 
( w  u.  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )  e.  J )
10683, 104, 105mp3an13 1315 . . . . . . . . . . . . . 14  |-  ( w  e.  J  ->  (
w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  e.  J )
10798, 106syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
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 )
108 simpl1l 1047 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 ) )
109108adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 ) )
110 simpl1r 1048 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 )
111110adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 )
112 simpll3 1037 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 ) ) )
113 difreicc 11677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( RR  \  ( A [,] B ) )  =  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )
1144, 5, 113syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( RR  \  ( A [,] B ) )  =  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )
115114eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  =  ( RR  \ 
( A [,] B
) ) )
116115eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( y  e.  ( ( -oo (,) A
)  u.  ( B (,) +oo ) )  <-> 
y  e.  ( RR 
\  ( A [,] B ) ) ) )
117116notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  <->  -.  y  e.  ( RR  \  ( A [,] B ) ) ) )
118117biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  -.  y  e.  ( RR  \  ( A [,] B ) ) )
119 eldif 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( RR  \ 
( A [,] B
) )  <->  ( y  e.  RR  /\  -.  y  e.  ( A [,] B
) ) )
120118, 119sylnib 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  -.  (
y  e.  RR  /\  -.  y  e.  ( A [,] B ) ) )
121 imnan 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  RR  ->  -. 
-.  y  e.  ( A [,] B ) )  <->  -.  ( y  e.  RR  /\  -.  y  e.  ( A [,] B
) ) )
122120, 121sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( y  e.  RR  ->  -.  -.  y  e.  ( A [,] B
) ) )
123122imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  /\  y  e.  RR )  ->  -.  -.  y  e.  ( A [,] B
) )
124123notnotrd 113 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  /\  y  e.  RR )  ->  y  e.  ( A [,] B ) )
125124an32s 804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  RR )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  -> 
y  e.  ( A [,] B ) )
126125adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  y  e.  ( A [,] B ) )
127 simplll 759 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ph )
1286sselda 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  RR )
12916adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  F :
( A [,] B
) --> Y )
130129ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  y  e.  ( A [,] B
) )  /\  y  e.  ( A [,] B
) )  ->  ( F `  y )  e.  Y )
13116, 28ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( F `  A
)  e.  Y )
132131ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  y  e.  ( A [,] B ) )  /\  -.  y  e.  ( A [,] B ) )  /\  y  <  A
)  ->  ( F `  A )  e.  Y
)
13316, 36ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( F `  B
)  e.  Y )
134133ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  y  e.  ( A [,] B ) )  /\  -.  y  e.  ( A [,] B ) )  /\  -.  y  < 
A )  ->  ( F `  B )  e.  Y )
135132, 134ifclda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  y  e.  ( A [,] B
) )  /\  -.  y  e.  ( A [,] B ) )  ->  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )  e.  Y )
136130, 135ifclda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  if (
y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  Y )
13766fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) ) )
138128, 136, 137syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( G `  y )  =  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
139 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  y  e.  ( A [,] B ) )
140139iftrued 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  if (
y  e.  ( A [,] B ) ,  ( F `  y
) ,  if ( y  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  =  ( F `
 y ) )
141138, 140eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( G `  y )  =  ( F `  y ) )
142141eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( F `  y )  =  ( G `  y ) )
143127, 126, 142syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( F `  y )  =  ( G `  y ) )
144 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( G `  y )  e.  u
)
145143, 144eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( F `  y )  e.  u
)
146127, 18syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  F  Fn  ( A [,] B ) )
147 elpreima 6008 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F  Fn  ( A [,] B )  ->  (
y  e.  ( `' F " u )  <-> 
( y  e.  ( A [,] B )  /\  ( F `  y )  e.  u
) ) )
148146, 147syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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
) ) )
149126, 145, 148mpbir2and 922 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  y  e.  ( `' F " u ) )
150149adantlr 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 ) )
151 simplr 755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 ) ) )
152150, 151eleqtrd 2547 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 ) ) )
153 elin 3683 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( w  i^i  ( A [,] B
) )  <->  ( y  e.  w  /\  y  e.  ( A [,] B
) ) )
154152, 153sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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
) ) )
155154simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 )
156155ex 434 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) )
157156orrd 378 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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
) )
158157orcomd 388 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) ) )
159 elun 3641 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  <->  ( y  e.  w  \/  y  e.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) )
160158, 159sylibr 212 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B ) ) )  ->  y  e.  ( w  u.  (
( -oo (,) A )  u.  ( B (,) +oo ) ) ) )
161109, 111, 112, 160syl21anc 1227 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
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 ) ) ) )
162 imaundi 5425 . . . . . . . . . . . . . 14  |-  ( G
" ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) )  =  ( ( G " w
)  u.  ( G
" ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) )
163109simpld 459 . . . . . . . . . . . . . . . . . 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 )  ->  ph )
164 toponss 19557 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J  e.  (TopOn `  RR )  /\  w  e.  J )  ->  w  C_  RR )
1653, 98, 164sylancr 663 . . . . . . . . . . . . . . . . . 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  C_  RR )
166163, 165, 112jca31 534 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
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
) ) ) )
167 simplr 755 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
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 )
168 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
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 )
16944funmpt2 5631 . . . . . . . . . . . . . . . . . . . . . . 23  |-  Fun  G
170169a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Fun  G )
171170ad5antr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
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 )
172 fvelima 5925 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Fun  G  /\  y  e.  ( G " w
) )  ->  E. z  e.  w  ( G `  z )  =  y )
173171, 172sylancom 667 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 )
174 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( G `  z )  =  y  <->  y  =  ( G `  z ) )
175174biimpi 194 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( G `  z )  =  y  ->  y  =  ( G `  z ) )
1761753ad2ant3 1019 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( 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 ) )
177 simp1ll 1059 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( ( 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 ) )
178 simp1lr 1060 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( ( 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 )
179 simp2 997 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( ( 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 )
180 simp-5l 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( 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 ) )
181 simp-5r 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( 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 ) ) )
182 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( 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
)
183180, 181, 182jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( ( 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 ) )
184 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  z  ->  (
y  e.  ( A [,] B )  <->  z  e.  ( A [,] B ) ) )
185184anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  z  ->  (
( ph  /\  y  e.  ( A [,] B
) )  <->  ( ph  /\  z  e.  ( A [,] B ) ) ) )
186 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  z  ->  ( G `  y )  =  ( G `  z ) )
187 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  z  ->  ( F `  y )  =  ( F `  z ) )
188186, 187eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  z  ->  (
( G `  y
)  =  ( F `
 y )  <->  ( G `  z )  =  ( F `  z ) ) )
189185, 188imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( A [,] B ) )  -> 
( G `  y
)  =  ( F `
 y ) )  <-> 
( ( ph  /\  z  e.  ( A [,] B ) )  -> 
( G `  z
)  =  ( F `
 z ) ) ) )
190189, 141chvarv 2015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( G `  z )  =  ( F `  z ) )
191190adant423 31607 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ( G `  z )  =  ( F `  z ) )
192191adantlllr 31598 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( G `  z )  =  ( F `  z ) )
193 simp-4l 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ph )
194 simp-4r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  w  C_  RR )
195 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  w
)
196 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( A [,] B ) )
197195, 196elind 3684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( w  i^i  ( A [,] B ) ) )
198 eqcom 2466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( `' F " u )  =  ( w  i^i  ( A [,] B
) )  <->  ( w  i^i  ( A [,] B
) )  =  ( `' F " u ) )
199198biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( `' F " u )  =  ( w  i^i  ( A [,] B
) )  ->  (
w  i^i  ( A [,] B ) )  =  ( `' F "
u ) )
200199ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  ( w  i^i  ( A [,] B
) )  =  ( `' F " u ) )
201197, 200eleqtrd 2547 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( `' F " u )  =  ( w  i^i  ( A [,] B
) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B ) )  ->  z  e.  ( `' F " u ) )
202201adantlllr 31598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  z  e.  ( `' F "
u ) )
203 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
z  e.  ( `' F " u ) )
20418ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  ->  F  Fn  ( A [,] B ) )
205 elpreima 6008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( F  Fn  ( A [,] B )  ->  (
z  e.  ( `' F " u )  <-> 
( z  e.  ( A [,] B )  /\  ( F `  z )  e.  u
) ) )
206204, 205syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
( z  e.  ( `' F " u )  <-> 
( z  e.  ( A [,] B )  /\  ( F `  z )  e.  u
) ) )
207203, 206mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
( z  e.  ( A [,] B )  /\  ( F `  z )  e.  u
) )
208207simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  w  C_  RR )  /\  z  e.  ( `' F "
u ) )  -> 
( F `  z
)  e.  u )
209193, 194, 202, 208syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( F `  z )  e.  u )
210192, 209eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  w  C_  RR )  /\  ( `' F "
u )  =  ( w  i^i  ( A [,] B ) ) )  /\  z  e.  w )  /\  z  e.  ( A [,] B
) )  ->  ( G `  z )  e.  u )
211183, 210sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( ( 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
)
212 simp-5l 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  ->  ph )
213 simp-4r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( F `  A
)  e.  u )
214212, 213jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( ph  /\  ( F `  A )  e.  u ) )
215 simpllr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( F `  B
)  e.  u )
216 simp-5r 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  ->  w  C_  RR )
217 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
z  e.  w )
218216, 217sseldd 3500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
z  e.  RR )
219214, 215, 218jca31 534 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
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 ) )
22066a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 ) ) ) ) )
221 breq1 4459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  z  ->  (
y  <  A  <->  z  <  A ) )
222221ifbid 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  z  ->  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) )  =  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )
223184, 187, 222ifeq123d 31614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) ) )
224223adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( (
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 ) ) ) )
225 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( F `  A
)  e.  u )  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  ->  z  e.  RR )
226 iffalse 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -.  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 ) ) )
227226adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 ) ) )
228 simp-5r 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  /\  z  <  A )  ->  ( F `  A )  e.  u )
229 simp-4r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( (
ph  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  /\  -.  z  <  A )  -> 
( F `  B
)  e.  u )
230228, 229ifclda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 )
231227, 230eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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
)
232220, 224, 225, 231fvmptd 5961 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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
) ) ) )
233232, 227eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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
) ) )
234233, 230eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( F `  A
)  e.  u )  /\  ( F `  B )  e.  u
)  /\  z  e.  RR )  /\  -.  z  e.  ( A [,] B
) )  ->  ( G `  z )  e.  u )
235219, 234sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  w  C_  RR )  /\  ( F `  A )  e.  u
)  /\  ( F `  B )  e.  u
)  /\  z  e.  w )  /\  -.  z  e.  ( A [,] B ) )  -> 
( G `  z
)  e.  u )
236235adantl4r 750 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( ( 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
)
237211, 236pm2.61dan 791 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
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 )
238177, 178, 179, 237syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( 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 )
239176, 238eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( 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 )
240239rexlimdv3a 2951 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 ) )
241173, 240mpd 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
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 )
242241ex 434 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 ) )
243242alrimiv 1720 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( 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
) )
244166, 167, 168, 243syl21anc 1227 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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 ) )
245 dfss2 3488 . . . . . . . . . . . . . . . 16  |-  ( ( G " w ) 
C_  u  <->  A. y
( y  e.  ( G " w )  ->  y  e.  u
) )
246244, 245sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 )
247 imaundi 5425 . . . . . . . . . . . . . . . . 17  |-  ( G
" ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  =  ( ( G " ( -oo (,) A ) )  u.  ( G " ( B (,) +oo ) ) )
248169a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  Fun  G )
249 fvelima 5925 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Fun  G  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  E. z  e.  ( -oo (,) A
) ( G `  z )  =  t )
250248, 249sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  E. z  e.  ( -oo (,) A ) ( G `  z
)  =  t )
251 simp1l 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  ph )
252 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  z  e.  ( -oo (,) A ) )
253 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  ( G `  z )  =  t )
25466a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  G  =  ( y  e.  RR  |->  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) ) )
255223adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 ) ) ) )
256 elioore 11584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  e.  ( -oo (,) A )  ->  z  e.  RR )
257256adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  z  e.  RR )
258 elioo3g 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z  e.  ( -oo (,) A )  <->  ( ( -oo  e.  RR*  /\  A  e. 
RR*  /\  z  e.  RR* )  /\  ( -oo  <  z  /\  z  < 
A ) ) )
259258biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z  e.  ( -oo (,) A )  ->  (
( -oo  e.  RR*  /\  A  e.  RR*  /\  z  e. 
RR* )  /\  ( -oo  <  z  /\  z  <  A ) ) )
260259simprrd 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( z  e.  ( -oo (,) A )  ->  z  <  A )
261260adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  z  <  A )
262 ltnle 9681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( z  e.  RR  /\  A  e.  RR )  ->  ( z  <  A  <->  -.  A  <_  z )
)
263256, 4, 262syl2anr 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( z  <  A  <->  -.  A  <_  z ) )
264261, 263mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  -.  A  <_  z )
265264intn3an2d 1339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  -.  (
z  e.  RR  /\  A  <_  z  /\  z  <_  B ) )
2664, 5jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
267266adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( A  e.  RR  /\  B  e.  RR ) )
268 elicc2 11614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( z  e.  ( A [,] B )  <-> 
( z  e.  RR  /\  A  <_  z  /\  z  <_  B ) ) )
269267, 268syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( z  e.  ( A [,] B
)  <->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) ) )
270265, 269mtbird 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  -.  z  e.  ( A [,] B
) )
271270iffalsed 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
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 ) ) )
272260iftrued 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  ( -oo (,) A )  ->  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) )  =  ( F `
 A ) )
273272adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  if (
z  <  A , 
( F `  A
) ,  ( F `
 B ) )  =  ( F `  A ) )
274271, 273eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  if (
z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  =  ( F `
 A ) )
275131adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( F `  A )  e.  Y
)
276274, 275eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  if (
z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  Y )
277254, 255, 257, 276fvmptd 5961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  ( -oo (,) A ) )  ->  ( G `  z )  =  if ( z  e.  ( A [,] B ) ,  ( F `  z ) ,  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
278277adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  -> 
( G `  z
)  =  if ( z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) ) )
279 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  -> 
( G `  z
)  =  t )
280274adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  ->  if ( z  e.  ( A [,] B ) ,  ( F `  z ) ,  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) ) )  =  ( F `  A ) )
281278, 279, 2803eqtr3d 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  ( -oo (,) A
) )  /\  ( G `  z )  =  t )  -> 
t  =  ( F `
 A ) )
282251, 252, 253, 281syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  /\  z  e.  ( -oo (,) A
)  /\  ( G `  z )  =  t )  ->  t  =  ( F `  A ) )
283282rexlimdv3a 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  ( E. z  e.  ( -oo (,) A
) ( G `  z )  =  t  ->  t  =  ( F `  A ) ) )
284250, 283mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  t  =  ( F `  A ) )
285 elsn 4046 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  { ( F `
 A ) }  <-> 
t  =  ( F `
 A ) )
286284, 285sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( G " ( -oo (,) A ) ) )  ->  t  e.  {
( F `  A
) } )
287286ex 434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( t  e.  ( G " ( -oo (,) A ) )  -> 
t  e.  { ( F `  A ) } ) )
288287ssrdv 3505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( G " ( -oo (,) A ) ) 
C_  { ( F `
 A ) } )
289288adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( F `  A )  e.  u
)  ->  ( G " ( -oo (,) A
) )  C_  { ( F `  A ) } )
290 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( F `  A )  e.  u
)  ->  ( F `  A )  e.  u
)
291290snssd 4177 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( F `  A )  e.  u
)  ->  { ( F `  A ) }  C_  u )
292289, 291sstrd 3509 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( F `  A )  e.  u
)  ->  ( G " ( -oo (,) A
) )  C_  u
)
293292adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( F `  A )  e.  u )  /\  ( F `  B )  e.  u )  ->  ( G " ( -oo (,) A ) )  C_  u )
294 fvelima 5925 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Fun  G  /\  t  e.  ( G " ( B (,) +oo ) ) )  ->  E. z  e.  ( B (,) +oo ) ( G `  z )  =  t )
295170, 294sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  ->  E. z  e.  ( B (,) +oo ) ( G `  z )  =  t )
296 simp1l 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  /\  z  e.  ( B (,) +oo )  /\  ( G `  z )  =  t )  ->  ph )
297 simp2 997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  /\  z  e.  ( B (,) +oo )  /\  ( G `  z )  =  t )  ->  z  e.  ( B (,) +oo )
)
298 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  /\  z  e.  ( B (,) +oo )  /\  ( G `  z )  =  t )  ->  ( G `  z )  =  t )
29966a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  G  =  ( y  e.  RR  |->  if ( y  e.  ( A [,] B ) ,  ( F `  y ) ,  if ( y  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) ) )
300223adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 ) ) ) )
301 elioore 11584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  e.  ( B (,) +oo )  ->  z  e.  RR )
302301adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  z  e.  RR )
30316ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A [,] B ) )  ->  ( F `  z )  e.  Y
)
304303adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( B (,) +oo ) )  /\  z  e.  ( A [,] B
) )  ->  ( F `  z )  e.  Y )
3054adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  A  e.  RR )
3065adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  B  e.  RR )
30726adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  A  <_  B )
308 elioo3g 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( z  e.  ( B (,) +oo )  <->  ( ( B  e.  RR*  /\ +oo  e.  RR* 
/\  z  e.  RR* )  /\  ( B  < 
z  /\  z  < +oo ) ) )
309308biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( z  e.  ( B (,) +oo )  ->  ( ( B  e.  RR*  /\ +oo  e.  RR*  /\  z  e. 
RR* )  /\  ( B  <  z  /\  z  < +oo ) ) )
310309simprld 31600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( z  e.  ( B (,) +oo )  ->  B  <  z )
311310adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  B  <  z )
312305, 306, 302, 307, 311lelttrd 9757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  A  <  z )
313305, 302, 312ltnsymd 9751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  -.  z  <  A )
314313iffalsed 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  if (
z  <  A , 
( F `  A
) ,  ( F `
 B ) )  =  ( F `  B ) )
315133adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  ( F `  B )  e.  Y
)
316314, 315eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  if (
z  <  A , 
( F `  A
) ,  ( F `
 B ) )  e.  Y )
317316adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( B (,) +oo ) )  /\  -.  z  e.  ( A [,] B ) )  ->  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) )  e.  Y )
318304, 317ifclda 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  if (
z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  e.  Y )
319299, 300, 302, 318fvmptd 5961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  ( G `  z )  =  if ( z  e.  ( A [,] B ) ,  ( F `  z ) ,  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) ) ) )
320319adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( B (,) +oo ) )  /\  ( G `  z )  =  t )  -> 
( G `  z
)  =  if ( z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) ) )
321 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( B (,) +oo ) )  /\  ( G `  z )  =  t )  -> 
( G `  z
)  =  t )
322306, 302ltnled 9749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  ( B  <  z  <->  -.  z  <_  B ) )
323311, 322mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  -.  z  <_  B )
324323intn3an3d 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  -.  (
z  e.  RR  /\  A  <_  z  /\  z  <_  B ) )
325266adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  ( A  e.  RR  /\  B  e.  RR ) )
326325, 268syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  ( z  e.  ( A [,] B
)  <->  ( z  e.  RR  /\  A  <_ 
z  /\  z  <_  B ) ) )
327324, 326mtbird 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  -.  z  e.  ( A [,] B
) )
328327iffalsed 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
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 ) ) )
329328, 314eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  ( B (,) +oo )
)  ->  if (
z  e.  ( A [,] B ) ,  ( F `  z
) ,  if ( z  <  A , 
( F `  A
) ,  ( F `
 B ) ) )  =  ( F `
 B ) )
330329adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( B (,) +oo ) )  /\  ( G `  z )  =  t )  ->  if ( z  e.  ( A [,] B ) ,  ( F `  z ) ,  if ( z  <  A ,  ( F `  A ) ,  ( F `  B ) ) )  =  ( F `  B ) )
331320, 321, 3303eqtr3d 2506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  z  e.  ( B (,) +oo ) )  /\  ( G `  z )  =  t )  -> 
t  =  ( F `
 B ) )
332296, 297, 298, 331syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  /\  z  e.  ( B (,) +oo )  /\  ( G `  z )  =  t )  ->  t  =  ( F `  B ) )
333332rexlimdv3a 2951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  ->  ( E. z  e.  ( B (,) +oo ) ( G `
 z )  =  t  ->  t  =  ( F `  B ) ) )
334295, 333mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  ->  t  =  ( F `  B ) )
335 elsn 4046 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  { ( F `
 B ) }  <-> 
t  =  ( F `
 B ) )
336334, 335sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  ( G " ( B (,) +oo ) ) )  ->  t  e.  { ( F `  B
) } )
337336ex 434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( t  e.  ( G " ( B (,) +oo ) )  ->  t  e.  {
( F `  B
) } ) )
338337ssrdv 3505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( G " ( B (,) +oo ) ) 
C_  { ( F `
 B ) } )
339338adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( F `  B )  e.  u
)  ->  ( G " ( B (,) +oo ) )  C_  { ( F `  B ) } )
340 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( F `  B )  e.  u
)  ->  ( F `  B )  e.  u
)
341340snssd 4177 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( F `  B )  e.  u
)  ->  { ( F `  B ) }  C_  u )
342339, 341sstrd 3509 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( F `  B )  e.  u
)  ->  ( G " ( B (,) +oo ) )  C_  u
)
343342adantlr 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( F `  A )  e.  u )  /\  ( F `  B )  e.  u )  ->  ( G " ( B (,) +oo ) )  C_  u
)
344293, 343unssd 3676 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( F `  A )  e.  u )  /\  ( F `  B )  e.  u )  ->  (
( G " ( -oo (,) A ) )  u.  ( G "
( B (,) +oo ) ) )  C_  u )
345247, 344syl5eqss 3543 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( F `  A )  e.  u )  /\  ( F `  B )  e.  u )  ->  ( G " ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  C_  u )
346163, 167, 168, 345syl21anc 1227 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 )
347246, 346unssd 3676 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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
)
348162, 347syl5eqss 3543 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
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 )
349 eleq2 2530 . . . . . . . . . . . . . . 15  |-  ( v  =  ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( y  e.  v  <->  y  e.  ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) ) )
350 imaeq2 5343 . . . . . . . . . . . . . . . 16  |-  ( v  =  ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( G " v )  =  ( G " ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) ) )
351350sseq1d 3526 . . . . . . . . . . . . . . 15  |-  ( v  =  ( w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  ->  ( ( G " v )  C_  u 
<->  ( G " (
w  u.  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) ) ) 
C_  u ) )
352349, 351anbi12d 710 . . . . . . . . . . . . . 14  |-  ( 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
) ) )
353352rspcev 3210 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
354107, 161, 348, 353syl12anc 1226 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
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
) )
35583a1i 11 . . . . . . . . . . . . . . . 16  |-  ( w  e.  J  ->  J  e.  Top )
356 iooretop 21399 . . . . . . . . . . . . . . . . . 18  |-  ( -oo (,) B )  e.  (
topGen `  ran  (,) )
357356, 1eleqtrri 2544 . . . . . . . . . . . . . . . . 17  |-  ( -oo (,) B )  e.  J
358 inopn 19535 . . . . . . . . . . . . . . . . 17  |-  ( ( J  e.  Top  /\  w  e.  J  /\  ( -oo (,) B )  e.  J )  -> 
( w  i^i  ( -oo (,) B ) )  e.  J )
35983, 357, 358mp3an13 1315 . . . . . . . . . . . . . . . 16  |-  ( w  e.  J  ->  (
w  i^i  ( -oo (,) B ) )  e.  J )
360100a1i 11 . . . . . . . . . . . . . . . 16  |-  ( w  e.  J  ->  ( -oo (,) A )  e.  J )
361 unopn 19539 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  ( w  i^i  ( -oo (,) B ) )  e.  J  /\  ( -oo (,) A )  e.  J )  ->  (
( w  i^i  ( -oo (,) B ) )  u.  ( -oo (,) A ) )  e.  J )
362355, 359, 360, 361syl3anc 1228 . . . . . . . . . . . . . . 15  |-  ( w  e.  J  ->  (
( w  i^i  ( -oo (,) B ) )  u.  ( -oo (,) A ) )  e.  J )
3633623ad2ant2 1018 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
)
364363ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
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
)
365 simpll1 1035 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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
) )
366 simpll3 1037 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 ) ) )
367 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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
)
368 simpll 753 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 ) ) ) )
369266ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  ( F `
 B )  e.  u )  ->  ( A  e.  RR  /\  B  e.  RR ) )
370 eqimss 3551 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( RR  \  ( A [,] B ) )  =  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  ->  ( RR  \ 
( A [,] B
) )  C_  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )
371113, 370syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( RR  \  ( A [,] B ) ) 
C_  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )
372 difcom 3915 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  \  ( A [,] B ) ) 
C_  ( ( -oo (,) A )  u.  ( B (,) +oo ) )  <-> 
( RR  \  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )  C_  ( A [,] B ) )
373371, 372sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( RR  \  (
( -oo (,) A )  u.  ( B (,) +oo ) ) )  C_  ( A [,] B ) )
374369, 373syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y
)  e.  u )  /\  -.  ( F `
 B )  e.  u )  ->  ( RR  \  ( ( -oo (,) A )  u.  ( B (,) +oo ) ) )  C_  ( A [,] B ) )
375374adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 ) )
376 simp-4r 768 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y )  e.  u
)  /\  -.  ( F `  B )  e.  u )  /\  -.  y  e.  ( -oo (,) A ) )  -> 
y  e.  RR )
377 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  ( G `  y )  e.  u
)  /\  -.  ( F `  B )  e.  u )  /\  -.  y  e.  ( -oo (,) A ) )  ->  -.  y  e.  ( -oo (,) A ) )
378 elioore 11584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  e.  ( B (,) +oo )  ->  y  e.  RR )
379378adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  y  e.  RR )
380 elioo3g 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( y  e.  ( B (,) +oo )  <->  ( ( B  e.  RR*  /\ +oo  e.  RR* 
/\  y  e.  RR* )  /\  ( B  < 
y  /\  y  < +oo ) ) )
381380biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y  e.  ( B (,) +oo )  ->  ( ( B  e.  RR*  /\ +oo  e.  RR*  /\  y  e. 
RR* )  /\  ( B  <  y  /\  y  < +oo ) ) )
382381simprld 31600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  e.  ( B (,) +oo )  ->  B  <  y )
383382adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  B  <  y )
3845adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  B  e.  RR )
385384, 379ltnled 9749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  ( B  <  y  <->  -.  y  <_  B ) )
386383, 385mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  -.  y  <_  B )
387386intn3an3d 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  -.  (
y  e.  RR  /\  A  <_  y  /\  y  <_  B ) )
388266adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  ( A  e.  RR  /\  B  e.  RR ) )
389 elicc2 11614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( y  e.  ( A [,] B )  <-> 
( y  e.  RR  /\  A  <_  y  /\  y  <_  B ) ) )
390388, 389syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  ( y  e.  ( A [,] B
)  <->  ( y  e.  RR  /\  A  <_ 
y  /\  y  <_  B ) ) )
391387, 390mtbird 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  y  e.  ( B (,) +oo )
)  ->  -.  y  e.  ( A [,] B
) )
392391iffalsed 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
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 `