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

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