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	⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
Assertion	itg2lcl	⊢ 𝐿 ⊆ ℝ*

Proof

Step	Hyp	Ref	Expression
1		itg2val.1	⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2		itg1cl	⊢ ( 𝑔 ∈ dom ∫1 → ( ∫1 ‘ 𝑔 ) ∈ ℝ )
3	2	rexrd	⊢ ( 𝑔 ∈ dom ∫1 → ( ∫1 ‘ 𝑔 ) ∈ ℝ* )
4		simpr	⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → 𝑥 = ( ∫1 ‘ 𝑔 ) )
5	4	eleq1d	⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → ( 𝑥 ∈ ℝ* ↔ ( ∫1 ‘ 𝑔 ) ∈ ℝ* ) )
6	3 5	syl5ibrcom	⊢ ( 𝑔 ∈ dom ∫1 → ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → 𝑥 ∈ ℝ* ) )
7	6	rexlimiv	⊢ ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) → 𝑥 ∈ ℝ* )
8	7	abssi	⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ⊆ ℝ*
9	1 8	eqsstri	⊢ 𝐿 ⊆ ℝ*