Theorem itg2lcl

Description: The set of lower sums is a set of extended reals. (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	itg2lcl	|- L C_ 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		itg1cl	|- ( g e. dom S.1 -> ( S.1 ` g ) e. RR )
3	2	rexrd	|- ( g e. dom S.1 -> ( S.1 ` g ) e. RR* )
4		simpr	|- ( ( g oR <_ F /\ x = ( S.1 ` g ) ) -> x = ( S.1 ` g ) )
5	4	eleq1d	|- ( ( g oR <_ F /\ x = ( S.1 ` g ) ) -> ( x e. RR* <-> ( S.1 ` g ) e. RR* ) )
6	3 5	syl5ibrcom	|- ( g e. dom S.1 -> ( ( g oR <_ F /\ x = ( S.1 ` g ) ) -> x e. RR* ) )
7	6	rexlimiv	|- ( E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) -> x e. RR* )
8	7	abssi	|- { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR*
9	1 8	eqsstri	|- L C_ RR*