MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2cnlem1 Structured version   Unicode version

Theorem itg2cnlem1 21208
Description: Lemma for itgcn 21289. (Contributed by Mario Carneiro, 30-Aug-2014.)
Hypotheses
Ref Expression
itg2cn.1  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
itg2cn.2  |-  ( ph  ->  F  e. MblFn )
itg2cn.3  |-  ( ph  ->  ( S.2 `  F
)  e.  RR )
Assertion
Ref Expression
itg2cnlem1  |-  ( ph  ->  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) ) , 
RR* ,  <  )  =  ( S.2 `  F
) )
Distinct variable groups:    x, n, F    ph, n, x

Proof of Theorem itg2cnlem1
Dummy variables  m  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5694 . . . . . . . . . 10  |-  ( F `
 x )  e. 
_V
2 c0ex 9372 . . . . . . . . . 10  |-  0  e.  _V
31, 2ifex 3851 . . . . . . . . 9  |-  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 )  e.  _V
4 eqid 2437 . . . . . . . . . 10  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )
54fvmpt2 5774 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  e.  _V )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `
 x )  =  if ( ( F `
 x )  <_  n ,  ( F `  x ) ,  0 ) )
63, 5mpan2 671 . . . . . . . 8  |-  ( x  e.  RR  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
)  =  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )
76mpteq2dv 4372 . . . . . . 7  |-  ( x  e.  RR  ->  (
n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
) )  =  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
87rneqd 5059 . . . . . 6  |-  ( x  e.  RR  ->  ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `
 x ) )  =  ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) )
98supeq1d 7688 . . . . 5  |-  ( x  e.  RR  ->  sup ( ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  x ) ) ,  RR ,  <  )  =  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  ) )
109mpteq2ia 4367 . . . 4  |-  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `
 x ) ) ,  RR ,  <  ) )  =  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  ) )
11 nfcv 2573 . . . . 5  |-  F/_ y sup ( ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
) ) ,  RR ,  <  )
12 nfcv 2573 . . . . . . . 8  |-  F/_ x NN
13 nfmpt1 4374 . . . . . . . . . . 11  |-  F/_ x
( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )
1412, 13nfmpt 4373 . . . . . . . . . 10  |-  F/_ x
( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
15 nfcv 2573 . . . . . . . . . 10  |-  F/_ x m
1614, 15nffv 5691 . . . . . . . . 9  |-  F/_ x
( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )
17 nfcv 2573 . . . . . . . . 9  |-  F/_ x
y
1816, 17nffv 5691 . . . . . . . 8  |-  F/_ x
( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
1912, 18nfmpt 4373 . . . . . . 7  |-  F/_ x
( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
)
2019nfrn 5074 . . . . . 6  |-  F/_ x ran  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
)
21 nfcv 2573 . . . . . 6  |-  F/_ x RR
22 nfcv 2573 . . . . . 6  |-  F/_ x  <
2320, 21, 22nfsup 7693 . . . . 5  |-  F/_ x sup ( ran  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
) ) ,  RR ,  <  )
24 fveq2 5684 . . . . . . . . 9  |-  ( x  =  y  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
)  =  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  y
) )
2524mpteq2dv 4372 . . . . . . . 8  |-  ( x  =  y  ->  (
n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
) )  =  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  y
) ) )
26 breq2 4289 . . . . . . . . . . . . 13  |-  ( n  =  m  ->  (
( F `  x
)  <_  n  <->  ( F `  x )  <_  m
) )
2726ifbid 3804 . . . . . . . . . . . 12  |-  ( n  =  m  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  =  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
2827mpteq2dv 4372 . . . . . . . . . . 11  |-  ( n  =  m  ->  (
x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) )
2928fveq1d 5686 . . . . . . . . . 10  |-  ( n  =  m  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  y
)  =  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
) )
3029cbvmptv 4376 . . . . . . . . 9  |-  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  y
) )  =  ( m  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
) )
31 eqid 2437 . . . . . . . . . . . 12  |-  ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) )  =  ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
32 reex 9365 . . . . . . . . . . . . 13  |-  RR  e.  _V
3332mptex 5941 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  e.  _V
3428, 31, 33fvmpt 5767 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  (
( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) )
3534fveq1d 5686 . . . . . . . . . 10  |-  ( m  e.  NN  ->  (
( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `
 y )  =  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `
 y ) )
3635mpteq2ia 4367 . . . . . . . . 9  |-  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
) )  =  ( m  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
) )
3730, 36eqtr4i 2460 . . . . . . . 8  |-  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  y
) )  =  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `
 y ) )
3825, 37syl6eq 2485 . . . . . . 7  |-  ( x  =  y  ->  (
n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
) )  =  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `
 y ) ) )
3938rneqd 5059 . . . . . 6  |-  ( x  =  y  ->  ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `
 x ) )  =  ran  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
) ) )
4039supeq1d 7688 . . . . 5  |-  ( x  =  y  ->  sup ( ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  x ) ) ,  RR ,  <  )  =  sup ( ran  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
) ,  RR ,  <  ) )
4111, 23, 40cbvmpt 4375 . . . 4  |-  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `
 x ) ) ,  RR ,  <  ) )  =  ( y  e.  RR  |->  sup ( ran  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
) ,  RR ,  <  ) )
4210, 41eqtr3i 2459 . . 3  |-  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  ) )  =  ( y  e.  RR  |->  sup ( ran  ( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
) ) ,  RR ,  <  ) )
43 fveq2 5684 . . . . . . . 8  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
4443breq1d 4295 . . . . . . 7  |-  ( x  =  y  ->  (
( F `  x
)  <_  m  <->  ( F `  y )  <_  m
) )
4544, 43ifbieq1d 3805 . . . . . 6  |-  ( x  =  y  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  if ( ( F `  y
)  <_  m , 
( F `  y
) ,  0 ) )
4645cbvmptv 4376 . . . . 5  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  =  ( y  e.  RR  |->  if ( ( F `  y
)  <_  m , 
( F `  y
) ,  0 ) )
4734adantl 466 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) )
48 nnre 10321 . . . . . . . . . . . . 13  |-  ( m  e.  NN  ->  m  e.  RR )
4948ad2antlr 726 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  m  e.  RR )
5049rexrd 9425 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  m  e.  RR* )
51 elioopnf 11375 . . . . . . . . . . 11  |-  ( m  e.  RR*  ->  ( ( F `  y )  e.  ( m (,) +oo )  <->  ( ( F `
 y )  e.  RR  /\  m  < 
( F `  y
) ) ) )
5250, 51syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( F `  y
)  e.  ( m (,) +oo )  <->  ( ( F `  y )  e.  RR  /\  m  < 
( F `  y
) ) ) )
53 itg2cn.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
54 ffn 5552 . . . . . . . . . . . . . 14  |-  ( F : RR --> ( 0 [,) +oo )  ->  F  Fn  RR )
5553, 54syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  F  Fn  RR )
5655ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  F  Fn  RR )
57 elpreima 5816 . . . . . . . . . . . 12  |-  ( F  Fn  RR  ->  (
y  e.  ( `' F " ( m (,) +oo ) )  <-> 
( y  e.  RR  /\  ( F `  y
)  e.  ( m (,) +oo ) ) ) )
5856, 57syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( `' F " ( m (,) +oo ) )  <-> 
( y  e.  RR  /\  ( F `  y
)  e.  ( m (,) +oo ) ) ) )
59 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  y  e.  RR )
6059biantrurd 508 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( F `  y
)  e.  ( m (,) +oo )  <->  ( y  e.  RR  /\  ( F `
 y )  e.  ( m (,) +oo ) ) ) )
6158, 60bitr4d 256 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( `' F " ( m (,) +oo ) )  <-> 
( F `  y
)  e.  ( m (,) +oo ) ) )
62 0re 9378 . . . . . . . . . . . . . . 15  |-  0  e.  RR
63 pnfxr 11084 . . . . . . . . . . . . . . 15  |- +oo  e.  RR*
64 icossre 11368 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\ +oo  e.  RR* )  ->  (
0 [,) +oo )  C_  RR )
6562, 63, 64mp2an 672 . . . . . . . . . . . . . 14  |-  ( 0 [,) +oo )  C_  RR
66 fss 5560 . . . . . . . . . . . . . 14  |-  ( ( F : RR --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  RR )  ->  F : RR --> RR )
6753, 65, 66sylancl 662 . . . . . . . . . . . . 13  |-  ( ph  ->  F : RR --> RR )
6867adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  F : RR
--> RR )
6968ffvelrnda 5836 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  ( F `  y )  e.  RR )
7069biantrurd 508 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
m  <  ( F `  y )  <->  ( ( F `  y )  e.  RR  /\  m  < 
( F `  y
) ) ) )
7152, 61, 703bitr4d 285 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( `' F " ( m (,) +oo ) )  <-> 
m  <  ( F `  y ) ) )
7271notbid 294 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  ( -.  y  e.  ( `' F " ( m (,) +oo ) )  <->  -.  m  <  ( F `
 y ) ) )
73 eldif 3331 . . . . . . . . . 10  |-  ( y  e.  ( RR  \ 
( `' F "
( m (,) +oo ) ) )  <->  ( y  e.  RR  /\  -.  y  e.  ( `' F "
( m (,) +oo ) ) ) )
7473baib 896 . . . . . . . . 9  |-  ( y  e.  RR  ->  (
y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) )  <->  -.  y  e.  ( `' F "
( m (,) +oo ) ) ) )
7574adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) )  <->  -.  y  e.  ( `' F "
( m (,) +oo ) ) ) )
7669, 49lenltd 9512 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( F `  y
)  <_  m  <->  -.  m  <  ( F `  y
) ) )
7772, 75, 763bitr4d 285 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) )  <->  ( F `  y )  <_  m
) )
7877ifbid 3804 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 )  =  if ( ( F `  y )  <_  m ,  ( F `  y ) ,  0 ) )
7978mpteq2dva 4371 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( y  e.  RR  |->  if ( y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) ) ,  ( F `  y
) ,  0 ) )  =  ( y  e.  RR  |->  if ( ( F `  y
)  <_  m , 
( F `  y
) ,  0 ) ) )
8046, 47, 793eqtr4a 2495 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  =  ( y  e.  RR  |->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 ) ) )
81 difss 3476 . . . . . 6  |-  ( RR 
\  ( `' F " ( m (,) +oo ) ) )  C_  RR
8281a1i 11 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( RR 
\  ( `' F " ( m (,) +oo ) ) )  C_  RR )
83 rembl 20991 . . . . . 6  |-  RR  e.  dom  vol
8483a1i 11 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  RR  e.  dom  vol )
85 fvex 5694 . . . . . . 7  |-  ( F `
 y )  e. 
_V
8685, 2ifex 3851 . . . . . 6  |-  if ( y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) ) ,  ( F `  y
) ,  0 )  e.  _V
8786a1i 11 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) )  ->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 )  e.  _V )
88 eldifn 3472 . . . . . . 7  |-  ( y  e.  ( RR  \ 
( RR  \  ( `' F " ( m (,) +oo ) ) ) )  ->  -.  y  e.  ( RR  \  ( `' F "
( m (,) +oo ) ) ) )
8988adantl 466 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  ( RR  \  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ) )  ->  -.  y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) )
90 iffalse 3792 . . . . . 6  |-  ( -.  y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) )  ->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 )  =  0 )
9189, 90syl 16 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  ( RR  \  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ) )  ->  if (
y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) ) ,  ( F `  y
) ,  0 )  =  0 )
92 iftrue 3790 . . . . . . . . 9  |-  ( y  e.  ( RR  \ 
( `' F "
( m (,) +oo ) ) )  ->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 )  =  ( F `  y ) )
9392mpteq2ia 4367 . . . . . . . 8  |-  ( y  e.  ( RR  \ 
( `' F "
( m (,) +oo ) ) )  |->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 ) )  =  ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) )  |->  ( F `  y ) )
94 resmpt 5149 . . . . . . . . 9  |-  ( ( RR  \  ( `' F " ( m (,) +oo ) ) )  C_  RR  ->  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F "
( m (,) +oo ) ) ) )  =  ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) )  |->  ( F `  y ) ) )
9581, 94ax-mp 5 . . . . . . . 8  |-  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F "
( m (,) +oo ) ) ) )  =  ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) )  |->  ( F `  y ) )
9693, 95eqtr4i 2460 . . . . . . 7  |-  ( y  e.  ( RR  \ 
( `' F "
( m (,) +oo ) ) )  |->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 ) )  =  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F " ( m (,) +oo ) ) ) )
9753feqmptd 5737 . . . . . . . . 9  |-  ( ph  ->  F  =  ( y  e.  RR  |->  ( F `
 y ) ) )
98 itg2cn.2 . . . . . . . . 9  |-  ( ph  ->  F  e. MblFn )
9997, 98eqeltrrd 2512 . . . . . . . 8  |-  ( ph  ->  ( y  e.  RR  |->  ( F `  y ) )  e. MblFn )
100 mbfima 21079 . . . . . . . . . 10  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " ( m (,) +oo ) )  e.  dom  vol )
10198, 67, 100syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( `' F "
( m (,) +oo ) )  e.  dom  vol )
102 cmmbl 20985 . . . . . . . . 9  |-  ( ( `' F " ( m (,) +oo ) )  e.  dom  vol  ->  ( RR  \  ( `' F " ( m (,) +oo ) ) )  e.  dom  vol )
103101, 102syl 16 . . . . . . . 8  |-  ( ph  ->  ( RR  \  ( `' F " ( m (,) +oo ) ) )  e.  dom  vol )
104 mbfres 21091 . . . . . . . 8  |-  ( ( ( y  e.  RR  |->  ( F `  y ) )  e. MblFn  /\  ( RR  \  ( `' F " ( m (,) +oo ) ) )  e. 
dom  vol )  ->  (
( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F "
( m (,) +oo ) ) ) )  e. MblFn )
10599, 103, 104syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F " ( m (,) +oo ) ) ) )  e. MblFn )
10696, 105syl5eqel 2521 . . . . . 6  |-  ( ph  ->  ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) )  |->  if ( y  e.  ( RR  \ 
( `' F "
( m (,) +oo ) ) ) ,  ( F `  y
) ,  0 ) )  e. MblFn )
107106adantr 465 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( y  e.  ( RR  \ 
( `' F "
( m (,) +oo ) ) )  |->  if ( y  e.  ( RR  \  ( `' F " ( m (,) +oo ) ) ) ,  ( F `
 y ) ,  0 ) )  e. MblFn
)
10882, 84, 87, 91, 107mbfss 21093 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( y  e.  RR  |->  if ( y  e.  ( RR 
\  ( `' F " ( m (,) +oo ) ) ) ,  ( F `  y
) ,  0 ) )  e. MblFn )
10980, 108eqeltrd 2511 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  e. MblFn )
11053ffvelrnda 5836 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  ( 0 [,) +oo ) )
111 0e0icopnf 11387 . . . . . . 7  |-  0  e.  ( 0 [,) +oo )
112 ifcl 3824 . . . . . . 7  |-  ( ( ( F `  x
)  e.  ( 0 [,) +oo )  /\  0  e.  ( 0 [,) +oo ) )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  e.  ( 0 [,) +oo ) )
113110, 111, 112sylancl 662 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 )  e.  ( 0 [,) +oo ) )
114113adantlr 714 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  e.  ( 0 [,) +oo ) )
115 eqid 2437 . . . . 5  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
116114, 115fmptd 5860 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) : RR --> ( 0 [,) +oo ) )
11747feq1d 5539 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) : RR --> ( 0 [,) +oo ) 
<->  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) : RR --> ( 0 [,) +oo ) ) )
118116, 117mpbird 232 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) : RR --> ( 0 [,) +oo ) )
119 elrege0 11384 . . . . . . . . . . . . 13  |-  ( ( F `  x )  e.  ( 0 [,) +oo )  <->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
120110, 119sylib 196 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( F `  x )  e.  RR  /\  0  <_  ( F `  x
) ) )
121120simpld 459 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  RR )
122121adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
123122adantr 465 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  e.  RR )
124123leidd 9898 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  <_  ( F `  x )
)
125 iftrue 3790 . . . . . . . . 9  |-  ( ( F `  x )  <_  m  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
126125adantl 466 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  if (
( F `  x
)  <_  m , 
( F `  x
) ,  0 )  =  ( F `  x ) )
12748ad3antlr 730 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  m  e.  RR )
128 peano2re 9534 . . . . . . . . . . 11  |-  ( m  e.  RR  ->  (
m  +  1 )  e.  RR )
129127, 128syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( m  +  1 )  e.  RR )
130 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  <_  m
)
131127lep1d 10256 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  m  <_  ( m  +  1 ) )
132123, 127, 129, 130, 131letrd 9520 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  <_  (
m  +  1 ) )
133 iftrue 3790 . . . . . . . . 9  |-  ( ( F `  x )  <_  ( m  + 
1 )  ->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
134132, 133syl 16 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  if (
( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 )  =  ( F `  x ) )
135124, 126, 1343brtr4d 4315 . . . . . . 7  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  if (
( F `  x
)  <_  m , 
( F `  x
) ,  0 )  <_  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 ) )
136 iffalse 3792 . . . . . . . . 9  |-  ( -.  ( F `  x
)  <_  m  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  0 )
137136adantl 466 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  -.  ( F `
 x )  <_  m )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  0 )
138120simprd 463 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  0  <_ 
( F `  x
) )
139 0le0 10403 . . . . . . . . . . 11  |-  0  <_  0
140 breq2 4289 . . . . . . . . . . . 12  |-  ( ( F `  x )  =  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 )  -> 
( 0  <_  ( F `  x )  <->  0  <_  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 ) ) )
141 breq2 4289 . . . . . . . . . . . 12  |-  ( 0  =  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 ) ) )
142140, 141ifboth 3818 . . . . . . . . . . 11  |-  ( ( 0  <_  ( F `  x )  /\  0  <_  0 )  ->  0  <_  if ( ( F `
 x )  <_ 
( m  +  1 ) ,  ( F `
 x ) ,  0 ) )
143138, 139, 142sylancl 662 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  0  <_  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) )
144143adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  0  <_  if ( ( F `
 x )  <_ 
( m  +  1 ) ,  ( F `
 x ) ,  0 ) )
145144adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  -.  ( F `
 x )  <_  m )  ->  0  <_  if ( ( F `
 x )  <_ 
( m  +  1 ) ,  ( F `
 x ) ,  0 ) )
146137, 145eqbrtrd 4305 . . . . . . 7  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  -.  ( F `
 x )  <_  m )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  if (
( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )
147135, 146pm2.61dan 789 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  if (
( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )
148147ralrimiva 2793 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) )
1491, 2ifex 3851 . . . . . . 7  |-  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 )  e.  _V
150149a1i 11 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 )  e.  _V )
151 eqidd 2438 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) )
152 eqidd 2438 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) ) )
15384, 114, 150, 151, 152ofrfval2 6332 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  oR  <_  ( x  e.  RR  |->  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 ) )  <->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  if (
( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) ) )
154148, 153mpbird 232 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  oR  <_ 
( x  e.  RR  |->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) ) )
155 peano2nn 10326 . . . . . 6  |-  ( m  e.  NN  ->  (
m  +  1 )  e.  NN )
156155adantl 466 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  +  1 )  e.  NN )
157 breq2 4289 . . . . . . . 8  |-  ( n  =  ( m  + 
1 )  ->  (
( F `  x
)  <_  n  <->  ( F `  x )  <_  (
m  +  1 ) ) )
158157ifbid 3804 . . . . . . 7  |-  ( n  =  ( m  + 
1 )  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  =  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )
159158mpteq2dv 4372 . . . . . 6  |-  ( n  =  ( m  + 
1 )  ->  (
x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) ) )
16032mptex 5941 . . . . . 6  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )  e.  _V
161159, 31, 160fvmpt 5767 . . . . 5  |-  ( ( m  +  1 )  e.  NN  ->  (
( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  ( m  +  1
) )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) ) )
162156, 161syl 16 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  ( m  +  1
) )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) ) )
163154, 47, 1623brtr4d 4315 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  oR  <_  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  (
m  +  1 ) ) )
16467ffvelrnda 5836 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 y )  e.  RR )
16534adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  RR )  /\  m  e.  NN )  ->  (
( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) )
166165fveq1d 5686 . . . . . 6  |-  ( ( ( ph  /\  y  e.  RR )  /\  m  e.  NN )  ->  (
( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `
 y )  =  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `
 y ) )
167121leidd 9898 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  <_ 
( F `  x
) )
168 breq1 4288 . . . . . . . . . . . . . 14  |-  ( ( F `  x )  =  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  -> 
( ( F `  x )  <_  ( F `  x )  <->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
169 breq1 4288 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  -> 
( 0  <_  ( F `  x )  <->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
170168, 169ifboth 3818 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
171167, 138, 170syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 )  <_  ( F `  x ) )
172171adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
173172ralrimiva 2793 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_ 
( F `  x
) )
17432a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  RR  e.  _V )
1751, 2ifex 3851 . . . . . . . . . . . 12  |-  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 )  e.  _V
176175a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  e.  _V )
17753feqmptd 5737 . . . . . . . . . . . 12  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
178177adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  F  =  ( x  e.  RR  |->  ( F `  x ) ) )
179174, 176, 122, 151, 178ofrfval2 6332 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  oR  <_  F  <->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_ 
( F `  x
) ) )
180173, 179mpbird 232 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  oR  <_  F )
181176, 115fmptd 5860 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) : RR --> _V )
182 ffn 5552 . . . . . . . . . . 11  |-  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) : RR --> _V  ->  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  Fn  RR )
183181, 182syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  Fn  RR )
18455adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  F  Fn  RR )
185 inidm 3552 . . . . . . . . . 10  |-  ( RR 
i^i  RR )  =  RR
186 eqidd 2438 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
)  =  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
) )
187 eqidd 2438 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  ( F `  y )  =  ( F `  y ) )
188183, 184, 174, 174, 185, 186, 187ofrfval 6323 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  oR  <_  F  <->  A. y  e.  RR  ( ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) `  y )  <_  ( F `  y ) ) )
189180, 188mpbid 210 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  A. y  e.  RR  ( ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) `  y )  <_  ( F `  y ) )
190189r19.21bi 2808 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
)  <_  ( F `  y ) )
191190an32s 802 . . . . . 6  |-  ( ( ( ph  /\  y  e.  RR )  /\  m  e.  NN )  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
)  <_  ( F `  y ) )
192166, 191eqbrtrd 4305 . . . . 5  |-  ( ( ( ph  /\  y  e.  RR )  /\  m  e.  NN )  ->  (
( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `
 y )  <_ 
( F `  y
) )
193192ralrimiva 2793 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  A. m  e.  NN  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
)  <_  ( F `  y ) )
194 breq2 4289 . . . . . 6  |-  ( z  =  ( F `  y )  ->  (
( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )  <_  z  <->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
)  <_  ( F `  y ) ) )
195194ralbidv 2729 . . . . 5  |-  ( z  =  ( F `  y )  ->  ( A. m  e.  NN  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )  <_  z  <->  A. m  e.  NN  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )  <_  ( F `  y
) ) )
196195rspcev 3066 . . . 4  |-  ( ( ( F `  y
)  e.  RR  /\  A. m  e.  NN  (
( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `
 y )  <_ 
( F `  y
) )  ->  E. z  e.  RR  A. m  e.  NN  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
)  <_  z )
197164, 193, 196syl2anc 661 . . 3  |-  ( (
ph  /\  y  e.  RR )  ->  E. z  e.  RR  A. m  e.  NN  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) `  y
)  <_  z )
19828fveq2d 5688 . . . . . . 7  |-  ( n  =  m  ->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )  =  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) ) )
199198cbvmptv 4376 . . . . . 6  |-  ( n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) )  =  ( m  e.  NN  |->  ( S.2 `  (
x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) ) )
20034fveq2d 5688 . . . . . . 7  |-  ( m  e.  NN  ->  ( S.2 `  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) )  =  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) ) )
201200mpteq2ia 4367 . . . . . 6  |-  ( m  e.  NN  |->  ( S.2 `  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) ) )  =  ( m  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) ) )
202199, 201eqtr4i 2460 . . . . 5  |-  ( n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) )  =  ( m  e.  NN  |->  ( S.2 `  (
( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) ) )
203202rneqi 5058 . . . 4  |-  ran  (
n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) )  =  ran  ( m  e.  NN  |->  ( S.2 `  (
( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) ) )
204203supeq1i 7689 . . 3  |-  sup ( ran  ( n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) ) , 
RR* ,  <  )  =  sup ( ran  (
m  e.  NN  |->  ( S.2 `  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) ) ) ,  RR* ,  <  )
20542, 109, 118, 163, 197, 204itg2mono 21200 . 2  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) ) )  =  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) ) , 
RR* ,  <  ) )
206 eqid 2437 . . . . . . . . . . . 12  |-  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  =  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )
20727, 206, 175fvmpt 5767 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  (
( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  m
)  =  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
208207adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  (
( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  m
)  =  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
209171adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
210208, 209eqbrtrd 4305 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  (
( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  m
)  <_  ( F `  x ) )
211210ralrimiva 2793 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  A. m  e.  NN  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  <_  ( F `  x ) )
2123a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  e.  _V )
213212, 206fmptd 5860 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) : NN --> _V )
214 ffn 5552 . . . . . . . . . 10  |-  ( ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) : NN --> _V  ->  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  Fn  NN )
215213, 214syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  Fn  NN )
216 breq1 4288 . . . . . . . . . 10  |-  ( w  =  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  ->  ( w  <_ 
( F `  x
)  <->  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  <_  ( F `  x ) ) )
217216ralrn 5839 . . . . . . . . 9  |-  ( ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  Fn  NN  ->  ( A. w  e. 
ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  ( F `  x )  <->  A. m  e.  NN  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  <_  ( F `  x ) ) )
218215, 217syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ( A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) w  <_  ( F `  x )  <->  A. m  e.  NN  (
( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  m
)  <_  ( F `  x ) ) )
219211, 218mpbird 232 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  ( F `  x ) )
220121adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  ( F `  x )  e.  RR )
221 ifcl 3824 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  e.  RR  /\  0  e.  RR )  ->  if ( ( F `
 x )  <_  n ,  ( F `  x ) ,  0 )  e.  RR )
222220, 62, 221sylancl 662 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  e.  RR )
223222, 206fmptd 5860 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) : NN --> RR )
224 frn 5558 . . . . . . . . 9  |-  ( ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) : NN --> RR  ->  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) 
C_  RR )
225223, 224syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  C_  RR )
226 1nn 10325 . . . . . . . . . 10  |-  1  e.  NN
227 fdm 5556 . . . . . . . . . . 11  |-  ( ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) : NN --> RR  ->  dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  NN )
228223, 227syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  dom  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  NN )
229226, 228syl5eleqr 2524 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  1  e. 
dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
230 n0i 3635 . . . . . . . . . 10  |-  ( 1  e.  dom  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  ->  -.  dom  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/) )
231 dm0rn0 5048 . . . . . . . . . . 11  |-  ( dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/)  <->  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/) )
232231necon3bbii 2633 . . . . . . . . . 10  |-  ( -. 
dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/)  <->  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/) )
233230, 232sylib 196 . . . . . . . . 9  |-  ( 1  e.  dom  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  ->  ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  =/=  (/) )
234229, 233syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/) )
235 breq2 4289 . . . . . . . . . . 11  |-  ( z  =  ( F `  x )  ->  (
w  <_  z  <->  w  <_  ( F `  x ) ) )
236235ralbidv 2729 . . . . . . . . . 10  |-  ( z  =  ( F `  x )  ->  ( A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_ 
z  <->  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_ 
( F `  x
) ) )
237236rspcev 3066 . . . . . . . . 9  |-  ( ( ( F `  x
)  e.  RR  /\  A. w  e.  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_ 
( F `  x
) )  ->  E. z  e.  RR  A. w  e. 
ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  z )
238121, 219, 237syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  E. z  e.  RR  A. w  e. 
ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  z )
239 suprleub 10286 . . . . . . . 8  |-  ( ( ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  C_  RR  /\  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  z )  /\  ( F `  x
)  e.  RR )  ->  ( sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  <_  ( F `  x )  <->  A. w  e.  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_ 
( F `  x
) ) )
240225, 234, 238, 121, 239syl31anc 1221 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  )  <_  ( F `  x )  <->  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  ( F `  x ) ) )
241219, 240mpbird 232 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  <_  ( F `  x )
)
242 arch 10568 . . . . . . . . 9  |-  ( ( F `  x )  e.  RR  ->  E. m  e.  NN  ( F `  x )  <  m
)
243121, 242syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  E. m  e.  NN  ( F `  x )  <  m
)
244207ad2antrl 727 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  =  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )
245 ltle 9455 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  e.  RR  /\  m  e.  RR )  ->  ( ( F `  x )  <  m  ->  ( F `  x
)  <_  m )
)
246121, 48, 245syl2an 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  (
( F `  x
)  <  m  ->  ( F `  x )  <_  m ) )
247246impr 619 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( F `  x )  <_  m
)
248247, 125syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  ( F `  x
) )
249244, 248eqtrd 2469 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  =  ( F `  x ) )
250215adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  Fn  NN )
251 simprl 755 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  m  e.  NN )
252 fnfvelrn 5833 . . . . . . . . . 10  |-  ( ( ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  Fn  NN  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  e.  ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) )
253250, 251, 252syl2anc 661 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  e.  ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) )
254249, 253eqeltrrd 2512 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( F `  x )  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
255243, 254rexlimddv 2839 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e. 
ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
256 suprub 10283 . . . . . . 7  |-  ( ( ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  C_  RR  /\  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  z )  /\  ( F `  x
)  e.  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )  -> 
( F `  x
)  <_  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  ) )
257225, 234, 238, 255, 256syl31anc 1221 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  <_  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) )
258 suprcl 10282 . . . . . . . 8  |-  ( ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) 
C_  RR  /\  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  z )  ->  sup ( ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  e.  RR )
259225, 234, 238, 258syl3anc 1218 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  e.  RR )
260259, 121letri3d 9508 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  )  =  ( F `
 x )  <->  ( sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  <_  ( F `  x )  /\  ( F `  x )  <_  sup ( ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  ) ) ) )
261241, 257, 260mpbir2and 913 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  =  ( F `  x ) )
262261mpteq2dva 4371 . . . 4  |-  ( ph  ->  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) )  =  ( x  e.  RR  |->  ( F `  x ) ) )
263262, 177eqtr4d 2472 . . 3  |-  ( ph  ->  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) )  =  F )
264263fveq2d 5688 . 2  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) ) )  =  ( S.2 `  F
) )
265205, 264eqtr3d 2471 1  |-  ( ph  ->  sup ( ran  (
n  e.  NN  |->  ( S.2 `  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) ) , 
RR* ,  <  )  =  ( S.2 `  F
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2600   A.wral 2709   E.wrex 2710   _Vcvv 2966    \ cdif 3318    C_ wss 3321   (/)c0 3630   ifcif 3784   class class class wbr 4285    e. cmpt 4343   `'ccnv 4831   dom cdm 4832   ran crn 4833    |` cres 4834   "cima 4835    Fn wfn 5406   -->wf 5407   ` cfv 5411  (class class class)co 6086    oRcofr 6314   supcsup 7682   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277   +oocpnf 9407   RR*cxr 9409    < clt 9410    <_ cle 9411   NNcn 10314   (,)cioo 11292   [,)cico 11294   volcvol 20916  MblFncmbf 21063   S.2citg2 21065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-inf2 7839  ax-cc 8596  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-disj 4256  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-ofr 6316  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-2o 6913  df-oadd 6916  df-omul 6917  df-er 7093  df-map 7208  df-pm 7209  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fi 7653  df-sup 7683  df-oi 7716  df-card 8101  df-acn 8104  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-n0 10572  df-z 10639  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-ioc 11297  df-ico 11298  df-icc 11299  df-fz 11430  df-fzo 11541  df-fl 11634  df-seq 11799  df-exp 11858  df-hash 12096  df-cj 12580  df-re 12581  df-im 12582  df-sqr 12716  df-abs 12717  df-clim 12958  df-rlim 12959  df-sum 13156  df-rest 14353  df-topgen 14374  df-psmet 17778  df-xmet 17779  df-met 17780  df-bl 17781  df-mopn 17782  df-top 18472  df-bases 18474  df-topon 18475  df-cmp 18959  df-ovol 20917  df-vol 20918  df-mbf 21068  df-itg1 21069  df-itg2 21070
This theorem is referenced by:  itg2cn  21210
  Copyright terms: Public domain W3C validator