Theorem itg2lr

Description: Sufficient condition for elementhood in the set L . (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	itg2lr	|- ( ( G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. L )

Proof

Step	Hyp	Ref	Expression
1		itg2val.1	|- L = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
2		eqid	|- ( S.1 ` G ) = ( S.1 ` G )
3		breq1	|- ( g = G -> ( g oR <_ F <-> G oR <_ F ) )
4		fveq2	|- ( g = G -> ( S.1 ` g ) = ( S.1 ` G ) )
5	4	eqeq2d	|- ( g = G -> ( ( S.1 ` G ) = ( S.1 ` g ) <-> ( S.1 ` G ) = ( S.1 ` G ) ) )
6	3 5	anbi12d	|- ( g = G -> ( ( g oR <_ F /\ ( S.1 ` G ) = ( S.1 ` g ) ) <-> ( G oR <_ F /\ ( S.1 ` G ) = ( S.1 ` G ) ) ) )
7	6	rspcev	|- ( ( G e. dom S.1 /\ ( G oR <_ F /\ ( S.1 ` G ) = ( S.1 ` G ) ) ) -> E. g e. dom S.1 ( g oR <_ F /\ ( S.1 ` G ) = ( S.1 ` g ) ) )
8	2 7	mpanr2	|- ( ( G e. dom S.1 /\ G oR <_ F ) -> E. g e. dom S.1 ( g oR <_ F /\ ( S.1 ` G ) = ( S.1 ` g ) ) )
9	1	itg2l	|- ( ( S.1 ` G ) e. L <-> E. g e. dom S.1 ( g oR <_ F /\ ( S.1 ` G ) = ( S.1 ` g ) ) )
10	8 9	sylibr	|- ( ( G e. dom S.1 /\ G oR <_ F ) -> ( S.1 ` G ) e. L )