# 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> C e. Cat )`
` |-  ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> x e. ( Base ` C ) )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 syl6eq
` |-  ( ( ( ( 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 syl6eq
` |-  ( ( ( ( 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 syl6eq
` |-  ( ( ( ( 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 syl6eq
` |-  ( ( ( ( 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 syl6eq
` |-  ( ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( ( 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 syl6eqr
` |-  ( ( ( ( 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 )`
` |-  ( ( ( 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 syl5bb
` |-  ( 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 )`