This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2cl

Description: The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2cl 
|- ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { 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 ) ) }
2 1 itg2val 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
3 1 itg2lcl 
 |-  { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR*
4 supxrcl 
 |-  ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR* -> sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) e. RR* )
5 3 4 ax-mp 
 |-  sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) e. RR*
6 2 5 eqeltrdi 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) e. RR* )