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

Metamath Proof Explorer

Theorem uncfcurf

Description: Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses uncfcurf.g 
|- G = ( <. C , D >. curryF F )
uncfcurf.c 
|- ( ph -> C e. Cat )
uncfcurf.d 
|- ( ph -> D e. Cat )
uncfcurf.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
Assertion uncfcurf 
|- ( ph -> ( <" C D E "> uncurryF G ) = F )

Proof

Step Hyp Ref Expression
1 uncfcurf.g 
 |-  G = ( <. C , D >. curryF F )
2 uncfcurf.c 
 |-  ( ph -> C e. Cat )
3 uncfcurf.d 
 |-  ( ph -> D e. Cat )
4 uncfcurf.f 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
5 eqid 
 |-  ( <" C D E "> uncurryF G ) = ( <" C D E "> uncurryF G )
6 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> D e. Cat )
7 funcrcl 
 |-  ( F e. ( ( C Xc. D ) Func E ) -> ( ( C Xc. D ) e. Cat /\ E e. Cat ) )
8 4 7 syl 
 |-  ( ph -> ( ( C Xc. D ) e. Cat /\ E e. Cat ) )
9 8 simprd 
 |-  ( ph -> E e. Cat )
10 9 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> E e. Cat )
11 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
12 1 11 2 3 4 curfcl 
 |-  ( ph -> G e. ( C Func ( D FuncCat E ) ) )
13 12 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> G e. ( C Func ( D FuncCat E ) ) )
14 eqid 
 |-  ( Base ` C ) = ( Base ` C )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` C ) )
17 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
18 5 6 10 13 14 15 16 17 uncf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) )
19 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> C e. Cat )
20 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> F e. ( ( C Xc. D ) Func E ) )
21 eqid 
 |-  ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` x )
22 1 14 19 6 20 15 16 21 17 curf11 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) = ( x ( 1st ` F ) y ) )
23 18 22 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( x ( 1st ` F ) y ) )
24 23 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` D ) ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( x ( 1st ` F ) y ) )
25 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
26 25 14 15 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( C Xc. D ) )
27 eqid 
 |-  ( Base ` E ) = ( Base ` E )
28 relfunc 
 |-  Rel ( ( C Xc. D ) Func E )
29 5 3 9 12 uncfcl 
 |-  ( ph -> ( <" C D E "> uncurryF G ) e. ( ( C Xc. D ) Func E ) )
30 1st2ndbr 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ ( <" C D E "> uncurryF G ) e. ( ( C Xc. D ) Func E ) ) -> ( 1st ` ( <" C D E "> uncurryF G ) ) ( ( C Xc. D ) Func E ) ( 2nd ` ( <" C D E "> uncurryF G ) ) )
31 28 29 30 sylancr 
 |-  ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) ( ( C Xc. D ) Func E ) ( 2nd ` ( <" C D E "> uncurryF G ) ) )
32 26 27 31 funcf1 
 |-  ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` E ) )
33 32 ffnd 
 |-  ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) Fn ( ( Base ` C ) X. ( Base ` D ) ) )
34 1st2ndbr 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ F e. ( ( C Xc. D ) Func E ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
35 28 4 34 sylancr 
 |-  ( ph -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
36 26 27 35 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` E ) )
37 36 ffnd 
 |-  ( ph -> ( 1st ` F ) Fn ( ( Base ` C ) X. ( Base ` D ) ) )
38 eqfnov2 
 |-  ( ( ( 1st ` ( <" C D E "> uncurryF G ) ) Fn ( ( Base ` C ) X. ( Base ` D ) ) /\ ( 1st ` F ) Fn ( ( Base ` C ) X. ( Base ` D ) ) ) -> ( ( 1st ` ( <" C D E "> uncurryF G ) ) = ( 1st ` F ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` D ) ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( x ( 1st ` F ) y ) ) )
39 33 37 38 syl2anc 
 |-  ( ph -> ( ( 1st ` ( <" C D E "> uncurryF G ) ) = ( 1st ` F ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` D ) ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( x ( 1st ` F ) y ) ) )
40 24 39 mpbird 
 |-  ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) = ( 1st ` F ) )
41 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> D e. Cat )
42 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> E e. Cat )
43 12 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> G e. ( C Func ( D FuncCat E ) ) )
44 16 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> x e. ( Base ` C ) )
45 44 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> x e. ( Base ` C ) )
46 17 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
47 46 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> y e. ( Base ` D ) )
48 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
49 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
50 simprl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> z e. ( Base ` C ) )
51 50 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> z e. ( Base ` C ) )
52 simprr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> w e. ( Base ` D ) )
53 52 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> w e. ( Base ` D ) )
54 simprl 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> f e. ( x ( Hom ` C ) z ) )
55 simprr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> g e. ( y ( Hom ` D ) w ) )
56 5 41 42 43 14 15 45 47 48 49 51 53 54 55 uncf2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( f ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) g ) = ( ( ( ( x ( 2nd ` G ) z ) ` f ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) w ) ` g ) ) )
57 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> C e. Cat )
58 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> F e. ( ( C Xc. D ) Func E ) )
59 1 14 57 41 58 15 45 21 47 curf11 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) = ( x ( 1st ` F ) y ) )
60 df-ov 
 |-  ( x ( 1st ` F ) y ) = ( ( 1st ` F ) ` <. x , y >. )
61 59 60 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) = ( ( 1st ` F ) ` <. x , y >. ) )
62 1 14 57 41 58 15 45 21 53 curf11 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) = ( x ( 1st ` F ) w ) )
63 df-ov 
 |-  ( x ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. x , w >. )
64 62 63 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) = ( ( 1st ` F ) ` <. x , w >. ) )
65 61 64 opeq12d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) >. = <. ( ( 1st ` F ) ` <. x , y >. ) , ( ( 1st ` F ) ` <. x , w >. ) >. )
66 eqid 
 |-  ( ( 1st ` G ) ` z ) = ( ( 1st ` G ) ` z )
67 1 14 57 41 58 15 51 66 53 curf11 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) = ( z ( 1st ` F ) w ) )
68 df-ov 
 |-  ( z ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. z , w >. )
69 67 68 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) = ( ( 1st ` F ) ` <. z , w >. ) )
70 65 69 oveq12d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) = ( <. ( ( 1st ` F ) ` <. x , y >. ) , ( ( 1st ` F ) ` <. x , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) )
71 eqid 
 |-  ( Id ` D ) = ( Id ` D )
72 eqid 
 |-  ( ( x ( 2nd ` G ) z ) ` f ) = ( ( x ( 2nd ` G ) z ) ` f )
73 1 14 57 41 58 15 48 71 45 51 54 72 53 curf2val 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( ( x ( 2nd ` G ) z ) ` f ) ` w ) = ( f ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) )
74 df-ov 
 |-  ( f ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) = ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. )
75 73 74 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( ( x ( 2nd ` G ) z ) ` f ) ` w ) = ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. ) )
76 eqid 
 |-  ( Id ` C ) = ( Id ` C )
77 1 14 57 41 58 15 45 21 47 49 76 53 55 curf12 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) w ) ` g ) = ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , w >. ) g ) )
78 df-ov 
 |-  ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , w >. ) g ) = ( ( <. x , y >. ( 2nd ` F ) <. x , w >. ) ` <. ( ( Id ` C ) ` x ) , g >. )
79 77 78 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) w ) ` g ) = ( ( <. x , y >. ( 2nd ` F ) <. x , w >. ) ` <. ( ( Id ` C ) ` x ) , g >. ) )
80 70 75 79 oveq123d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( ( ( x ( 2nd ` G ) z ) ` f ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) w ) ` g ) ) = ( ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. ) ( <. ( ( 1st ` F ) ` <. x , y >. ) , ( ( 1st ` F ) ` <. x , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) ( ( <. x , y >. ( 2nd ` F ) <. x , w >. ) ` <. ( ( Id ` C ) ` x ) , g >. ) ) )
81 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
82 eqid 
 |-  ( comp ` ( C Xc. D ) ) = ( comp ` ( C Xc. D ) )
83 eqid 
 |-  ( comp ` E ) = ( comp ` E )
84 35 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
85 84 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
86 opelxpi 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
87 86 ad2antlr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
88 87 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
89 45 53 opelxpd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. x , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
90 opelxpi 
 |-  ( ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) -> <. z , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
91 90 adantl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> <. z , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
92 91 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. z , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
93 14 48 76 57 45 catidcl 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
94 93 55 opelxpd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` x ) , g >. e. ( ( x ( Hom ` C ) x ) X. ( y ( Hom ` D ) w ) ) )
95 25 14 15 48 49 45 47 45 53 81 xpchom2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , w >. ) = ( ( x ( Hom ` C ) x ) X. ( y ( Hom ` D ) w ) ) )
96 94 95 eleqtrrd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` x ) , g >. e. ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , w >. ) )
97 15 49 71 41 53 catidcl 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( Id ` D ) ` w ) e. ( w ( Hom ` D ) w ) )
98 54 97 opelxpd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. f , ( ( Id ` D ) ` w ) >. e. ( ( x ( Hom ` C ) z ) X. ( w ( Hom ` D ) w ) ) )
99 25 14 15 48 49 45 53 51 53 81 xpchom2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( <. x , w >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) = ( ( x ( Hom ` C ) z ) X. ( w ( Hom ` D ) w ) ) )
100 98 99 eleqtrrd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> <. f , ( ( Id ` D ) ` w ) >. e. ( <. x , w >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) )
101 26 81 82 83 85 88 89 92 96 100 funcco 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ` ( <. f , ( ( Id ` D ) ` w ) >. ( <. <. x , y >. , <. x , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. ( ( Id ` C ) ` x ) , g >. ) ) = ( ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. ) ( <. ( ( 1st ` F ) ` <. x , y >. ) , ( ( 1st ` F ) ` <. x , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) ( ( <. x , y >. ( 2nd ` F ) <. x , w >. ) ` <. ( ( Id ` C ) ` x ) , g >. ) ) )
102 eqid 
 |-  ( comp ` C ) = ( comp ` C )
103 eqid 
 |-  ( comp ` D ) = ( comp ` D )
104 25 14 15 48 49 45 47 45 53 102 103 82 51 53 93 55 54 97 xpcco2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( <. f , ( ( Id ` D ) ` w ) >. ( <. <. x , y >. , <. x , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. ( ( Id ` C ) ` x ) , g >. ) = <. ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) , ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) >. )
105 104 fveq2d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ` ( <. f , ( ( Id ` D ) ` w ) >. ( <. <. x , y >. , <. x , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. ( ( Id ` C ) ` x ) , g >. ) ) = ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ` <. ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) , ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) >. ) )
106 df-ov 
 |-  ( ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) ) = ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ` <. ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) , ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) >. )
107 105 106 eqtr4di 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ` ( <. f , ( ( Id ` D ) ` w ) >. ( <. <. x , y >. , <. x , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. ( ( Id ` C ) ` x ) , g >. ) ) = ( ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) ) )
108 14 48 76 57 45 102 51 54 catrid 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) = f )
109 15 49 71 41 47 103 53 55 catlid 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) = g )
110 108 109 oveq12d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( f ( <. x , x >. ( comp ` C ) z ) ( ( Id ` C ) ` x ) ) ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ( ( ( Id ` D ) ` w ) ( <. y , w >. ( comp ` D ) w ) g ) ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) )
111 107 110 eqtrd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ` ( <. f , ( ( Id ` D ) ` w ) >. ( <. <. x , y >. , <. x , w >. >. ( comp ` ( C Xc. D ) ) <. z , w >. ) <. ( ( Id ` C ) ` x ) , g >. ) ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) )
112 80 101 111 3eqtr2d 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( ( ( ( x ( 2nd ` G ) z ) ` f ) ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) , ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` z ) ) ` w ) ) ( ( y ( 2nd ` ( ( 1st ` G ) ` x ) ) w ) ` g ) ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) )
113 56 112 eqtrd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) /\ ( f e. ( x ( Hom ` C ) z ) /\ g e. ( y ( Hom ` D ) w ) ) ) -> ( f ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) g ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) )
114 113 ralrimivva 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> A. f e. ( x ( Hom ` C ) z ) A. g e. ( y ( Hom ` D ) w ) ( f ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) g ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) )
115 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
116 31 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( 1st ` ( <" C D E "> uncurryF G ) ) ( ( C Xc. D ) Func E ) ( 2nd ` ( <" C D E "> uncurryF G ) ) )
117 26 81 115 116 87 91 funcf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) : ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) --> ( ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. z , w >. ) ) )
118 25 14 15 48 49 44 46 50 52 81 xpchom2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) = ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) )
119 118 feq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) : ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) --> ( ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. z , w >. ) ) <-> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) : ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) --> ( ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. z , w >. ) ) ) )
120 117 119 mpbid 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) : ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) --> ( ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. z , w >. ) ) )
121 120 ffnd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) Fn ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) )
122 26 81 115 84 87 91 funcf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` F ) <. z , w >. ) : ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) --> ( ( ( 1st ` F ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) )
123 118 feq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( ( <. x , y >. ( 2nd ` F ) <. z , w >. ) : ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. z , w >. ) --> ( ( ( 1st ` F ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) <-> ( <. x , y >. ( 2nd ` F ) <. z , w >. ) : ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) --> ( ( ( 1st ` F ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) ) )
124 122 123 mpbid 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` F ) <. z , w >. ) : ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) --> ( ( ( 1st ` F ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) )
125 124 ffnd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` F ) <. z , w >. ) Fn ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) )
126 eqfnov2 
 |-  ( ( ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) Fn ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) /\ ( <. x , y >. ( 2nd ` F ) <. z , w >. ) Fn ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) ) -> ( ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) <-> A. f e. ( x ( Hom ` C ) z ) A. g e. ( y ( Hom ` D ) w ) ( f ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) g ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) ) )
127 121 125 126 syl2anc 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) <-> A. f e. ( x ( Hom ` C ) z ) A. g e. ( y ( Hom ` D ) w ) ( f ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) g ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) ) )
128 114 127 mpbird 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) )
129 128 ralrimivva 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) )
130 129 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` D ) A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) )
131 oveq2 
 |-  ( v = <. z , w >. -> ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) )
132 oveq2 
 |-  ( v = <. z , w >. -> ( u ( 2nd ` F ) v ) = ( u ( 2nd ` F ) <. z , w >. ) )
133 131 132 eqeq12d 
 |-  ( v = <. z , w >. -> ( ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) <-> ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( u ( 2nd ` F ) <. z , w >. ) ) )
134 133 ralxp 
 |-  ( A. v e. ( ( Base ` C ) X. ( Base ` D ) ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) <-> A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( u ( 2nd ` F ) <. z , w >. ) )
135 oveq1 
 |-  ( u = <. x , y >. -> ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) )
136 oveq1 
 |-  ( u = <. x , y >. -> ( u ( 2nd ` F ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) )
137 135 136 eqeq12d 
 |-  ( u = <. x , y >. -> ( ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( u ( 2nd ` F ) <. z , w >. ) <-> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ) )
138 137 2ralbidv 
 |-  ( u = <. x , y >. -> ( A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( u ( 2nd ` F ) <. z , w >. ) <-> A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ) )
139 134 138 bitrid 
 |-  ( u = <. x , y >. -> ( A. v e. ( ( Base ` C ) X. ( Base ` D ) ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) <-> A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) ) )
140 139 ralxp 
 |-  ( A. u e. ( ( Base ` C ) X. ( Base ` D ) ) A. v e. ( ( Base ` C ) X. ( Base ` D ) ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` D ) A. z e. ( Base ` C ) A. w e. ( Base ` D ) ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) )
141 130 140 sylibr 
 |-  ( ph -> A. u e. ( ( Base ` C ) X. ( Base ` D ) ) A. v e. ( ( Base ` C ) X. ( Base ` D ) ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) )
142 26 31 funcfn2 
 |-  ( ph -> ( 2nd ` ( <" C D E "> uncurryF G ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) )
143 26 35 funcfn2 
 |-  ( ph -> ( 2nd ` F ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) )
144 eqfnov2 
 |-  ( ( ( 2nd ` ( <" C D E "> uncurryF G ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) /\ ( 2nd ` F ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) ) -> ( ( 2nd ` ( <" C D E "> uncurryF G ) ) = ( 2nd ` F ) <-> A. u e. ( ( Base ` C ) X. ( Base ` D ) ) A. v e. ( ( Base ` C ) X. ( Base ` D ) ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) ) )
145 142 143 144 syl2anc 
 |-  ( ph -> ( ( 2nd ` ( <" C D E "> uncurryF G ) ) = ( 2nd ` F ) <-> A. u e. ( ( Base ` C ) X. ( Base ` D ) ) A. v e. ( ( Base ` C ) X. ( Base ` D ) ) ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` F ) v ) ) )
146 141 145 mpbird 
 |-  ( ph -> ( 2nd ` ( <" C D E "> uncurryF G ) ) = ( 2nd ` F ) )
147 40 146 opeq12d 
 |-  ( ph -> <. ( 1st ` ( <" C D E "> uncurryF G ) ) , ( 2nd ` ( <" C D E "> uncurryF G ) ) >. = <. ( 1st ` F ) , ( 2nd ` F ) >. )
148 1st2nd 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ ( <" C D E "> uncurryF G ) e. ( ( C Xc. D ) Func E ) ) -> ( <" C D E "> uncurryF G ) = <. ( 1st ` ( <" C D E "> uncurryF G ) ) , ( 2nd ` ( <" C D E "> uncurryF G ) ) >. )
149 28 29 148 sylancr 
 |-  ( ph -> ( <" C D E "> uncurryF G ) = <. ( 1st ` ( <" C D E "> uncurryF G ) ) , ( 2nd ` ( <" C D E "> uncurryF G ) ) >. )
150 1st2nd 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ F e. ( ( C Xc. D ) Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
151 28 4 150 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
152 147 149 151 3eqtr4d 
 |-  ( ph -> ( <" C D E "> uncurryF G ) = F )