Theorem itg2ub

Description: The integral of a nonnegative real function F is an upper bound on the integrals of all simple functions G dominated by F . (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	itg2ub	|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ ( S.2 ` F ) )

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	itg2lcl	|- { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR*
3	1	itg2lr	|- ( ( G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } )
4	3	3adant1	|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } )
5		supxrub	|- ( ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR* /\ ( S.1 ` G ) e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } ) -> ( S.1 ` G ) <_ sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
6	2 4 5	sylancr	|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
7	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* , < ) )
8	7	3ad2ant1	|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.2 ` F ) = sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
9	6 8	breqtrrd	|- ( ( F : RR --> ( 0 [,] +oo ) /\ G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) <_ ( S.2 ` F ) )