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

Metamath Proof Explorer

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*