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 
|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
Assertion itg2l 
|- ( A e. L <-> E. g e. dom S.1 ( g oR <_ F /\ A = ( S.1 ` g ) ) )

Proof

Step Hyp Ref Expression
1 itg2val.1 
 |-  L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
2 1 eleq2i 
 |-  ( A e. L <-> A e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } )
3 simpr 
 |-  ( ( g oR <_ F /\ A = ( S.1 ` g ) ) -> A = ( S.1 ` g ) )
4 fvex 
 |-  ( S.1 ` g ) e. _V
5 3 4 eqeltrdi 
 |-  ( ( g oR <_ F /\ A = ( S.1 ` g ) ) -> A e. _V )
6 5 rexlimivw 
 |-  ( E. g e. dom S.1 ( g oR <_ F /\ A = ( S.1 ` g ) ) -> A e. _V )
7 eqeq1 
 |-  ( x = A -> ( x = ( S.1 ` g ) <-> A = ( S.1 ` g ) ) )
8 7 anbi2d 
 |-  ( x = A -> ( ( g oR <_ F /\ x = ( S.1 ` g ) ) <-> ( g oR <_ F /\ A = ( S.1 ` g ) ) ) )
9 8 rexbidv 
 |-  ( x = A -> ( E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) <-> E. g e. dom S.1 ( g oR <_ F /\ A = ( S.1 ` g ) ) ) )
10 6 9 elab3 
 |-  ( A e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } <-> E. g e. dom S.1 ( g oR <_ F /\ A = ( S.1 ` g ) ) )
11 2 10 bitri 
 |-  ( A e. L <-> E. g e. dom S.1 ( g oR <_ F /\ A = ( S.1 ` g ) ) )