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