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

Theorem itg2cnlem1 19654
Description: Lemma for itgcn 19735. (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 5743 . . . . . . . . . 10  |-  ( F `
 x )  e. 
_V
2 c0ex 9086 . . . . . . . . . 10  |-  0  e.  _V
31, 2ifex 3798 . . . . . . . . 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 5813 . . . . . . . . 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 654 . . . . . . . 8  |-  ( x  e.  RR  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  x
)  =  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )
76mpteq2dv 4297 . . . . . . 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 5098 . . . . . 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 7452 . . . . 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 4292 . . . 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 4299 . . . . . . . . . . 11  |-  F/_ x
( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )
1412, 13nfmpt 4298 . . . . . . . . . 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 5736 . . . . . . . . 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 5736 . . . . . . . 8  |-  F/_ x
( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
1912, 18nfmpt 4298 . . . . . . 7  |-  F/_ x
( m  e.  NN  |->  ( ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  m
) `  y )
)
2019nfrn 5113 . . . . . 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 7457 . . . . 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 5729 . . . . . . . . 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 4297 . . . . . . . 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 4217 . . . . . . . . . . . . 13  |-  ( n  =  m  ->  (
( F `  x
)  <_  n  <->  ( F `  x )  <_  m
) )
2726ifbid 3758 . . . . . . . . . . . 12  |-  ( n  =  m  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  =  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
2827mpteq2dv 4297 . . . . . . . . . . 11  |-  ( n  =  m  ->  (
x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) )
2928fveq1d 5731 . . . . . . . . . 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 4301 . . . . . . . . 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 9082 . . . . . . . . . . . . 13  |-  RR  e.  _V
3332mptex 5967 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  e.  _V
3428, 31, 33fvmpt 5807 . . . . . . . . . . 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 5731 . . . . . . . . . 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 4292 . . . . . . . . 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 5098 . . . . . 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 7452 . . . . 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 4300 . . . 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 5729 . . . . . . . 8  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
4443breq1d 4223 . . . . . . 7  |-  ( x  =  y  ->  (
( F `  x
)  <_  m  <->  ( F `  y )  <_  m
) )
45 eqidd 2438 . . . . . . 7  |-  ( x  =  y  ->  0  =  0 )
4644, 43, 45ifbieq12d 3762 . . . . . 6  |-  ( x  =  y  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  if ( ( F `  y
)  <_  m , 
( F `  y
) ,  0 ) )
4746cbvmptv 4301 . . . . 5  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  =  ( y  e.  RR  |->  if ( ( F `  y
)  <_  m , 
( F `  y
) ,  0 ) )
4834adantl 454 . . . . 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 ) ) )
49 nnre 10008 . . . . . . . . . . . . 13  |-  ( m  e.  NN  ->  m  e.  RR )
5049ad2antlr 709 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  m  e.  RR )
5150rexrd 9135 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  m  e.  RR* )
52 elioopnf 10999 . . . . . . . . . . 11  |-  ( m  e.  RR*  ->  ( ( F `  y )  e.  ( m (,) 
+oo )  <->  ( ( F `  y )  e.  RR  /\  m  < 
( F `  y
) ) ) )
5351, 52syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( F `  y
)  e.  ( m (,)  +oo )  <->  ( ( F `  y )  e.  RR  /\  m  < 
( F `  y
) ) ) )
54 itg2cn.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
55 ffn 5592 . . . . . . . . . . . . . 14  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
5654, 55syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  F  Fn  RR )
5756ad2antrr 708 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  F  Fn  RR )
58 elpreima 5851 . . . . . . . . . . . 12  |-  ( F  Fn  RR  ->  (
y  e.  ( `' F " ( m (,)  +oo ) )  <->  ( y  e.  RR  /\  ( F `
 y )  e.  ( m (,)  +oo ) ) ) )
5957, 58syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( `' F " ( m (,)  +oo ) )  <->  ( y  e.  RR  /\  ( F `
 y )  e.  ( m (,)  +oo ) ) ) )
60 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  y  e.  RR )
6160biantrurd 496 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( F `  y
)  e.  ( m (,)  +oo )  <->  ( y  e.  RR  /\  ( F `
 y )  e.  ( m (,)  +oo ) ) ) )
6259, 61bitr4d 249 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( `' F " ( m (,)  +oo ) )  <->  ( F `  y )  e.  ( m (,)  +oo )
) )
63 0re 9092 . . . . . . . . . . . . . . 15  |-  0  e.  RR
64 pnfxr 10714 . . . . . . . . . . . . . . 15  |-  +oo  e.  RR*
65 icossre 10992 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
6663, 64, 65mp2an 655 . . . . . . . . . . . . . 14  |-  ( 0 [,)  +oo )  C_  RR
67 fss 5600 . . . . . . . . . . . . . 14  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
6854, 66, 67sylancl 645 . . . . . . . . . . . . 13  |-  ( ph  ->  F : RR --> RR )
6968adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  F : RR
--> RR )
7069ffvelrnda 5871 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  ( F `  y )  e.  RR )
7170biantrurd 496 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
m  <  ( F `  y )  <->  ( ( F `  y )  e.  RR  /\  m  < 
( F `  y
) ) ) )
7253, 62, 713bitr4d 278 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( `' F " ( m (,)  +oo ) )  <->  m  <  ( F `  y ) ) )
7372notbid 287 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  ( -.  y  e.  ( `' F " ( m (,)  +oo ) )  <->  -.  m  <  ( F `  y
) ) )
74 eldif 3331 . . . . . . . . . 10  |-  ( y  e.  ( RR  \ 
( `' F "
( m (,)  +oo ) ) )  <->  ( y  e.  RR  /\  -.  y  e.  ( `' F "
( m (,)  +oo ) ) ) )
7574baib 873 . . . . . . . . 9  |-  ( y  e.  RR  ->  (
y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) )  <->  -.  y  e.  ( `' F "
( m (,)  +oo ) ) ) )
7675adantl 454 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) )  <->  -.  y  e.  ( `' F "
( m (,)  +oo ) ) ) )
7770, 50lenltd 9220 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( F `  y
)  <_  m  <->  -.  m  <  ( F `  y
) ) )
7873, 76, 773bitr4d 278 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) )  <->  ( F `  y )  <_  m
) )
7978ifbid 3758 . . . . . 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 ) )
8079mpteq2dva 4296 . . . . 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 ) ) )
8147, 48, 803eqtr4a 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 ) ) )
82 difss 3475 . . . . . 6  |-  ( RR 
\  ( `' F " ( m (,)  +oo ) ) )  C_  RR
8382a1i 11 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( RR 
\  ( `' F " ( m (,)  +oo ) ) )  C_  RR )
84 rembl 19436 . . . . . 6  |-  RR  e.  dom  vol
8584a1i 11 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  RR  e.  dom  vol )
86 fvex 5743 . . . . . . 7  |-  ( F `
 y )  e. 
_V
8786, 2ifex 3798 . . . . . 6  |-  if ( y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y
) ,  0 )  e.  _V
8887a1i 11 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) )  ->  if (
y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y
) ,  0 )  e.  _V )
89 eldifn 3471 . . . . . . 7  |-  ( y  e.  ( RR  \ 
( RR  \  ( `' F " ( m (,)  +oo ) ) ) )  ->  -.  y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) )
9089adantl 454 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  ( RR  \  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) ) )  ->  -.  y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) )
91 iffalse 3747 . . . . . 6  |-  ( -.  y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) )  ->  if ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y ) ,  0 )  =  0 )
9290, 91syl 16 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  ( RR  \  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) ) )  ->  if (
y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y
) ,  0 )  =  0 )
93 iftrue 3746 . . . . . . . . 9  |-  ( y  e.  ( RR  \ 
( `' F "
( m (,)  +oo ) ) )  ->  if ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y ) ,  0 )  =  ( F `
 y ) )
9493mpteq2ia 4292 . . . . . . . 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 ) )
95 resmpt 5192 . . . . . . . . 9  |-  ( ( RR  \  ( `' F " ( m (,)  +oo ) ) ) 
C_  RR  ->  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F "
( m (,)  +oo ) ) ) )  =  ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) 
|->  ( F `  y
) ) )
9682, 95ax-mp 8 . . . . . . . 8  |-  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F "
( m (,)  +oo ) ) ) )  =  ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) 
|->  ( F `  y
) )
9794, 96eqtr4i 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 ) ) ) )
9854feqmptd 5780 . . . . . . . . 9  |-  ( ph  ->  F  =  ( y  e.  RR  |->  ( F `
 y ) ) )
99 itg2cn.2 . . . . . . . . 9  |-  ( ph  ->  F  e. MblFn )
10098, 99eqeltrrd 2512 . . . . . . . 8  |-  ( ph  ->  ( y  e.  RR  |->  ( F `  y ) )  e. MblFn )
101 mbfima 19525 . . . . . . . . . 10  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " ( m (,)  +oo ) )  e. 
dom  vol )
10299, 68, 101syl2anc 644 . . . . . . . . 9  |-  ( ph  ->  ( `' F "
( m (,)  +oo ) )  e.  dom  vol )
103 cmmbl 19430 . . . . . . . . 9  |-  ( ( `' F " ( m (,)  +oo ) )  e. 
dom  vol  ->  ( RR  \  ( `' F "
( m (,)  +oo ) ) )  e. 
dom  vol )
104102, 103syl 16 . . . . . . . 8  |-  ( ph  ->  ( RR  \  ( `' F " ( m (,)  +oo ) ) )  e.  dom  vol )
105 mbfres 19537 . . . . . . . 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 )
106100, 104, 105syl2anc 644 . . . . . . 7  |-  ( ph  ->  ( ( y  e.  RR  |->  ( F `  y ) )  |`  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) )  e. MblFn )
10797, 106syl5eqel 2521 . . . . . 6  |-  ( ph  ->  ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) 
|->  if ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y ) ,  0 ) )  e. MblFn )
108107adantr 453 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( y  e.  ( RR  \ 
( `' F "
( m (,)  +oo ) ) )  |->  if ( y  e.  ( RR  \  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y ) ,  0 ) )  e. MblFn )
10983, 85, 88, 92, 108mbfss 19539 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( y  e.  RR  |->  if ( y  e.  ( RR 
\  ( `' F " ( m (,)  +oo ) ) ) ,  ( F `  y
) ,  0 ) )  e. MblFn )
11081, 109eqeltrd 2511 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  e. MblFn )
11154ffvelrnda 5871 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  ( 0 [,)  +oo ) )
112 0le0 10082 . . . . . . . 8  |-  0  <_  0
113 elrege0 11008 . . . . . . . 8  |-  ( 0  e.  ( 0 [,) 
+oo )  <->  ( 0  e.  RR  /\  0  <_  0 ) )
11463, 112, 113mpbir2an 888 . . . . . . 7  |-  0  e.  ( 0 [,)  +oo )
115 ifcl 3776 . . . . . . 7  |-  ( ( ( F `  x
)  e.  ( 0 [,)  +oo )  /\  0  e.  ( 0 [,)  +oo ) )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  e.  ( 0 [,)  +oo ) )
116111, 114, 115sylancl 645 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 )  e.  ( 0 [,) 
+oo ) )
117116adantlr 697 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  e.  ( 0 [,)  +oo ) )
118 eqid 2437 . . . . 5  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  =  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
119117, 118fmptd 5894 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
12048feq1d 5581 . . . 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 ) ) )
121119, 120mpbird 225 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m ) : RR --> ( 0 [,)  +oo ) )
122 elrege0 11008 . . . . . . . . . . . . 13  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
123111, 122sylib 190 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( F `  x )  e.  RR  /\  0  <_  ( F `  x
) ) )
124123simpld 447 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  RR )
125124adantlr 697 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
126125adantr 453 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  e.  RR )
127126leidd 9594 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  <_  ( F `  x )
)
128 iftrue 3746 . . . . . . . . 9  |-  ( ( F `  x )  <_  m  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
129128adantl 454 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  if (
( F `  x
)  <_  m , 
( F `  x
) ,  0 )  =  ( F `  x ) )
13049ad3antlr 713 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  m  e.  RR )
131 peano2re 9240 . . . . . . . . . . 11  |-  ( m  e.  RR  ->  (
m  +  1 )  e.  RR )
132130, 131syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( m  +  1 )  e.  RR )
133 simpr 449 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  <_  m
)
134130lep1d 9943 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  m  <_  ( m  +  1 ) )
135126, 130, 132, 133, 134letrd 9228 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  ( F `  x )  <_  (
m  +  1 ) )
136 iftrue 3746 . . . . . . . . 9  |-  ( ( F `  x )  <_  ( m  + 
1 )  ->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 )  =  ( F `
 x ) )
137135, 136syl 16 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  ( F `  x )  <_  m
)  ->  if (
( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 )  =  ( F `  x ) )
138127, 129, 1373brtr4d 4243 . . . . . . 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 ) )
139 iffalse 3747 . . . . . . . . 9  |-  ( -.  ( F `  x
)  <_  m  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  0 )
140139adantl 454 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  -.  ( F `
 x )  <_  m )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  0 )
141123simprd 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR )  ->  0  <_ 
( F `  x
) )
142 breq2 4217 . . . . . . . . . . . 12  |-  ( ( F `  x )  =  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 )  -> 
( 0  <_  ( F `  x )  <->  0  <_  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 ) ) )
143 breq2 4217 . . . . . . . . . . . 12  |-  ( 0  =  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 )  -> 
( 0  <_  0  <->  0  <_  if ( ( F `  x )  <_  ( m  + 
1 ) ,  ( F `  x ) ,  0 ) ) )
144142, 143ifboth 3771 . . . . . . . . . . 11  |-  ( ( 0  <_  ( F `  x )  /\  0  <_  0 )  ->  0  <_  if ( ( F `
 x )  <_ 
( m  +  1 ) ,  ( F `
 x ) ,  0 ) )
145141, 112, 144sylancl 645 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  0  <_  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) )
146145adantlr 697 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  0  <_  if ( ( F `
 x )  <_ 
( m  +  1 ) ,  ( F `
 x ) ,  0 ) )
147146adantr 453 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  /\  -.  ( F `
 x )  <_  m )  ->  0  <_  if ( ( F `
 x )  <_ 
( m  +  1 ) ,  ( F `
 x ) ,  0 ) )
148140, 147eqbrtrd 4233 . . . . . . 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 ) )
149138, 148pm2.61dan 768 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  if (
( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )
150149ralrimiva 2790 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) )
1511, 2ifex 3798 . . . . . . 7  |-  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 )  e.  _V
152151a1i 11 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 )  e.  _V )
153 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 ) ) )
154 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 ) ) )
15585, 117, 152, 153, 154ofrfval2 6324 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  o R  <_  ( 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 ) ) )
156150, 155mpbird 225 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  o R  <_ 
( x  e.  RR  |->  if ( ( F `  x )  <_  (
m  +  1 ) ,  ( F `  x ) ,  0 ) ) )
157 peano2nn 10013 . . . . . 6  |-  ( m  e.  NN  ->  (
m  +  1 )  e.  NN )
158157adantl 454 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  +  1 )  e.  NN )
159 breq2 4217 . . . . . . . 8  |-  ( n  =  ( m  + 
1 )  ->  (
( F `  x
)  <_  n  <->  ( F `  x )  <_  (
m  +  1 ) ) )
160159ifbid 3758 . . . . . . 7  |-  ( n  =  ( m  + 
1 )  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  =  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )
161160mpteq2dv 4297 . . . . . 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 ) ) )
16232mptex 5967 . . . . . 6  |-  ( x  e.  RR  |->  if ( ( F `  x
)  <_  ( m  +  1 ) ,  ( F `  x
) ,  0 ) )  e.  _V
163161, 31, 162fvmpt 5807 . . . . 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 ) ) )
164158, 163syl 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 ) ) )
165156, 48, 1643brtr4d 4243 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ) `  m )  o R  <_  ( ( n  e.  NN  |->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ) `  (
m  +  1 ) ) )
16668ffvelrnda 5871 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 y )  e.  RR )
16734adantl 454 . . . . . . 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 ) ) )
168167fveq1d 5731 . . . . . 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 ) )
169124leidd 9594 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  <_ 
( F `  x
) )
170 breq1 4216 . . . . . . . . . . . . . 14  |-  ( ( F `  x )  =  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  -> 
( ( F `  x )  <_  ( F `  x )  <->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
171 breq1 4216 . . . . . . . . . . . . . 14  |-  ( 0  =  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  -> 
( 0  <_  ( F `  x )  <->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) ) )
172170, 171ifboth 3771 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  <_  ( F `  x )  /\  0  <_  ( F `  x
) )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
173169, 141, 172syl2anc 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 )  <_  ( F `  x ) )
174173adantlr 697 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
175174ralrimiva 2790 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_ 
( F `  x
) )
17632a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  RR  e.  _V )
1771, 2ifex 3798 . . . . . . . . . . . 12  |-  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 )  e.  _V
178177a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  x  e.  RR )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  e.  _V )
17954feqmptd 5780 . . . . . . . . . . . 12  |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( F `
 x ) ) )
180179adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  F  =  ( x  e.  RR  |->  ( F `  x ) ) )
181176, 178, 125, 153, 180ofrfval2 6324 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  o R  <_  F  <->  A. x  e.  RR  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_ 
( F `  x
) ) )
182175, 181mpbird 225 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  o R  <_  F )
183178, 118fmptd 5894 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) : RR --> _V )
184 ffn 5592 . . . . . . . . . . 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 )
185183, 184syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )  Fn  RR )
18656adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  F  Fn  RR )
187 inidm 3551 . . . . . . . . . 10  |-  ( RR 
i^i  RR )  =  RR
188 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
) )
189 eqidd 2438 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  ( F `  y )  =  ( F `  y ) )
190185, 186, 176, 176, 187, 188, 189ofrfval 6314 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) )  o R  <_  F  <->  A. y  e.  RR  ( ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) `  y )  <_  ( F `  y ) ) )
191182, 190mpbid 203 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  A. y  e.  RR  ( ( x  e.  RR  |->  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) ) `  y )  <_  ( F `  y ) )
192191r19.21bi 2805 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  NN )  /\  y  e.  RR )  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
)  <_  ( F `  y ) )
193192an32s 781 . . . . . 6  |-  ( ( ( ph  /\  y  e.  RR )  /\  m  e.  NN )  ->  (
( x  e.  RR  |->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 ) ) `  y
)  <_  ( F `  y ) )
194168, 193eqbrtrd 4233 . . . . 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
) )
195194ralrimiva 2790 . . . 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 ) )
196 breq2 4217 . . . . . 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 ) ) )
197196ralbidv 2726 . . . . 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
) ) )
198197rspcev 3053 . . . 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 )
199166, 195, 198syl2anc 644 . . 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 )
20028fveq2d 5733 . . . . . . 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 ) ) ) )
201200cbvmptv 4301 . . . . . 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 ) ) ) )
20234fveq2d 5733 . . . . . . 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 ) ) ) )
203202mpteq2ia 4292 . . . . . 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 ) ) ) )
204201, 203eqtr4i 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 ) ) )
205204rneqi 5097 . . . 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 ) ) )
206205supeq1i 7453 . . 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* ,  <  )
20742, 110, 121, 165, 199, 206itg2mono 19646 . 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* ,  <  ) )
208 eqid 2437 . . . . . . . . . . . 12  |-  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  =  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )
20927, 208, 177fvmpt 5807 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  (
( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  m
)  =  if ( ( F `  x
)  <_  m , 
( F `  x
) ,  0 ) )
210209adantl 454 . . . . . . . . . 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 ) )
211173adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  <_  ( F `  x ) )
212210, 211eqbrtrd 4233 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  (
( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) `  m
)  <_  ( F `  x ) )
213212ralrimiva 2790 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  A. m  e.  NN  ( ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) `  m )  <_  ( F `  x ) )
2143a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  e.  _V )
215214, 208fmptd 5894 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) : NN --> _V )
216 ffn 5592 . . . . . . . . . 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 )
217215, 216syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) )  Fn  NN )
218 breq1 4216 . . . . . . . . . 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 ) ) )
219218ralrn 5874 . . . . . . . . 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 ) ) )
220217, 219syl 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 ) ) )
221213, 220mpbird 225 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  A. w  e.  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) w  <_  ( F `  x ) )
222124adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  ( F `  x )  e.  RR )
223 ifcl 3776 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  e.  RR  /\  0  e.  RR )  ->  if ( ( F `
 x )  <_  n ,  ( F `  x ) ,  0 )  e.  RR )
224222, 63, 223sylancl 645 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  n  e.  NN )  ->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 )  e.  RR )
225224, 208fmptd 5894 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) : NN --> RR )
226 frn 5598 . . . . . . . . 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 )
227225, 226syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  C_  RR )
228 1nn 10012 . . . . . . . . . 10  |-  1  e.  NN
229 fdm 5596 . . . . . . . . . . 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 )
230225, 229syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  dom  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  NN )
231228, 230syl5eleqr 2524 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  1  e. 
dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
232 n0i 3634 . . . . . . . . . 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 ) )  =  (/) )
233 dm0rn0 5087 . . . . . . . . . . 11  |-  ( dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/)  <->  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/) )
234233necon3bbii 2633 . . . . . . . . . 10  |-  ( -. 
dom  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =  (/)  <->  ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/) )
235232, 234sylib 190 . . . . . . . . 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 ) )  =/=  (/) )
236231, 235syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ran  (
n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  =/=  (/) )
237 breq2 4217 . . . . . . . . . . 11  |-  ( z  =  ( F `  x )  ->  (
w  <_  z  <->  w  <_  ( F `  x ) ) )
238237ralbidv 2726 . . . . . . . . . 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
) ) )
239238rspcev 3053 . . . . . . . . 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 )
240124, 221, 239syl2anc 644 . . . . . . . 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 )
241 suprleub 9973 . . . . . . . 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
) ) )
242227, 236, 240, 124, 241syl31anc 1188 . . . . . . 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 ) ) )
243221, 242mpbird 225 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  <_  ( F `  x )
)
244 arch 10219 . . . . . . . . 9  |-  ( ( F `  x )  e.  RR  ->  E. m  e.  NN  ( F `  x )  <  m
)
245124, 244syl 16 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  E. m  e.  NN  ( F `  x )  <  m
)
246209ad2antrl 710 . . . . . . . . . 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 ) )
247 ltle 9164 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  e.  RR  /\  m  e.  RR )  ->  ( ( F `  x )  <  m  ->  ( F `  x
)  <_  m )
)
248124, 49, 247syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  m  e.  NN )  ->  (
( F `  x
)  <  m  ->  ( F `  x )  <_  m ) )
249248impr 604 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( F `  x )  <_  m
)
250249, 128syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  if ( ( F `  x )  <_  m ,  ( F `  x ) ,  0 )  =  ( F `  x
) )
251246, 250eqtrd 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 ) )
252217adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) )  Fn  NN )
253 simprl 734 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
m  e.  NN  /\  ( F `  x )  <  m ) )  ->  m  e.  NN )
254 fnfvelrn 5868 . . . . . . . . . 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 ) ) )
255252, 253, 254syl2anc 644 . . . . . . . . 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 ) ) )
256251, 255eqeltrrd 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 ) ) )
257245, 256rexlimddv 2835 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e. 
ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) )
258 suprub 9970 . . . . . . 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 ,  <  ) )
259227, 236, 240, 257, 258syl31anc 1188 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  <_  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) )
260 suprcl 9969 . . . . . . . 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 )
261227, 236, 240, 260syl3anc 1185 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  e.  RR )
262261, 124letri3d 9216 . . . . . 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 ,  <  ) ) ) )
263243, 259, 262mpbir2and 890 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x )  <_  n ,  ( F `  x ) ,  0 ) ) ,  RR ,  <  )  =  ( F `  x ) )
264263mpteq2dva 4296 . . . 4  |-  ( ph  ->  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) )  =  ( x  e.  RR  |->  ( F `  x ) ) )
265264, 179eqtr4d 2472 . . 3  |-  ( ph  ->  ( x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) )  =  F )
266265fveq2d 5733 . 2  |-  ( ph  ->  ( S.2 `  (
x  e.  RR  |->  sup ( ran  ( n  e.  NN  |->  if ( ( F `  x
)  <_  n , 
( F `  x
) ,  0 ) ) ,  RR ,  <  ) ) )  =  ( S.2 `  F
) )
267207, 266eqtr3d 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 set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726    =/= wne 2600   A.wral 2706   E.wrex 2707   _Vcvv 2957    \ cdif 3318    C_ wss 3321   (/)c0 3629   ifcif 3740   class class class wbr 4213    e. cmpt 4267   `'ccnv 4878   dom cdm 4879   ran crn 4880    |` cres 4881   "cima 4882    Fn wfn 5450   -->wf 5451   ` cfv 5455  (class class class)co 6082    o Rcofr 6305   supcsup 7446   RRcr 8990   0cc0 8991   1c1 8992    + caddc 8994    +oocpnf 9118   RR*cxr 9120    < clt 9121    <_ cle 9122   NNcn 10001   (,)cioo 10917   [,)cico 10919   volcvol 19361  MblFncmbf 19507   S.2citg2 19509
This theorem is referenced by:  itg2cn  19656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cc 8316  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069  ax-addf 9070
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-disj 4184  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6306  df-ofr 6307  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-2o 6726  df-oadd 6729  df-omul 6730  df-er 6906  df-map 7021  df-pm 7022  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-fi 7417  df-sup 7447  df-oi 7480  df-card 7827  df-acn 7830  df-cda 8049  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-n0 10223  df-z 10284  df-uz 10490  df-q 10576  df-rp 10614  df-xneg 10711  df-xadd 10712  df-xmul 10713  df-ioo 10921  df-ioc 10922  df-ico 10923  df-icc 10924  df-fz 11045  df-fzo 11137  df-fl 11203  df-seq 11325  df-exp 11384  df-hash 11620  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-clim 12283  df-rlim 12284  df-sum 12481  df-rest 13651  df-topgen 13668  df-psmet 16695  df-xmet 16696  df-met 16697  df-bl 16698  df-mopn 16699  df-top 16964  df-bases 16966  df-topon 16967  df-cmp 17451  df-ovol 19362  df-vol 19363  df-mbf 19513  df-itg1 19514  df-itg2 19515
  Copyright terms: Public domain W3C validator