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

Metamath Proof Explorer

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 )