Metamath Proof Explorer

Theorem marypha2lem3

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypothesis marypha2lem.t 
|- T = U_ x e. A ( { x } X. ( F ` x ) )
Assertion marypha2lem3 
|- ( ( F Fn A /\ G Fn A ) -> ( G C_ T <-> A. x e. A ( G ` x ) e. ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 marypha2lem.t 
 |-  T = U_ x e. A ( { x } X. ( F ` x ) )
2 dffn5 
 |-  ( G Fn A <-> G = ( x e. A |-> ( G ` x ) ) )
3 2 biimpi 
 |-  ( G Fn A -> G = ( x e. A |-> ( G ` x ) ) )
4 3 adantl 
 |-  ( ( F Fn A /\ G Fn A ) -> G = ( x e. A |-> ( G ` x ) ) )
5 df-mpt 
 |-  ( x e. A |-> ( G ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) }
6 4 5 eqtrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> G = { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) } )
7 1 marypha2lem2 
 |-  T = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
8 7 a1i 
 |-  ( ( F Fn A /\ G Fn A ) -> T = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } )
9 6 8 sseq12d 
 |-  ( ( F Fn A /\ G Fn A ) -> ( G C_ T <-> { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) } C_ { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } ) )
10 ssopab2bw 
 |-  ( { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) } C_ { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } <-> A. x A. y ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) )
11 9 10 bitrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> ( G C_ T <-> A. x A. y ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) ) )
12 19.21v 
 |-  ( A. y ( x e. A -> ( y = ( G ` x ) -> y e. ( F ` x ) ) ) <-> ( x e. A -> A. y ( y = ( G ` x ) -> y e. ( F ` x ) ) ) )
13 imdistan 
 |-  ( ( x e. A -> ( y = ( G ` x ) -> y e. ( F ` x ) ) ) <-> ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) )
14 13 albii 
 |-  ( A. y ( x e. A -> ( y = ( G ` x ) -> y e. ( F ` x ) ) ) <-> A. y ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) )
15 fvex 
 |-  ( G ` x ) e. _V
16 eleq1 
 |-  ( y = ( G ` x ) -> ( y e. ( F ` x ) <-> ( G ` x ) e. ( F ` x ) ) )
17 15 16 ceqsalv 
 |-  ( A. y ( y = ( G ` x ) -> y e. ( F ` x ) ) <-> ( G ` x ) e. ( F ` x ) )
18 17 imbi2i 
 |-  ( ( x e. A -> A. y ( y = ( G ` x ) -> y e. ( F ` x ) ) ) <-> ( x e. A -> ( G ` x ) e. ( F ` x ) ) )
19 12 14 18 3bitr3i 
 |-  ( A. y ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) <-> ( x e. A -> ( G ` x ) e. ( F ` x ) ) )
20 19 albii 
 |-  ( A. x A. y ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) <-> A. x ( x e. A -> ( G ` x ) e. ( F ` x ) ) )
21 df-ral 
 |-  ( A. x e. A ( G ` x ) e. ( F ` x ) <-> A. x ( x e. A -> ( G ` x ) e. ( F ` x ) ) )
22 20 21 bitr4i 
 |-  ( A. x A. y ( ( x e. A /\ y = ( G ` x ) ) -> ( x e. A /\ y e. ( F ` x ) ) ) <-> A. x e. A ( G ` x ) e. ( F ` x ) )
23 11 22 bitrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> ( G C_ T <-> A. x e. A ( G ` x ) e. ( F ` x ) ) )