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

Theorem cncfiooicclem1 31555
Description: A continuous function  F on an open interval  ( A (,) B ) can be extended to a continuous function  G on the corresponding close interval, if it has a finite right limit  R in  A and a finite left limit  L in  B.  F can be complex valued. This lemma assumes  A  <  B, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
cncfiooicclem1.x  |-  F/ x ph
cncfiooicclem1.g  |-  G  =  ( x  e.  ( A [,] B ) 
|->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )
cncfiooicclem1.a  |-  ( ph  ->  A  e.  RR )
cncfiooicclem1.b  |-  ( ph  ->  B  e.  RR )
cncfiooicclem1.altb  |-  ( ph  ->  A  <  B )
cncfiooicclem1.f  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
cncfiooicclem1.l  |-  ( ph  ->  L  e.  ( F lim
CC  B ) )
cncfiooicclem1.r  |-  ( ph  ->  R  e.  ( F lim
CC  A ) )
Assertion
Ref Expression
cncfiooicclem1  |-  ( ph  ->  G  e.  ( ( A [,] B )
-cn-> CC ) )
Distinct variable groups:    x, A    x, B    x, F    x, L    x, R
Allowed substitution hints:    ph( x)    G( x)

Proof of Theorem cncfiooicclem1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 cncfiooicclem1.x . . . . . 6  |-  F/ x ph
2 limccl 22147 . . . . . . . . . 10  |-  ( F lim
CC  A )  C_  CC
3 cncfiooicclem1.r . . . . . . . . . 10  |-  ( ph  ->  R  e.  ( F lim
CC  A ) )
42, 3sseldi 3507 . . . . . . . . 9  |-  ( ph  ->  R  e.  CC )
54ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( A [,] B
) )  /\  x  =  A )  ->  R  e.  CC )
6 limccl 22147 . . . . . . . . . . 11  |-  ( F lim
CC  B )  C_  CC
7 cncfiooicclem1.l . . . . . . . . . . 11  |-  ( ph  ->  L  e.  ( F lim
CC  B ) )
86, 7sseldi 3507 . . . . . . . . . 10  |-  ( ph  ->  L  e.  CC )
98ad3antrrr 729 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  x  =  B )  ->  L  e.  CC )
10 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  ph )
11 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  -.  x  =  A )
12 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  -.  x  =  B )
1311, 12jca 532 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  ( -.  x  =  A  /\  -.  x  =  B ) )
14 orel1 382 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  A  -> 
( ( x  =  A  \/  x  =  B )  ->  x  =  B ) )
1514con3dimp 441 . . . . . . . . . . . . . 14  |-  ( ( -.  x  =  A  /\  -.  x  =  B )  ->  -.  ( x  =  A  \/  x  =  B
) )
16 vex 3121 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
1716elpr 4051 . . . . . . . . . . . . . 14  |-  ( x  e.  { A ,  B }  <->  ( x  =  A  \/  x  =  B ) )
1815, 17sylnibr 305 . . . . . . . . . . . . 13  |-  ( ( -.  x  =  A  /\  -.  x  =  B )  ->  -.  x  e.  { A ,  B } )
1913, 18syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  -.  x  e.  { A ,  B } )
20 simpllr 758 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  x  e.  ( A [,] B
) )
21 cncfiooicclem1.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR )
2221rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR* )
2310, 22syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  A  e.  RR* )
24 cncfiooicclem1.b . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  RR )
2524rexrd 9655 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR* )
2610, 25syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  B  e.  RR* )
27 cncfiooicclem1.altb . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  <  B )
2822, 25jca 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR* )
)
29 xrltle 11367 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  ->  A  <_  B ) )
3028, 29syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  <  B  ->  A  <_  B )
)
3127, 30mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  <_  B )
3210, 31syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  A  <_  B )
3323, 26, 323jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B ) )
34 prunioo 11661 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  (
( A (,) B
)  u.  { A ,  B } )  =  ( A [,] B
) )
3533, 34syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  (
( A (,) B
)  u.  { A ,  B } )  =  ( A [,] B
) )
3635eqcomd 2475 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  ( A [,] B )  =  ( ( A (,) B )  u.  { A ,  B }
) )
3720, 36eleqtrd 2557 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  x  e.  ( ( A (,) B )  u.  { A ,  B }
) )
38 elun 3650 . . . . . . . . . . . . 13  |-  ( x  e.  ( ( A (,) B )  u. 
{ A ,  B } )  <->  ( x  e.  ( A (,) B
)  \/  x  e. 
{ A ,  B } ) )
3937, 38sylib 196 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  (
x  e.  ( A (,) B )  \/  x  e.  { A ,  B } ) )
40 orel2 383 . . . . . . . . . . . 12  |-  ( -.  x  e.  { A ,  B }  ->  (
( x  e.  ( A (,) B )  \/  x  e.  { A ,  B }
)  ->  x  e.  ( A (,) B ) ) )
4119, 39, 40sylc 60 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  x  e.  ( A (,) B
) )
4210, 41jca 532 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  ( ph  /\  x  e.  ( A (,) B ) ) )
43 cncfiooicclem1.f . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
44 cncff 21265 . . . . . . . . . . . 12  |-  ( F  e.  ( ( A (,) B ) -cn-> CC )  ->  F :
( A (,) B
) --> CC )
4543, 44syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F : ( A (,) B ) --> CC )
4645ffvelrnda 6032 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( F `  x )  e.  CC )
4742, 46syl 16 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( A [,] B ) )  /\  -.  x  =  A
)  /\  -.  x  =  B )  ->  ( F `  x )  e.  CC )
489, 47ifclda 3977 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( A [,] B
) )  /\  -.  x  =  A )  ->  if ( x  =  B ,  L , 
( F `  x
) )  e.  CC )
495, 48ifclda 3977 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A [,] B ) )  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  e.  CC )
5049ex 434 . . . . . 6  |-  ( ph  ->  ( x  e.  ( A [,] B )  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) )  e.  CC ) )
511, 50ralrimi 2867 . . . . 5  |-  ( ph  ->  A. x  e.  ( A [,] B ) if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) )  e.  CC )
52 cncfiooicclem1.g . . . . . 6  |-  G  =  ( x  e.  ( A [,] B ) 
|->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )
5352fmpt 6053 . . . . 5  |-  ( A. x  e.  ( A [,] B ) if ( x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  e.  CC  <->  G :
( A [,] B
) --> CC )
5451, 53sylib 196 . . . 4  |-  ( ph  ->  G : ( A [,] B ) --> CC )
55 simpl 457 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ph )
56 elun 3650 . . . . . . . . . 10  |-  ( y  e.  ( ( A (,) B )  u. 
{ A ,  B } )  <->  ( y  e.  ( A (,) B
)  \/  y  e. 
{ A ,  B } ) )
5722, 25, 313jca 1176 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B ) )
5857, 34syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A (,) B )  u.  { A ,  B }
)  =  ( A [,] B ) )
5958eleq2d 2537 . . . . . . . . . 10  |-  ( ph  ->  ( y  e.  ( ( A (,) B
)  u.  { A ,  B } )  <->  y  e.  ( A [,] B ) ) )
6056, 59syl5bbr 259 . . . . . . . . 9  |-  ( ph  ->  ( ( y  e.  ( A (,) B
)  \/  y  e. 
{ A ,  B } )  <->  y  e.  ( A [,] B ) ) )
6160biimprd 223 . . . . . . . 8  |-  ( ph  ->  ( y  e.  ( A [,] B )  ->  ( y  e.  ( A (,) B
)  \/  y  e. 
{ A ,  B } ) ) )
6261imp 429 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( y  e.  ( A (,) B
)  \/  y  e. 
{ A ,  B } ) )
6355, 62jca 532 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A [,] B ) )  ->  ( ph  /\  ( y  e.  ( A (,) B )  \/  y  e.  { A ,  B }
) ) )
64 ioossicc 11622 . . . . . . . . . . . . . . . . . 18  |-  ( A (,) B )  C_  ( A [,] B )
6564a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A (,) B
)  C_  ( A [,] B ) )
6654, 65jca 532 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( G : ( A [,] B ) --> CC  /\  ( A (,) B )  C_  ( A [,] B ) ) )
67 fssres 5757 . . . . . . . . . . . . . . . 16  |-  ( ( G : ( A [,] B ) --> CC 
/\  ( A (,) B )  C_  ( A [,] B ) )  ->  ( G  |`  ( A (,) B ) ) : ( A (,) B ) --> CC )
6866, 67syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G  |`  ( A (,) B ) ) : ( A (,) B ) --> CC )
6968feqmptd 5927 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  =  ( y  e.  ( A (,) B
)  |->  ( ( G  |`  ( A (,) B
) ) `  y
) ) )
70 nfmpt1 4542 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( x  e.  ( A [,] B ) 
|->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )
7152, 70nfcxfr 2627 . . . . . . . . . . . . . . . . . 18  |-  F/_ x G
72 nfcv 2629 . . . . . . . . . . . . . . . . . 18  |-  F/_ x
( A (,) B
)
7371, 72nfres 5281 . . . . . . . . . . . . . . . . 17  |-  F/_ x
( G  |`  ( A (,) B ) )
74 nfcv 2629 . . . . . . . . . . . . . . . . 17  |-  F/_ x
y
7573, 74nffv 5879 . . . . . . . . . . . . . . . 16  |-  F/_ x
( ( G  |`  ( A (,) B ) ) `  y )
76 nfcv 2629 . . . . . . . . . . . . . . . . 17  |-  F/_ y
( G  |`  ( A (,) B ) )
77 nfcv 2629 . . . . . . . . . . . . . . . . 17  |-  F/_ y
x
7876, 77nffv 5879 . . . . . . . . . . . . . . . 16  |-  F/_ y
( ( G  |`  ( A (,) B ) ) `  x )
79 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  (
( G  |`  ( A (,) B ) ) `
 y )  =  ( ( G  |`  ( A (,) B ) ) `  x ) )
8075, 78, 79cbvmpt 4543 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( A (,) B )  |->  ( ( G  |`  ( A (,) B ) ) `  y ) )  =  ( x  e.  ( A (,) B ) 
|->  ( ( G  |`  ( A (,) B ) ) `  x ) )
8180a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  e.  ( A (,) B ) 
|->  ( ( G  |`  ( A (,) B ) ) `  y ) )  =  ( x  e.  ( A (,) B )  |->  ( ( G  |`  ( A (,) B ) ) `  x ) ) )
82 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  x  e.  ( A (,) B ) )
83 fvres 5886 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A (,) B )  ->  (
( G  |`  ( A (,) B ) ) `
 x )  =  ( G `  x
) )
8482, 83syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( G  |`  ( A (,) B ) ) `  x )  =  ( G `  x ) )
8564, 82sseldi 3507 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  x  e.  ( A [,] B ) )
864idi 2 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  R  e.  CC )
8786adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  R  e.  CC )
888adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  =  B )  ->  L  e.  CC )
8988adantlr 714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( A (,) B
) )  /\  x  =  B )  ->  L  e.  CC )
9045adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  F :
( A (,) B
) --> CC )
9190, 82ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( F `  x )  e.  CC )
9291adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( A (,) B
) )  /\  -.  x  =  B )  ->  ( F `  x
)  e.  CC )
9389, 92ifclda 3977 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  if (
x  =  B ,  L ,  ( F `  x ) )  e.  CC )
9487, 93jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( R  e.  CC  /\  if ( x  =  B ,  L ,  ( F `  x ) )  e.  CC ) )
95 ifcl 3987 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  CC  /\  if ( x  =  B ,  L ,  ( F `  x ) )  e.  CC )  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) )  e.  CC )
9694, 95syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  e.  CC )
9785, 96jca 532 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( x  e.  ( A [,] B
)  /\  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  e.  CC ) )
9852fvmpt2 5964 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( A [,] B )  /\  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) )  e.  CC )  ->  ( G `  x )  =  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) ) )
9997, 98syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( G `  x )  =  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) ) )
100 elioo4g 11597 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  ( A (,) B )  <->  ( ( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  RR )  /\  ( A  <  x  /\  x  <  B ) ) )
101100biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  ( A (,) B )  ->  (
( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  RR )  /\  ( A  <  x  /\  x  <  B ) ) )
102101simpld 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( A (,) B )  ->  ( A  e.  RR*  /\  B  e.  RR*  /\  x  e.  RR ) )
103102simp1d 1008 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  ->  A  e.  RR* )
104102simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( A (,) B )  ->  x  e.  RR )
105104rexrd 9655 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  ->  x  e.  RR* )
106101simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( A (,) B )  ->  ( A  <  x  /\  x  <  B ) )
107106simpld 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  ->  A  <  x )
108103, 105, 1073jca 1176 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A (,) B )  ->  ( A  e.  RR*  /\  x  e.  RR*  /\  A  < 
x ) )
109 xrltne 11378 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  RR*  /\  x  e.  RR*  /\  A  < 
x )  ->  x  =/=  A )
110108, 109syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A (,) B )  ->  x  =/=  A )
111110adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  x  =/=  A )
112111neneqd 2669 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  -.  x  =  A )
113 iffalse 3954 . . . . . . . . . . . . . . . . . 18  |-  ( -.  x  =  A  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) )  =  if ( x  =  B ,  L ,  ( F `  x ) ) )
114112, 113syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  =  if ( x  =  B ,  L ,  ( F `  x ) ) )
115102simp2d 1009 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( A (,) B )  ->  B  e.  RR* )
116106simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( A (,) B )  ->  x  <  B )
117105, 115, 1163jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  ->  (
x  e.  RR*  /\  B  e.  RR*  /\  x  < 
B ) )
118 xrltne 11378 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR*  /\  B  e.  RR*  /\  x  < 
B )  ->  B  =/=  x )
119117, 118syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( A (,) B )  ->  B  =/=  x )
120119necomd 2738 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( A (,) B )  ->  x  =/=  B )
121120neneqd 2669 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( A (,) B )  ->  -.  x  =  B )
122 iffalse 3954 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  x  =  B  ->  if ( x  =  B ,  L ,  ( F `  x ) )  =  ( F `
 x ) )
123121, 122syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A (,) B )  ->  if ( x  =  B ,  L ,  ( F `
 x ) )  =  ( F `  x ) )
124123adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  if (
x  =  B ,  L ,  ( F `  x ) )  =  ( F `  x
) )
125114, 124eqtrd 2508 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  =  ( F `  x ) )
12684, 99, 1253eqtrd 2512 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( G  |`  ( A (,) B ) ) `  x )  =  ( F `  x ) )
1271, 126mpteq2da 4538 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( ( G  |`  ( A (,) B ) ) `  x ) )  =  ( x  e.  ( A (,) B )  |->  ( F `
 x ) ) )
12869, 81, 1273eqtrd 2512 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  =  ( x  e.  ( A (,) B
)  |->  ( F `  x ) ) )
129 ffn 5737 . . . . . . . . . . . . . . . . . 18  |-  ( F : ( A (,) B ) --> CC  ->  F  Fn  ( A (,) B ) )
13045, 129syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F  Fn  ( A (,) B ) )
131 dffn5 5919 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  ( A (,) B )  <->  F  =  ( x  e.  ( A (,) B )  |->  ( F `  x ) ) )
132130, 131sylib 196 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F  =  ( x  e.  ( A (,) B )  |->  ( F `
 x ) ) )
133132eqcomd 2475 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( F `  x
) )  =  F )
134133, 43eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( F `  x
) )  e.  ( ( A (,) B
) -cn-> CC ) )
135 ioossre 11598 . . . . . . . . . . . . . . . . 17  |-  ( A (,) B )  C_  RR
136 ax-resscn 9561 . . . . . . . . . . . . . . . . 17  |-  RR  C_  CC
137135, 136sstri 3518 . . . . . . . . . . . . . . . 16  |-  ( A (,) B )  C_  CC
138137a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A (,) B
)  C_  CC )
139 ssid 3528 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
140139a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  C_  CC )
141 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
142 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( (
TopOpen ` fld )t  ( A (,) B
) )  =  ( ( TopOpen ` fld )t  ( A (,) B ) )
143141cnfldtop 21159 . . . . . . . . . . . . . . . . . 18  |-  ( TopOpen ` fld )  e.  Top
144 unicntop 31336 . . . . . . . . . . . . . . . . . . 19  |-  CC  =  U. ( TopOpen ` fld )
145144restid 14706 . . . . . . . . . . . . . . . . . 18  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
146143, 145ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
147146eqcomi 2480 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
148141, 142, 147cncfcn 21281 . . . . . . . . . . . . . . 15  |-  ( ( ( A (,) B
)  C_  CC  /\  CC  C_  CC )  ->  (
( A (,) B
) -cn-> CC )  =  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
149138, 140, 148syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A (,) B ) -cn-> CC )  =  ( ( (
TopOpen ` fld )t  ( A (,) B
) )  Cn  ( TopOpen
` fld
) ) )
150134, 149eleqtrd 2557 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  ( A (,) B ) 
|->  ( F `  x
) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
151128, 150eqeltrd 2555 . . . . . . . . . . . 12  |-  ( ph  ->  ( G  |`  ( A (,) B ) )  e.  ( ( (
TopOpen ` fld )t  ( A (,) B
) )  Cn  ( TopOpen
` fld
) ) )
152151adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( G  |`  ( A (,) B
) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) ) )
153 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( A (,) B ) )
154152, 153jca 532 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( G  |`  ( A (,) B ) )  e.  ( ( ( TopOpen ` fld )t  ( A (,) B ) )  Cn  ( TopOpen ` fld ) )  /\  y  e.  ( A (,) B
) ) )
155143, 137pm3.2i 455 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )  e.  Top  /\  ( A (,) B ) 
C_  CC )
156141cnfldtopon 21158 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
157156toponunii 19302 . . . . . . . . . . . . 13  |-  CC  =  U. ( TopOpen ` fld )
158157restuni 19531 . . . . . . . . . . . 12  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( A (,) B
)  C_  CC )  ->  ( A (,) B
)  =  U. (
( TopOpen ` fld )t  ( A (,) B ) ) )
159155, 158ax-mp 5 . . . . . . . . . . 11  |-  ( A (,) B )  = 
U. ( ( TopOpen ` fld )t  ( A (,) B ) )
160159cncnpi 19647 . . . . . . . . . 10  |-  ( ( ( G  |`  ( A (,) B ) )  e.  ( ( (
TopOpen ` fld )t  ( A (,) B
) )  Cn  ( TopOpen
` fld
) )  /\  y  e.  ( A (,) B
) )  ->  ( G  |`  ( A (,) B ) )  e.  ( ( ( (
TopOpen ` fld )t  ( A (,) B
) )  CnP  ( TopOpen
` fld
) ) `  y
) )
161154, 160syl 16 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( G  |`  ( A (,) B
) )  e.  ( ( ( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
) )
162143a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( TopOpen ` fld )  e.  Top )
16364a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( A (,) B )  C_  ( A [,] B ) )
164 ovex 6320 . . . . . . . . . . . . . . 15  |-  ( A [,] B )  e. 
_V
165164a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( A [,] B )  e.  _V )
166162, 163, 1653jca 1176 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( TopOpen
` fld
)  e.  Top  /\  ( A (,) B ) 
C_  ( A [,] B )  /\  ( A [,] B )  e. 
_V ) )
167 restabs 19534 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( A (,) B
)  C_  ( A [,] B )  /\  ( A [,] B )  e. 
_V )  ->  (
( ( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) )  =  ( ( TopOpen ` fld )t  ( A (,) B ) ) )
168166, 167syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( (
( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) )  =  ( ( TopOpen ` fld )t  ( A (,) B ) ) )
169168eqcomd 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( TopOpen
` fld
)t  ( A (,) B
) )  =  ( ( ( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) ) )
170169oveq1d 6310 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( (
( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) )  =  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) )  CnP  ( TopOpen ` fld )
) )
171170fveq1d 5874 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( (
( ( TopOpen ` fld )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
)  =  ( ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) )  CnP  ( TopOpen ` fld )
) `  y )
)
172161, 171eleqtrd 2557 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( G  |`  ( A (,) B
) )  e.  ( ( ( ( (
TopOpen ` fld )t  ( A [,] B
) )t  ( A (,) B ) )  CnP  ( TopOpen ` fld ) ) `  y
) )
173143, 164pm3.2i 455 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )  e.  Top  /\  ( A [,] B )  e.  _V )
174 resttop 19529 . . . . . . . . . . . 12  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( A [,] B
)  e.  _V )  ->  ( ( TopOpen ` fld )t  ( A [,] B ) )  e. 
Top )
175173, 174ax-mp 5 . . . . . . . . . . 11  |-  ( (
TopOpen ` fld )t  ( A [,] B
) )  e.  Top
176175a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( TopOpen
` fld
)t  ( A [,] B
) )  e.  Top )
177143a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( TopOpen ` fld )  e.  Top )
17821, 24jca 532 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR ) )
179 iccssre 11618 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
180178, 179syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A [,] B
)  C_  RR )
181136a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  CC )
182180, 181sstrd 3519 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A [,] B
)  C_  CC )
183177, 182jca 532 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( TopOpen ` fld )  e.  Top  /\  ( A [,] B
)  C_  CC )
)
184157restuni 19531 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( A [,] B
)  C_  CC )  ->  ( A [,] B
)  =  U. (
( TopOpen ` fld )t  ( A [,] B ) ) )
185183, 184syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( A [,] B
)  =  U. (
( TopOpen ` fld )t  ( A [,] B ) ) )
18665, 185sseqtrd 3545 . . . . . . . . . . 11  |-  ( ph  ->  ( A (,) B
)  C_  U. (
( TopOpen ` fld )t  ( A [,] B ) ) )
187186adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( A (,) B )  C_  U. (
( TopOpen ` fld )t  ( A [,] B ) ) )
188 retop 21136 . . . . . . . . . . . . . . . . . . 19  |-  ( topGen ` 
ran  (,) )  e.  Top
189188a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( topGen ` 
ran  (,) )  e.  Top )
190 difss 3636 . . . . . . . . . . . . . . . . . . . . 21  |-  ( RR 
\  ( A [,] B ) )  C_  RR
191135, 190pm3.2i 455 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A (,) B ) 
C_  RR  /\  ( RR  \  ( A [,] B ) )  C_  RR )
192 unss 3683 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A (,) B
)  C_  RR  /\  ( RR  \  ( A [,] B ) )  C_  RR )  <->  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) )  C_  RR )
193191, 192mpbi 208 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A (,) B )  u.  ( RR  \ 
( A [,] B
) ) )  C_  RR
194193a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) )  C_  RR )
195 ssun1 3672 . . . . . . . . . . . . . . . . . . 19  |-  ( A (,) B )  C_  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) )
196195a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( A (,) B )  C_  (
( A (,) B
)  u.  ( RR 
\  ( A [,] B ) ) ) )
197189, 194, 1963jca 1176 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( topGen `
 ran  (,) )  e.  Top  /\  ( ( A (,) B )  u.  ( RR  \ 
( A [,] B
) ) )  C_  RR  /\  ( A (,) B )  C_  (
( A (,) B
)  u.  ( RR 
\  ( A [,] B ) ) ) ) )
198 uniretop 21137 . . . . . . . . . . . . . . . . . 18  |-  RR  =  U. ( topGen `  ran  (,) )
199198ntrss 19424 . . . . . . . . . . . . . . . . 17  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( A (,) B )  u.  ( RR  \ 
( A [,] B
) ) )  C_  RR  /\  ( A (,) B )  C_  (
( A (,) B
)  u.  ( RR 
\  ( A [,] B ) ) ) )  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A (,) B ) ) 
C_  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
200197, 199syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A (,) B ) ) 
C_  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
201 isopn3i 19451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A (,) B ) )  =  ( A (,) B ) )
202 iooretop 21141 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A (,) B )  e.  ( topGen `  ran  (,) )
203188a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( topGen ` 
ran  (,) )  e.  Top  /\  ( A (,) B
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) )  =  ( A (,) B
) )  /\  ( A (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( topGen ` 
ran  (,) )  e.  Top )
204202a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( topGen ` 
ran  (,) )  e.  Top  /\  ( A (,) B
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) )  =  ( A (,) B
) )  /\  ( A (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( A (,) B )  e.  (
topGen `  ran  (,) )
)
205203, 204jca 532 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( topGen ` 
ran  (,) )  e.  Top  /\  ( A (,) B
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) )  =  ( A (,) B
) )  /\  ( A (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( topGen `
 ran  (,) )  e.  Top  /\  ( A (,) B )  e.  ( topGen `  ran  (,) )
) )
206205, 201syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( topGen ` 
ran  (,) )  e.  Top  /\  ( A (,) B
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) )  =  ( A (,) B
) )  /\  ( A (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A (,) B ) )  =  ( A (,) B ) )
207201, 202, 206mp2an 672 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A (,) B ) )  =  ( A (,) B )
208207eqcomi 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( A (,) B )  =  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) )
209208a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A (,) B
)  =  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A (,) B ) ) )
210209adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( A (,) B )  =  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) ) )
211153, 210eleqtrd 2557 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) B ) ) )
212200, 211sseldd 3510 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
21364, 153sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( A [,] B ) )
214212, 213jca 532 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( y  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  /\  y  e.  ( A [,] B
) ) )
215 elin 3692 . . . . . . . . . . . . . 14  |-  ( y  e.  ( ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) )  <-> 
( y  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  /\  y  e.  ( A [,] B
) ) )
216214, 215sylibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( ( ( int `  ( topGen `  ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) ) )
217180adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( A [,] B )  C_  RR )
218189, 217, 1633jca 1176 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( topGen `
 ran  (,) )  e.  Top  /\  ( A [,] B )  C_  RR  /\  ( A (,) B )  C_  ( A [,] B ) ) )
219 eqid 2467 . . . . . . . . . . . . . . . 16  |-  ( (
topGen `  ran  (,) )t  ( A [,] B ) )  =  ( ( topGen ` 
ran  (,) )t  ( A [,] B ) )
220198, 219restntr 19551 . . . . . . . . . . . . . . 15  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B )  C_  RR  /\  ( A (,) B )  C_  ( A [,] B ) )  ->  ( ( int `  ( ( topGen `  ran  (,) )t  ( A [,] B
) ) ) `  ( A (,) B ) )  =  ( ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) ) )
221218, 220syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( int `  ( ( topGen ` 
ran  (,) )t  ( A [,] B ) ) ) `
 ( A (,) B ) )  =  ( ( ( int `  ( topGen `  ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) ) )
222221eqcomd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( (
( int `  ( topGen `
 ran  (,) )
) `  ( ( A (,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) )  =  ( ( int `  ( ( topGen `  ran  (,) )t  ( A [,] B
) ) ) `  ( A (,) B ) ) )
223216, 222eleqtrd 2557 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( ( int `  (
( topGen `  ran  (,) )t  ( A [,] B ) ) ) `  ( A (,) B ) ) )
224141tgioo2 21176 . . . . . . . . . . . . . . . . . 18  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
225224a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( topGen `  ran  (,) )  =  ( ( TopOpen ` fld )t  RR ) )
226225oveq1d 6310 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( topGen `  ran  (,) )t  ( A [,] B
) )  =  ( ( ( TopOpen ` fld )t  RR )t  ( A [,] B ) ) )
227 reex 9595 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  _V
228227a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  RR  e.  _V )
229177, 180, 2283jca 1176 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( TopOpen ` fld )  e.  Top  /\  ( A [,] B
)  C_  RR  /\  RR  e.  _V ) )
230 restabs 19534 . . . . . . . . . . . . . . . . 17  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  ( A [,] B
)  C_  RR  /\  RR  e.  _V )  ->  (
( ( TopOpen ` fld )t  RR )t  ( A [,] B ) )  =  ( ( TopOpen ` fld )t  ( A [,] B ) ) )
231229, 230syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( TopOpen ` fld )t  RR )t  ( A [,] B ) )  =  ( (
TopOpen ` fld )t  ( A [,] B
) ) )
232226, 231eqtrd 2508 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( topGen `  ran  (,) )t  ( A [,] B
) )  =  ( ( TopOpen ` fld )t  ( A [,] B ) ) )
233232fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( int `  (
( topGen `  ran  (,) )t  ( A [,] B ) ) )  =  ( int `  ( ( TopOpen ` fld )t  ( A [,] B ) ) ) )
234233fveq1d 5874 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( int `  (
( topGen `  ran  (,) )t  ( A [,] B ) ) ) `  ( A (,) B ) )  =  ( ( int `  ( ( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A (,) B ) ) )
235234adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( ( int `  ( ( topGen ` 
ran  (,) )t  ( A [,] B ) ) ) `
 ( A (,) B ) )  =  ( ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A (,) B ) ) )
236223, 235eleqtrd 2557 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  y  e.  ( ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A (,) B ) ) )
237185feq2d 5724 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G : ( A [,] B ) --> CC  <->  G : U. (
( TopOpen ` fld )t  ( A [,] B ) ) --> CC ) )
23854, 237mpbid 210 . . . . . . . . . . . 12  |-  ( ph  ->  G : U. (
( TopOpen ` fld )t  ( A [,] B ) ) --> CC )
239238adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  G : U. ( ( TopOpen ` fld )t  ( A [,] B ) ) --> CC )
240236, 239jca 532 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( y  e.  ( ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A (,) B ) )  /\  G : U. ( (
TopOpen ` fld )t  ( A [,] B
) ) --> CC ) )
241176, 187, 240jca31 534 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( (
( ( TopOpen ` fld )t  ( A [,] B ) )  e. 
Top  /\  ( A (,) B )  C_  U. (
( TopOpen ` fld )t  ( A [,] B ) ) )  /\  ( y  e.  ( ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A (,) B ) )  /\  G : U. ( (
TopOpen ` fld )t  ( A [,] B
) ) --> CC ) ) )
242 eqid 2467 . . . . . . . . . 10  |-  U. (
( TopOpen ` fld )t  ( A [,] B ) )  = 
U. ( ( TopOpen ` fld )t  ( A [,] B ) )
243242, 157cnprest 19658 . . . . . . . . 9  |-  ( ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  e.  Top  /\  ( A (,) B )  C_  U. ( ( TopOpen ` fld )t  ( A [,] B ) ) )  /\  ( y  e.  ( ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A (,) B ) )  /\  G : U. ( (
TopOpen ` fld )t  ( A [,] B
) ) --> CC ) )  ->  ( G  e.  ( ( ( (
TopOpen ` fld )t  ( A [,] B
) )  CnP  ( TopOpen
` fld
) ) `  y
)  <->  ( G  |`  ( A (,) B ) )  e.  ( ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) )  CnP  ( TopOpen ` fld )
) `  y )
) )
244241, 243syl 16 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  ( G  e.  ( ( ( (
TopOpen ` fld )t  ( A [,] B
) )  CnP  ( TopOpen
` fld
) ) `  y
)  <->  ( G  |`  ( A (,) B ) )  e.  ( ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )t  ( A (,) B ) )  CnP  ( TopOpen ` fld )
) `  y )
) )
245172, 244mpbird 232 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A (,) B ) )  ->  G  e.  ( ( ( (
TopOpen ` fld )t  ( A [,] B
) )  CnP  ( TopOpen
` fld
) ) `  y
) )
246 elpri 4053 . . . . . . . . . 10  |-  ( y  e.  { A ,  B }  ->  ( y  =  A  \/  y  =  B ) )
247246a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  { A ,  B }  ->  ( y  =  A  \/  y  =  B ) ) )
248247imdistani 690 . . . . . . . 8  |-  ( (
ph  /\  y  e.  { A ,  B }
)  ->  ( ph  /\  ( y  =  A  \/  y  =  B ) ) )
249 lbicc2 11648 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  A  e.  ( A [,] B
) )
25057, 249syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  ( A [,] B ) )
251250, 3jca 532 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  e.  ( A [,] B )  /\  R  e.  ( F lim CC  A ) ) )
252 iftrue 3951 . . . . . . . . . . . . . . . . 17  |-  ( x  =  A  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) )  =  R )
25352idi 2 . . . . . . . . . . . . . . . . 17  |-  G  =  ( x  e.  ( A [,] B ) 
|->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )
254252, 253fvmptg 5955 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( A [,] B )  /\  R  e.  ( F lim CC  A ) )  -> 
( G `  A
)  =  R )
255251, 254syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  A
)  =  R )
256128, 133eqtr2d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F  =  ( G  |`  ( A (,) B
) ) )
257256oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F lim CC  A
)  =  ( ( G  |`  ( A (,) B ) ) lim CC  A ) )
2583, 257eleqtrd 2557 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  R  e.  ( ( G  |`  ( A (,) B ) ) lim CC  A ) )
259 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( (
TopOpen ` fld )t  ( ( A [,] B )  u.  { A } ) )  =  ( ( TopOpen ` fld )t  ( ( A [,] B )  u. 
{ A } ) )
260 mnfxr 11335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |- -oo  e.  RR*
261260a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  -> -oo  e.  RR* )
262261, 25, 223jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( -oo  e.  RR*  /\  B  e.  RR*  /\  A  e.  RR* ) )
263 mnflt 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  e.  RR  -> -oo  <  A )
26421, 263syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  -> -oo  <  A )
265264, 27jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( -oo  <  A  /\  A  <  B ) )
266262, 265jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( -oo  e.  RR* 
/\  B  e.  RR*  /\  A  e.  RR* )  /\  ( -oo  <  A  /\  A  <  B ) ) )
267 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  e.  ( -oo (,) B )  <->  ( ( -oo  e.  RR*  /\  B  e. 
RR*  /\  A  e.  RR* )  /\  ( -oo  <  A  /\  A  < 
B ) ) )
268266, 267sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A  e.  ( -oo (,) B ) )
269188a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( topGen `  ran  (,) )  e.  Top )
270 iooretop 21141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( -oo (,) B )  e.  (
topGen `  ran  (,) )
271270a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( -oo (,) B
)  e.  ( topGen ` 
ran  (,) ) )
272269, 271jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( topGen `  ran  (,) )  e.  Top  /\  ( -oo (,) B )  e.  ( topGen `  ran  (,) ) ) )
273 isopn3i 19451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( -oo (,) B )  e.  (
topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( -oo (,) B ) )  =  ( -oo (,) B ) )
274272, 273syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( -oo (,) B ) )  =  ( -oo (,) B
) )
275274eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( -oo (,) B
)  =  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -oo (,) B ) ) )
276268, 275eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  e.  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( -oo (,) B ) ) )
27721, 25jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( A  e.  RR  /\  B  e.  RR* )
)
278 icossre 11617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  RR  /\  B  e.  RR* )  -> 
( A [,) B
)  C_  RR )
279277, 278syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( A [,) B
)  C_  RR )
280190a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( RR  \  ( A [,] B ) ) 
C_  RR )
281279, 280jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( A [,) B )  C_  RR  /\  ( RR  \  ( A [,] B ) ) 
C_  RR ) )
282 unss 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A [,) B
)  C_  RR  /\  ( RR  \  ( A [,] B ) )  C_  RR )  <->  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) )  C_  RR )
283281, 282sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) 
C_  RR )
284 elioore 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -oo (,) B )  ->  x  e.  RR )
285284ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  x  e.  RR )
28621, 284anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  x  e.  ( -oo (,) B ) )  ->  ( x  e.  RR  /\  A  e.  RR ) )
287286adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  (
x  e.  RR  /\  A  e.  RR )
)
288287simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  A  e.  RR )
28928ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  ( A  e.  RR*  /\  B  e.  RR* ) )
290289simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  B  e.  RR* )
291285rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  x  e.  RR* )
292 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  x  <  A )
293288, 290, 291, 292ltnelicc 31417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  -.  x  e.  ( A [,] B ) )
294285, 293jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  (
x  e.  RR  /\  -.  x  e.  ( A [,] B ) ) )
295 eldif 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  ( RR  \ 
( A [,] B
) )  <->  ( x  e.  RR  /\  -.  x  e.  ( A [,] B
) ) )
296294, 295sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  x  e.  ( RR  \  ( A [,] B ) ) )
297296olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  x  <  A )  ->  (
x  e.  ( A [,) B )  \/  x  e.  ( RR 
\  ( A [,] B ) ) ) )
298284ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  ->  x  e.  RR )
299 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  ->  -.  x  <  A )
300286ancomd 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  x  e.  ( -oo (,) B ) )  ->  ( A  e.  RR  /\  x  e.  RR ) )
301300adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  -> 
( A  e.  RR  /\  x  e.  RR ) )
302 lenlt 9675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( A  e.  RR  /\  x  e.  RR )  ->  ( A  <_  x  <->  -.  x  <  A ) )
303301, 302syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  -> 
( A  <_  x  <->  -.  x  <  A ) )
304299, 303mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  ->  A  <_  x )
305 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  e.  ( -oo (,) B )  <->  ( ( -oo  e.  RR*  /\  B  e. 
RR*  /\  x  e.  RR* )  /\  ( -oo  <  x  /\  x  < 
B ) ) )
306305biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( -oo (,) B )  ->  (
( -oo  e.  RR*  /\  B  e.  RR*  /\  x  e. 
RR* )  /\  ( -oo  <  x  /\  x  <  B ) ) )
307306simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( -oo (,) B )  ->  ( -oo  <  x  /\  x  <  B ) )
308307simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( -oo (,) B )  ->  x  <  B )
309308ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  ->  x  <  B )
310298, 304, 3093jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  -> 
( x  e.  RR  /\  A  <_  x  /\  x  <  B ) )
311277ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  -> 
( A  e.  RR  /\  B  e.  RR* )
)
312 elico2 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A  e.  RR  /\  B  e.  RR* )  -> 
( x  e.  ( A [,) B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <  B ) ) )
313311, 312syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  -> 
( x  e.  ( A [,) B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <  B ) ) )
314310, 313mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  ->  x  e.  ( A [,) B ) )
315314orcd 392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( -oo (,) B
) )  /\  -.  x  <  A )  -> 
( x  e.  ( A [,) B )  \/  x  e.  ( RR  \  ( A [,] B ) ) ) )
316297, 315pm2.61dan 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  ( -oo (,) B ) )  ->  ( x  e.  ( A [,) B
)  \/  x  e.  ( RR  \  ( A [,] B ) ) ) )
317 elun 3650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) )  <->  ( x  e.  ( A [,) B
)  \/  x  e.  ( RR  \  ( A [,] B ) ) ) )
318316, 317sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  x  e.  ( -oo (,) B ) )  ->  x  e.  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )
319318ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( x  e.  ( -oo (,) B )  ->  x  e.  ( ( A [,) B
)  u.  ( RR 
\  ( A [,] B ) ) ) ) )
3201, 319ralrimi 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  A. x  e.  ( -oo (,) B ) x  e.  ( ( A [,) B )  u.  ( RR  \ 
( A [,] B
) ) ) )
321 dfss3 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( -oo (,) B ) 
C_  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) )  <->  A. x  e.  ( -oo (,) B ) x  e.  ( ( A [,) B )  u.  ( RR  \ 
( A [,] B
) ) ) )
322320, 321sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( -oo (,) B
)  C_  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )
323269, 283, 3223jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) 
C_  RR  /\  ( -oo (,) B )  C_  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
324198ntrss 19424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( A [,) B )  u.  ( RR  \ 
( A [,] B
) ) )  C_  RR  /\  ( -oo (,) B )  C_  (
( A [,) B
)  u.  ( RR 
\  ( A [,] B ) ) ) )  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( -oo (,) B ) ) 
C_  ( ( int `  ( topGen `  ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
325323, 324syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( -oo (,) B ) )  C_  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
326325sseld 3508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( -oo (,) B ) )  ->  A  e.  ( ( int `  ( topGen `  ran  (,) ) ) `  (
( A [,) B
)  u.  ( RR 
\  ( A [,] B ) ) ) ) ) )
327276, 326mpd 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A  e.  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
328327, 250jca 532 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  /\  A  e.  ( A [,] B
) ) )
329 elin 3692 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  e.  ( ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) )  <-> 
( A  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  /\  A  e.  ( A [,] B
) ) )
330328, 329sylibr 212 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  ( ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) ) )
331 icossicc 11623 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A [,) B )  C_  ( A [,] B )
332331a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A [,) B )  C_  ( A [,] B ) )
33328, 332syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( A [,) B
)  C_  ( A [,] B ) )
334269, 180, 3333jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B ) 
C_  RR  /\  ( A [,) B )  C_  ( A [,] B ) ) )
335198, 219restntr 19551 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A [,] B )  C_  RR  /\  ( A [,) B )  C_  ( A [,] B ) )  ->  ( ( int `  ( ( topGen `  ran  (,) )t  ( A [,] B
) ) ) `  ( A [,) B ) )  =  ( ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) ) )
336334, 335syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( int `  (
( topGen `  ran  (,) )t  ( A [,] B ) ) ) `  ( A [,) B ) )  =  ( ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) ) )
337336eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( int `  ( topGen `  ran  (,) )
) `  ( ( A [,) B )  u.  ( RR  \  ( A [,] B ) ) ) )  i^i  ( A [,] B ) )  =  ( ( int `  ( ( topGen `  ran  (,) )t  ( A [,] B
) ) ) `  ( A [,) B ) ) )
338330, 337eleqtrd 2557 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  ( ( int `  ( (
topGen `  ran  (,) )t  ( A [,] B ) ) ) `  ( A [,) B ) ) )
339233fveq1d 5874 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( int `  (
( topGen `  ran  (,) )t  ( A [,] B ) ) ) `  ( A [,) B ) )  =  ( ( int `  ( ( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A [,) B ) ) )
340338, 339eleqtrd 2557 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  ( ( int `  ( (
TopOpen ` fld )t  ( A [,] B
) ) ) `  ( A [,) B ) ) )
341250snssd 4178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  { A }  C_  ( A [,] B ) )
342 ssequn2 3682 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( { A }  C_  ( A [,] B )  <->  ( ( A [,] B )  u. 
{ A } )  =  ( A [,] B ) )
343341, 342sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( A [,] B )  u.  { A } )  =  ( A [,] B ) )
344343eqcomd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( A [,] B
)  =  ( ( A [,] B )  u.  { A }
) )
345344oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( TopOpen ` fld )t  ( A [,] B ) )  =  ( ( TopOpen ` fld )t  ( ( A [,] B )  u. 
{ A } ) ) )
346345fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) )  =  ( int `  (
( TopOpen ` fld )t  ( ( A [,] B )  u. 
{ A } ) ) ) )
347 uncom 3653 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A (,) B )  u.  { A }
)  =  ( { A }  u.  ( A (,) B ) )
34822, 25, 273jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR*  /\  A  <  B ) )
349 snunioo 11658 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  ( { A }  u.  ( A (,) B ) )  =  ( A [,) B ) )
350348, 349syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( { A }  u.  ( A (,) B
) )  =  ( A [,) B ) )
351347, 350syl5eq 2520 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( A (,) B )  u.  { A } )  =  ( A [,) B ) )
352351eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A [,) B
)  =  ( ( A (,) B )  u.  { A }
) )
353346, 352fveq12d 5878 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  ( A [,] B ) ) ) `
 ( A [,) B ) )  =  ( ( int `  (
( TopOpen ` fld )t  ( ( A [,] B )  u. 
{ A } ) ) ) `  (
( A (,) B
)  u.  { A } ) ) )
354340, 353eleqtrd 2557 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  ( ( int `  ( (
TopOpen ` fld )t  ( ( A [,] B )  u.  { A } ) ) ) `
 ( ( A (,) B )  u. 
{ A } ) ) )
35554, 65, 182, 141, 259, 354limcres 22158 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( G  |`  ( A (,) B ) ) lim CC  A )  =  ( G lim CC  A ) )
356258, 355eleqtrd 2557 . . . . . . . . . . . . . . 15  |-  ( ph  ->  R  e.  ( G lim
CC  A ) )
357255, 356eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  A
)  e.  ( G lim
CC  A ) )
35854, 357jca 532 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G : ( A [,] B ) --> CC  /\  ( G `
 A )  e.  ( G lim CC  A
) ) )
359182, 250jca 532 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A [,] B )  C_  CC  /\  A  e.  ( A [,] B ) ) )
360 eqid 2467 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )t  ( A [,] B
) )  =  ( ( TopOpen ` fld )t  ( A [,] B ) )
361141, 360cnplimc 22159 . . . . . . . . . . . . . 14  |-  ( ( ( A [,] B
)  C_  CC  /\  A  e.  ( A [,] B
) )  ->  ( G  e.  ( (
( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
)  <->  ( G :
( A [,] B
) --> CC  /\  ( G `  A )  e.  ( G lim CC  A
) ) ) )
362359, 361syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G  e.  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
)  <->  ( G :
( A [,] B
) --> CC  /\  ( G `  A )  e.  ( G lim CC  A
) ) ) )
363358, 362mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  G  e.  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
) )
364363idi 2 . . . . . . . . . . 11  |-  ( ph  ->  G  e.  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
) )
365364adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  A )  ->  G  e.  ( ( ( (
TopOpen ` fld )t  ( A [,] B
) )  CnP  ( TopOpen
` fld
) ) `  A
) )
366 fveq2 5872 . . . . . . . . . . . 12  |-  ( y  =  A  ->  (
( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  y
)  =  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
) )
367366eqcomd 2475 . . . . . . . . . . 11  |-  ( y  =  A  ->  (
( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
)  =  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  y
) )
368367adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  A )  ->  (
( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  A
)  =  ( ( ( ( TopOpen ` fld )t  ( A [,] B ) )  CnP  ( TopOpen ` fld ) ) `  y
) )
369365, 368eleqtrd 2557 . . . . . . . . 9  |-  ( (
ph  /\  y  =  A )  ->  G  e.  ( ( ( (
TopOpen ` fld )t  ( A [,] B
) )  CnP  ( TopOpen
` fld
) ) `  y
) )
37024leidd 10131 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  <_  B )
37124, 31, 3703jca 1176 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B  e.  RR  /\  A  <_  B  /\  B  <_  B ) )
372 elicc2 11601 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( B  e.  ( A [,] B )  <-> 
( B  e.  RR  /\  A  <_  B  /\  B  <_  B ) ) )
373178, 372syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B  e.  ( A [,] B )  <-> 
( B  e.  RR  /\  A  <_  B  /\  B  <_  B ) ) )
374371, 373mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  ( A [,] B ) )
375 eqid 2467 . . . . . . . . . . . . . . . . . . . . . 22  |-  B  =  B
376 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( B  =  B  ->  if ( B  =  B ,  L ,  ( F `
 B ) )  =  L )
377375, 376ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( B  =  B ,  L ,  ( F `  B ) )  =  L
378377, 8syl5eqel 2559 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  if ( B  =  B ,  L , 
( F `  B
) )  e.  CC )
3794, 378jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( R  e.  CC  /\  if ( B  =  B ,  L , 
( F `  B
) )  e.  CC ) )
380 ifcl 3987 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e.  CC  /\  if ( B  =  B ,  L ,  ( F `  B ) )  e.  CC )  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L , 
( F `  B
) ) )  e.  CC )
381379, 380syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  e.  CC )
382374, 381jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  e.  ( A [,] B )  /\  if ( B  =  A ,  R ,  if ( B  =  B ,  L , 
( F `  B
) ) )  e.  CC ) )
383 nfcv 2629 . . . . . . . . . . . . . . . . . 18  |-  F/_ x B
384 nfv 1683 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( B  e.  ( A [,] B )  /\  if ( B  =  A ,  R ,  if ( B  =  B ,  L , 
( F `  B
) ) )  e.  CC )
38571, 383nffv 5879 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x
( G `  B
)
386 nfcv 2629 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `
 B ) ) )
387385, 386nfeq 2640 . . . . . . . . . . . . . . . . . . 19  |-  F/ x
( G `  B
)  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )
388384, 387nfim 1867 . . . . . . . . . . . . . . . . . 18  |-  F/ x
( ( B  e.  ( A [,] B
)  /\  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  e.  CC )  -> 
( G `  B
)  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) )
389 eleq1 2539 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  B  ->  (
x  e.  ( A [,] B )  <->  B  e.  ( A [,] B ) ) )
390252adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  =  B  /\  x  =  A )  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) )  =  R )
391 eqtr2 2494 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  =  B  /\  x  =  A )  ->  B  =  A )
392 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( B  =  A  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  =  R )
393392eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( B  =  A  ->  R  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) )
394391, 393syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  =  B  /\  x  =  A )  ->  R  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) )
395390, 394eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  =  B  /\  x  =  A )  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) )  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `
 B ) ) ) )
396113adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  =  if ( x  =  B ,  L ,  ( F `  x ) ) )
397 iftrue 3951 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  B  ->  if ( x  =  B ,  L ,  ( F `
 x ) )  =  L )
398397adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if (
x  =  B ,  L ,  ( F `  x ) )  =  L )
399396, 398eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  =  L )
400 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  x  =  B )
401 df-ne 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =/=  A  <->  -.  x  =  A )
402401biimpri 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  x  =  A  ->  x  =/=  A )
403402adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  x  =/=  A )
404400, 403jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  ( x  =  B  /\  x  =/=  A ) )
405 pm13.18 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  =  B  /\  x  =/=  A )  ->  B  =/=  A )
406404, 405syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  B  =/=  A )
407406neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  -.  B  =  A )
408 iffalse 3954 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( -.  B  =  A  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `
 B ) ) )  =  if ( B  =  B ,  L ,  ( F `  B ) ) )
409407, 408syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  =  if ( B  =  B ,  L ,  ( F `  B ) ) )
410377a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if ( B  =  B ,  L ,  ( F `  B ) )  =  L )
411409, 410eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  =  L )
412411eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  L  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `
 B ) ) ) )
413399, 412eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  =  B  /\  -.  x  =  A
)  ->  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L , 
( F `  B
) ) ) )
414395, 413pm2.61dan 789 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  B  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) )  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L , 
( F `  B
) ) ) )
415414eleq1d 2536 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  B  ->  ( if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) )  e.  CC  <->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  e.  CC ) )
416389, 415anbi12d 710 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  B  ->  (
( x  e.  ( A [,] B )  /\  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) )  e.  CC )  <->  ( B  e.  ( A [,] B
)  /\  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  e.  CC ) ) )
417 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  B  ->  ( G `  x )  =  ( G `  B ) )
418417, 414eqeq12d 2489 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  B  ->  (
( G `  x
)  =  if ( x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  <-> 
( G `  B
)  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) ) )
419416, 418imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  B  ->  (
( ( x  e.  ( A [,] B
)  /\  if (
x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) )  e.  CC )  -> 
( G `  x
)  =  if ( x  =  A ,  R ,  if (
x  =  B ,  L ,  ( F `  x ) ) ) )  <->  ( ( B  e.  ( A [,] B )  /\  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  e.  CC )  -> 
( G `  B
)  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) ) ) )
42098a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( A [,] B )  ->  (
( x  e.  ( A [,] B )  /\  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) )  e.  CC )  ->  ( G `  x )  =  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) ) )
421383, 388, 419, 420vtoclgaf 3181 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  ( A [,] B )  ->  (
( B  e.  ( A [,] B )  /\  if ( B  =  A ,  R ,  if ( B  =  B ,  L , 
( F `  B
) ) )  e.  CC )  ->  ( G `  B )  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) ) )
422374, 382, 421sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( G `  B
)  =  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) ) )
42321, 27ltned 9732 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  =/=  B )
424423necomd 2738 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  =/=  A )
425424neneqd 2669 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  B  =  A )
426425, 408syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( B  =  A ,  R ,  if ( B  =  B ,  L ,  ( F `  B ) ) )  =  if ( B  =  B ,  L ,  ( F `  B ) ) )
427377a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  if ( B  =  B ,  L , 
( F `  B
) )  =  L )
428422, 426, 4273eqtrd 2512 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( G `  B
)  =  L )
429256oveq1d 6310 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F lim CC  B
)  =  ( ( G  |`  ( A (,) B ) ) lim CC  B ) )
4307, 429eleqtrd 2557 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  L  e.  ( ( G  |`  ( A (,) B ) ) lim CC  B ) )
431 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( (
TopOpen ` fld )t  ( ( A [,] B )  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( ( A [,] B )  u. 
{ B } ) )
432 pnfxr 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |- +oo  e.  RR*
433432a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  -> +oo  e.  RR* )
43422, 433, 253jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  e.  RR*  /\ +oo  e.  RR*  /\  B  e. 
RR* ) )
435 ltpnf 11343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( B  e.  RR  ->  B  < +oo )
43624, 435syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  B  < +oo )
43727, 436jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A  <  B  /\  B  < +oo )
)
438434, 437jca 532 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( A  e. 
RR*  /\ +oo  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  B  /\  B  < +oo )
) )
439 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( B  e.  ( A (,) +oo )  <->  ( ( A  e.  RR*  /\ +oo  e.  RR* 
/\  B  e.  RR* )  /\  ( A  < 
B  /\  B  < +oo ) ) )
440438, 439sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  B  e.  ( A (,) +oo ) )
441 iooretop 21141 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A (,) +oo )  e.  ( topGen `  ran  (,) )
442441a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A (,) +oo )  e.  ( topGen ` 
ran  (,) ) )
443269, 442jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( topGen `  ran  (,) )  e.  Top  /\  ( A (,) +oo )  e.  ( topGen `  ran  (,) )
) )
444 isopn3i 19451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( A (,) +oo )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A (,) +oo ) )  =  ( A (,) +oo ) )
445443, 444syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( A (,) +oo ) )  =  ( A (,) +oo ) )
446445eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( A (,) +oo )  =  ( ( int `  ( topGen `  ran  (,) ) ) `  ( A (,) +oo ) ) )
447440, 446eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  B  e.  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( A (,) +oo )
) )
44822, 24jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( A  e.  RR*  /\  B  e.  RR ) )
449 iocssre 11616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A (,] B )  C_  RR )
450448, 449syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( A (,] B
)  C_  RR )
451450, 280jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( A (,] B )  C_  RR  /\  ( RR  \  ( A [,] B ) ) 
C_  RR ) )
452 unss 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A (,] B
)  C_  RR  /\  ( RR  \  ( A [,] B ) )  C_  RR )  <->  ( ( A (,] B )  u.  ( RR  \  ( A [,] B ) ) )  C_  RR )
453451, 452sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( A (,] B )  u.  ( RR  \  ( A [,] B ) ) ) 
C_  RR )
454 elioore 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( A (,) +oo )  ->  x  e.  RR )
455454ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  x  e.  RR )
456 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  e.  ( A (,) +oo )  <->  ( ( A  e.  RR*  /\ +oo  e.  RR* 
/\  x  e.  RR* )  /\  ( A  < 
x  /\  x  < +oo ) ) )
457456biimpi 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  ( A (,) +oo )  ->  ( ( A  e.  RR*  /\ +oo  e.  RR*  /\  x  e. 
RR* )  /\  ( A  <  x  /\  x  < +oo ) ) )
458457simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  ( A (,) +oo )  ->  ( A  <  x  /\  x  < +oo ) )
459458simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( A (,) +oo )  ->  A  <  x )
460459ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  A  <  x )
461 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  x  <_  B )
462455, 460, 4613jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  (
x  e.  RR  /\  A  <  x  /\  x  <_  B ) )
463448ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  ( A  e.  RR*  /\  B  e.  RR ) )
464 elioc2 11599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  (
x  e.  ( A (,] B )  <->  ( x  e.  RR  /\  A  < 
x  /\  x  <_  B ) ) )
465463, 464syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  (
x  e.  ( A (,] B )  <->  ( x  e.  RR  /\  A  < 
x  /\  x  <_  B ) ) )
466462, 465mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  x  e.  ( A (,] B
) )
467 ssun1 3672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A (,] B )  C_  ( ( A (,] B )  u.  ( RR  \  ( A [,] B ) ) )
468467a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  ( A (,] B )  C_  ( ( A (,] B )  u.  ( RR  \  ( A [,] B ) ) ) )
469468sseld 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  (
x  e.  ( A (,] B )  ->  x  e.  ( ( A (,] B )  u.  ( RR  \  ( A [,] B ) ) ) ) )
470466, 469mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  x  <_  B )  ->  x  e.  ( ( A (,] B )  u.  ( RR  \  ( A [,] B ) ) ) )
471454ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  ->  x  e.  RR )
472 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  ->  -.  x  <_  B )
473 simp3 998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  A  <_  x  /\  x  <_  B )  ->  x  <_  B )
474472, 473nsyl 121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  ->  -.  ( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) )
475178ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  -> 
( A  e.  RR  /\  B  e.  RR ) )
476 elicc2 11601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
477475, 476syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  -> 
( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
478474, 477mtbird 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  ->  -.  x  e.  ( A [,] B ) )
479471, 478jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  -> 
( x  e.  RR  /\ 
-.  x  e.  ( A [,] B ) ) )
480479, 295sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  ( A (,) +oo ) )  /\  -.  x  <_  B )  ->  x  e.  ( RR  \  ( A [,] B