Metamath Proof Explorer

Theorem itg2val

Description: Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypothesis itg2val.1 
|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
Assertion itg2val 
|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( L , RR* , < ) )

Proof

Step Hyp Ref Expression
1 itg2val.1 
 |-  L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
2 xrltso 
 |-  < Or RR*
3 2 supex 
 |-  sup ( L , RR* , < ) e. _V
4 reex 
 |-  RR e. _V
5 ovex 
 |-  ( 0 [,] +oo ) e. _V
6 breq2 
 |-  ( f = F -> ( g oR <_ f <-> g oR <_ F ) )
7 6 anbi1d 
 |-  ( f = F -> ( ( g oR <_ f /\ x = ( S.1 ` g ) ) <-> ( g oR <_ F /\ x = ( S.1 ` g ) ) ) )
8 7 rexbidv 
 |-  ( f = F -> ( E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) <-> E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) ) )
9 8 abbidv 
 |-  ( f = F -> { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } )
10 9 1 eqtr4di 
 |-  ( f = F -> { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } = L )
11 10 supeq1d 
 |-  ( f = F -> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) = sup ( L , RR* , < ) )
12 df-itg2 
 |-  S.2 = ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )
13 3 4 5 11 12 fvmptmap 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( L , RR* , < ) )