Metamath Proof Explorer


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𝑔 ) ) )