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* )