Theorem uncfcurf 16879

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

Hypotheses

Ref	Expression
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 X.c D ) Func E ) )

Assertion

Ref	Expression
uncfcurf	|- ( ph -> ( <" C D E "> uncurryF G ) = F )

Proof of Theorem uncfcurf

Dummy variables f g u v w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . . . . . 7 |- ( <" C D E "> uncurryF G ) = ( <" C D E "> uncurryF G )
2		uncfcurf.d	. . . . . . . 8 |- ( ph -> D e. Cat )
3	2	adantr 481	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> D e. Cat )
4		uncfcurf.f	. . . . . . . . . 10 |- ( ph -> F e. ( ( C X.c D ) Func E ) )
5		funcrcl 16523	. . . . . . . . . 10 |- ( F e. ( ( C X.c D ) Func E ) -> ( ( C X.c D ) e. Cat /\ E e. Cat ) )
6	4, 5	syl 17	. . . . . . . . 9 |- ( ph -> ( ( C X.c D ) e. Cat /\ E e. Cat ) )
7	6	simprd 479	. . . . . . . 8 |- ( ph -> E e. Cat )
8	7	adantr 481	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> E e. Cat )
9		uncfcurf.g	. . . . . . . . 9 |- G = ( <. C , D >. curryF F )
10		eqid 2622	. . . . . . . . 9 |- ( D FuncCat E ) = ( D FuncCat E )
11		uncfcurf.c	. . . . . . . . 9 |- ( ph -> C e. Cat )
12	9, 10, 11, 2, 4	curfcl 16872	. . . . . . . 8 |- ( ph -> G e. ( C Func ( D FuncCat E ) ) )
13	12	adantr 481	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> G e. ( C Func ( D FuncCat E ) ) )
14		eqid 2622	. . . . . . 7 |- ( Base ` C ) = ( Base ` C )
15		eqid 2622	. . . . . . 7 |- ( Base ` D ) = ( Base ` D )
16		simprl 794	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` C ) )
17		simprr 796	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
18	1, 3, 8, 13, 14, 15, 16, 17	uncf1 16876	. . . . . 6 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) )
19	11	adantr 481	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> C e. Cat )
20	4	adantr 481	. . . . . . 7 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> F e. ( ( C X.c D ) Func E ) )
21		eqid 2622	. . . . . . 7 |- ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` x )
22	9, 14, 19, 3, 20, 15, 16, 21, 17	curf11 16866	. . . . . 6 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` x ) ) ` y ) = ( x ( 1st ` F ) y ) )
23	18, 22	eqtrd 2656	. . . . 5 |- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) -> ( x ( 1st ` ( <" C D E "> uncurryF G ) ) y ) = ( x ( 1st ` F ) y ) )
24	23	ralrimivva 2971	. . . 4 |- ( 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 2622	. . . . . . . 8 |- ( C X.c D ) = ( C X.c D )
26	25, 14, 15	xpcbas 16818	. . . . . . 7 |- ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( C X.c D ) )
27		eqid 2622	. . . . . . 7 |- ( Base ` E ) = ( Base ` E )
28		relfunc 16522	. . . . . . . 8 |- Rel ( ( C X.c D ) Func E )
29	1, 2, 7, 12	uncfcl 16875	. . . . . . . 8 |- ( ph -> ( <" C D E "> uncurryF G ) e. ( ( C X.c D ) Func E ) )
30		1st2ndbr 7217	. . . . . . . 8 |- ( ( Rel ( ( C X.c D ) Func E ) /\ ( <" C D E "> uncurryF G ) e. ( ( C X.c D ) Func E ) ) -> ( 1st ` ( <" C D E "> uncurryF G ) ) ( ( C X.c D ) Func E ) ( 2nd ` ( <" C D E "> uncurryF G ) ) )
31	28, 29, 30	sylancr 695	. . . . . . 7 |- ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) ( ( C X.c D ) Func E ) ( 2nd ` ( <" C D E "> uncurryF G ) ) )
32	26, 27, 31	funcf1 16526	. . . . . 6 |- ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` E ) )
33		ffn 6045	. . . . . 6 |- ( ( 1st ` ( <" C D E "> uncurryF G ) ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` E ) -> ( 1st ` ( <" C D E "> uncurryF G ) ) Fn ( ( Base ` C ) X. ( Base ` D ) ) )
34	32, 33	syl 17	. . . . 5 |- ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) Fn ( ( Base ` C ) X. ( Base ` D ) ) )
35		1st2ndbr 7217	. . . . . . . 8 |- ( ( Rel ( ( C X.c D ) Func E ) /\ F e. ( ( C X.c D ) Func E ) ) -> ( 1st ` F ) ( ( C X.c D ) Func E ) ( 2nd ` F ) )
36	28, 4, 35	sylancr 695	. . . . . . 7 |- ( ph -> ( 1st ` F ) ( ( C X.c D ) Func E ) ( 2nd ` F ) )
37	26, 27, 36	funcf1 16526	. . . . . 6 |- ( ph -> ( 1st ` F ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` E ) )
38		ffn 6045	. . . . . 6 |- ( ( 1st ` F ) : ( ( Base ` C ) X. ( Base ` D ) ) --> ( Base ` E ) -> ( 1st ` F ) Fn ( ( Base ` C ) X. ( Base ` D ) ) )
39	37, 38	syl 17	. . . . 5 |- ( ph -> ( 1st ` F ) Fn ( ( Base ` C ) X. ( Base ` D ) ) )
40		eqfnov2 6767	. . . . 5 |- ( ( ( 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 ) ) )
41	34, 39, 40	syl2anc 693	. . . 4 |- ( 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 ) ) )
42	24, 41	mpbird 247	. . 3 |- ( ph -> ( 1st ` ( <" C D E "> uncurryF G ) ) = ( 1st ` F ) )
43	2	ad3antrrr 766	. . . . . . . . . . 11 |- ( ( ( ( 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 )
44	7	ad3antrrr 766	. . . . . . . . . . 11 |- ( ( ( ( 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 )
45	12	ad3antrrr 766	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
46	16	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> x e. ( Base ` C ) )
47	46	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
48	17	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
49	48	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
50		eqid 2622	. . . . . . . . . . 11 |- ( Hom ` C ) = ( Hom ` C )
51		eqid 2622	. . . . . . . . . . 11 |- ( Hom ` D ) = ( Hom ` D )
52		simprl 794	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> z e. ( Base ` C ) )
53	52	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
54		simprr 796	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> w e. ( Base ` D ) )
55	54	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
56		simprl 794	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
57		simprr 796	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
58	1, 43, 44, 45, 14, 15, 47, 49, 50, 51, 53, 55, 56, 57	uncf2 16877	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
59	11	ad3antrrr 766	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
60	4	ad3antrrr 766	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 X.c D ) Func E ) )
61	9, 14, 59, 43, 60, 15, 47, 21, 49	curf11 16866	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
62		df-ov 6653	. . . . . . . . . . . . . . 15 |- ( x ( 1st ` F ) y ) = ( ( 1st ` F ) ` <. x , y >. )
63	61, 62	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 >. ) )
64	9, 14, 59, 43, 60, 15, 47, 21, 55	curf11 16866	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) )
65		df-ov 6653	. . . . . . . . . . . . . . 15 |- ( x ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. x , w >. )
66	64, 65	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 >. ) )
67	63, 66	opeq12d 4410	. . . . . . . . . . . . 13 |- ( ( ( ( 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 >. ) >. )
68		eqid 2622	. . . . . . . . . . . . . . 15 |- ( ( 1st ` G ) ` z ) = ( ( 1st ` G ) ` z )
69	9, 14, 59, 43, 60, 15, 53, 68, 55	curf11 16866	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
70		df-ov 6653	. . . . . . . . . . . . . 14 |- ( z ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. z , w >. )
71	69, 70	syl6eq 2672	. . . . . . . . . . . . 13 |- ( ( ( ( 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 >. ) )
72	67, 71	oveq12d 6668	. . . . . . . . . . . 12 |- ( ( ( ( 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 >. ) ) )
73		eqid 2622	. . . . . . . . . . . . . 14 |- ( Id ` D ) = ( Id ` D )
74		eqid 2622	. . . . . . . . . . . . . 14 |- ( ( x ( 2nd ` G ) z ) ` f ) = ( ( x ( 2nd ` G ) z ) ` f )
75	9, 14, 59, 43, 60, 15, 50, 73, 47, 53, 56, 74, 55	curf2val 16870	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
76		df-ov 6653	. . . . . . . . . . . . 13 |- ( f ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ( ( Id ` D ) ` w ) ) = ( ( <. x , w >. ( 2nd ` F ) <. z , w >. ) ` <. f , ( ( Id ` D ) ` w ) >. )
77	75, 76	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) >. ) )
78		eqid 2622	. . . . . . . . . . . . . 14 |- ( Id ` C ) = ( Id ` C )
79	9, 14, 59, 43, 60, 15, 47, 21, 49, 51, 78, 55, 57	curf12 16867	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
80		df-ov 6653	. . . . . . . . . . . . 13 |- ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` F ) <. x , w >. ) g ) = ( ( <. x , y >. ( 2nd ` F ) <. x , w >. ) ` <. ( ( Id ` C ) ` x ) , g >. )
81	79, 80	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ( ( 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 >. ) )
82	72, 77, 81	oveq123d 6671	. . . . . . . . . . 11 |- ( ( ( ( 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 >. ) ) )
83		eqid 2622	. . . . . . . . . . . 12 |- ( Hom ` ( C X.c D ) ) = ( Hom ` ( C X.c D ) )
84		eqid 2622	. . . . . . . . . . . 12 |- (comp ` ( C X.c D ) ) = (comp ` ( C X.c D ) )
85		eqid 2622	. . . . . . . . . . . 12 |- (comp ` E ) = (comp ` E )
86	36	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( 1st ` F ) ( ( C X.c D ) Func E ) ( 2nd ` F ) )
87	86	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( 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 X.c D ) Func E ) ( 2nd ` F ) )
88		opelxpi 5148	. . . . . . . . . . . . . 14 |- ( ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
89	88	ad2antlr 763	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
90	89	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
91		opelxpi 5148	. . . . . . . . . . . . 13 |- ( ( x e. ( Base ` C ) /\ w e. ( Base ` D ) ) -> <. x , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
92	47, 55, 91	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
93		opelxpi 5148	. . . . . . . . . . . . . 14 |- ( ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) -> <. z , w >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
94	93	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
95	94	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
96	14, 50, 78, 59, 47	catidcl 16343	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
97		opelxpi 5148	. . . . . . . . . . . . . 14 |- ( ( ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) /\ g e. ( y ( Hom ` D ) w ) ) -> <. ( ( Id ` C ) ` x ) , g >. e. ( ( x ( Hom ` C ) x ) X. ( y ( Hom ` D ) w ) ) )
98	96, 57, 97	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
99	25, 14, 15, 50, 51, 47, 49, 47, 55, 83	xpchom2 16826	. . . . . . . . . . . . 13 |- ( ( ( ( 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 X.c D ) ) <. x , w >. ) = ( ( x ( Hom ` C ) x ) X. ( y ( Hom ` D ) w ) ) )
100	98, 99	eleqtrrd 2704	. . . . . . . . . . . 12 |- ( ( ( ( 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 X.c D ) ) <. x , w >. ) )
101	15, 51, 73, 43, 55	catidcl 16343	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
102		opelxpi 5148	. . . . . . . . . . . . . 14 |- ( ( f e. ( x ( Hom ` C ) z ) /\ ( ( Id ` D ) ` w ) e. ( w ( Hom ` D ) w ) ) -> <. f , ( ( Id ` D ) ` w ) >. e. ( ( x ( Hom ` C ) z ) X. ( w ( Hom ` D ) w ) ) )
103	56, 101, 102	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) )
104	25, 14, 15, 50, 51, 47, 55, 53, 55, 83	xpchom2 16826	. . . . . . . . . . . . 13 |- ( ( ( ( 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 X.c D ) ) <. z , w >. ) = ( ( x ( Hom ` C ) z ) X. ( w ( Hom ` D ) w ) ) )
105	103, 104	eleqtrrd 2704	. . . . . . . . . . . 12 |- ( ( ( ( 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 X.c D ) ) <. z , w >. ) )
106	26, 83, 84, 85, 87, 90, 92, 95, 100, 105	funcco 16531	. . . . . . . . . . 11 |- ( ( ( ( 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 X.c 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 >. ) ) )
107		eqid 2622	. . . . . . . . . . . . . . 15 |- (comp ` C ) = (comp ` C )
108		eqid 2622	. . . . . . . . . . . . . . 15 |- (comp ` D ) = (comp ` D )
109	25, 14, 15, 50, 51, 47, 49, 47, 55, 107, 108, 84, 53, 55, 96, 57, 56, 101	xpcco2 16827	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 X.c 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 ) >. )
110	109	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ( ( ( 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 X.c 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 ) >. ) )
111		df-ov 6653	. . . . . . . . . . . . 13 |- ( ( 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 ) >. )
112	110, 111	syl6eqr 2674	. . . . . . . . . . . 12 |- ( ( ( ( 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 X.c 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 ) ) )
113	14, 50, 78, 59, 47, 107, 53, 56	catrid 16345	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
114	15, 51, 73, 43, 49, 108, 55, 57	catlid 16344	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
115	113, 114	oveq12d 6668	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
116	112, 115	eqtrd 2656	. . . . . . . . . . 11 |- ( ( ( ( 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 X.c D ) ) <. z , w >. ) <. ( ( Id ` C ) ` x ) , g >. ) ) = ( f ( <. x , y >. ( 2nd ` F ) <. z , w >. ) g ) )
117	82, 106, 116	3eqtr2d 2662	. . . . . . . . . 10 |- ( ( ( ( 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 ) )
118	58, 117	eqtrd 2656	. . . . . . . . 9 |- ( ( ( ( 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 ) )
119	118	ralrimivva 2971	. . . . . . . 8 |- ( ( ( 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 ) )
120		eqid 2622	. . . . . . . . . . . 12 |- ( Hom ` E ) = ( Hom ` E )
121	31	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( 1st ` ( <" C D E "> uncurryF G ) ) ( ( C X.c D ) Func E ) ( 2nd ` ( <" C D E "> uncurryF G ) ) )
122	26, 83, 120, 121, 89, 94	funcf2 16528	. . . . . . . . . . 11 |- ( ( ( 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 X.c D ) ) <. z , w >. ) --> ( ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` ( <" C D E "> uncurryF G ) ) ` <. z , w >. ) ) )
123	25, 14, 15, 50, 51, 46, 48, 52, 54, 83	xpchom2 16826	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` D ) ) ) -> ( <. x , y >. ( Hom ` ( C X.c D ) ) <. z , w >. ) = ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) )
124	123	feq2d 6031	. . . . . . . . . . 11 |- ( ( ( 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 X.c 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 >. ) ) ) )
125	122, 124	mpbid 222	. . . . . . . . . 10 |- ( ( ( 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 >. ) ) )
126		ffn 6045	. . . . . . . . . 10 |- ( ( <. 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 >. ) ) -> ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) Fn ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) )
127	125, 126	syl 17	. . . . . . . . 9 |- ( ( ( 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 ) ) )
128	26, 83, 120, 86, 89, 94	funcf2 16528	. . . . . . . . . . 11 |- ( ( ( 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 X.c D ) ) <. z , w >. ) --> ( ( ( 1st ` F ) ` <. x , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. z , w >. ) ) )
129	123	feq2d 6031	. . . . . . . . . . 11 |- ( ( ( 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 X.c 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 >. ) ) ) )
130	128, 129	mpbid 222	. . . . . . . . . 10 |- ( ( ( 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 >. ) ) )
131		ffn 6045	. . . . . . . . . 10 |- ( ( <. 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 >. ) ) -> ( <. x , y >. ( 2nd ` F ) <. z , w >. ) Fn ( ( x ( Hom ` C ) z ) X. ( y ( Hom ` D ) w ) ) )
132	130, 131	syl 17	. . . . . . . . 9 |- ( ( ( 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 ) ) )
133		eqfnov2 6767	. . . . . . . . 9 |- ( ( ( <. 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 ) ) )
134	127, 132, 133	syl2anc 693	. . . . . . . 8 |- ( ( ( 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 ) ) )
135	119, 134	mpbird 247	. . . . . . 7 |- ( ( ( 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 >. ) )
136	135	ralrimivva 2971	. . . . . 6 |- ( ( 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 >. ) )
137	136	ralrimivva 2971	. . . . 5 |- ( 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 >. ) )
138		oveq2 6658	. . . . . . . . 9 |- ( v = <. z , w >. -> ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) v ) = ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) )
139		oveq2 6658	. . . . . . . . 9 |- ( v = <. z , w >. -> ( u ( 2nd ` F ) v ) = ( u ( 2nd ` F ) <. z , w >. ) )
140	138, 139	eqeq12d 2637	. . . . . . . 8 |- ( 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 >. ) ) )
141	140	ralxp 5263	. . . . . . 7 |- ( 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 >. ) )
142		oveq1 6657	. . . . . . . . 9 |- ( u = <. x , y >. -> ( u ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) = ( <. x , y >. ( 2nd ` ( <" C D E "> uncurryF G ) ) <. z , w >. ) )
143		oveq1 6657	. . . . . . . . 9 |- ( u = <. x , y >. -> ( u ( 2nd ` F ) <. z , w >. ) = ( <. x , y >. ( 2nd ` F ) <. z , w >. ) )
144	142, 143	eqeq12d 2637	. . . . . . . 8 |- ( 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 >. ) ) )
145	144	2ralbidv 2989	. . . . . . 7 |- ( 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 >. ) ) )
146	141, 145	syl5bb 272	. . . . . 6 |- ( 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 >. ) ) )
147	146	ralxp 5263	. . . . 5 |- ( 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 >. ) )
148	137, 147	sylibr 224	. . . 4 |- ( 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 ) )
149	26, 31	funcfn2 16529	. . . . 5 |- ( ph -> ( 2nd ` ( <" C D E "> uncurryF G ) ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) )
150	26, 36	funcfn2 16529	. . . . 5 |- ( ph -> ( 2nd ` F ) Fn ( ( ( Base ` C ) X. ( Base ` D ) ) X. ( ( Base ` C ) X. ( Base ` D ) ) ) )
151		eqfnov2 6767	. . . . 5 |- ( ( ( 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 ) ) )
152	149, 150, 151	syl2anc 693	. . . 4 |- ( 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 ) ) )
153	148, 152	mpbird 247	. . 3 |- ( ph -> ( 2nd ` ( <" C D E "> uncurryF G ) ) = ( 2nd ` F ) )
154	42, 153	opeq12d 4410	. 2 |- ( ph -> <. ( 1st ` ( <" C D E "> uncurryF G ) ) , ( 2nd ` ( <" C D E "> uncurryF G ) ) >. = <. ( 1st ` F ) , ( 2nd ` F ) >. )
155		1st2nd 7214	. . 3 |- ( ( Rel ( ( C X.c D ) Func E ) /\ ( <" C D E "> uncurryF G ) e. ( ( C X.c D ) Func E ) ) -> ( <" C D E "> uncurryF G ) = <. ( 1st ` ( <" C D E "> uncurryF G ) ) , ( 2nd ` ( <" C D E "> uncurryF G ) ) >. )
156	28, 29, 155	sylancr 695	. 2 |- ( ph -> ( <" C D E "> uncurryF G ) = <. ( 1st ` ( <" C D E "> uncurryF G ) ) , ( 2nd ` ( <" C D E "> uncurryF G ) ) >. )
157		1st2nd 7214	. . 3 |- ( ( Rel ( ( C X.c D ) Func E ) /\ F e. ( ( C X.c D ) Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
158	28, 4, 157	sylancr 695	. 2 |- ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
159	154, 156, 158	3eqtr4d 2666	1 |- ( ph -> ( <" C D E "> uncurryF G ) = F )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   <.cop 4183   class class class wbr 4653   X. cxp 5112   Rel wrel 5119   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   <"cs3 13587   Basecbs 15857   Hom chom 15952  compcco 15953   Catccat 16325   Idccid 16326   Func cfunc 16514   FuncCat cfuc 16602   X._c cxpc 16808   curry_F ccurf 16850   uncurry_F cuncf 16851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-hom 15966  df-cco 15967  df-cat 16329  df-cid 16330  df-func 16518  df-cofu 16520  df-nat 16603  df-fuc 16604  df-xpc 16812  df-1stf 16813  df-2ndf 16814  df-prf 16815  df-evlf 16853  df-curf 16854  df-uncf 16855

This theorem is referenced by: (None)