Theorem itg2l

Description: Elementhood in the set L of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypothesis	itg2val.1	⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
Assertion	itg2l	⊢ ( 𝐴 ∈ 𝐿 ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		itg2val.1	⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2	1	eleq2i	⊢ ( 𝐴 ∈ 𝐿 ↔ 𝐴 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } )
3		simpr	⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) → 𝐴 = ( ∫1 ‘ 𝑔 ) )
4		fvex	⊢ ( ∫1 ‘ 𝑔 ) ∈ V
5	3 4	eqeltrdi	⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) → 𝐴 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) → 𝐴 ∈ V )
7		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( ∫1 ‘ 𝑔 ) ↔ 𝐴 = ( ∫1 ‘ 𝑔 ) ) )
8	7	anbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) )
9	8	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) )
10	6 9	elab3	⊢ ( 𝐴 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) )
11	2 10	bitri	⊢ ( 𝐴 ∈ 𝐿 ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) )