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

Metamath Proof Explorer

Theorem curf2ndf

Description: As shown in diagval , the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is x e. C |-> ( y e. D |-> y ) , which is a constant functor of the identity functor at D . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses curf2ndf.q 
|- Q = ( D FuncCat D )
curf2ndf.c 
|- ( ph -> C e. Cat )
curf2ndf.d 
|- ( ph -> D e. Cat )
Assertion curf2ndf 
|- ( ph -> ( <. C , D >. curryF ( C 2ndF D ) ) = ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) )

Proof

Step Hyp Ref Expression
1 curf2ndf.q 
 |-  Q = ( D FuncCat D )
2 curf2ndf.c 
 |-  ( ph -> C e. Cat )
3 curf2ndf.d 
 |-  ( ph -> D e. Cat )
4 df-ov 
 |-  ( x ( 1st ` ( C 2ndF D ) ) y ) = ( ( 1st ` ( C 2ndF D ) ) ` <. x , y >. )
5 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 5 6 7 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` ( C Xc. D ) )
9 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
10 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> C e. Cat )
11 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> D e. Cat )
12 eqid 
 |-  ( C 2ndF D ) = ( C 2ndF D )
13 opelxpi 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` D ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
14 13 adantll 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
15 5 8 9 10 11 12 14 2ndf1 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( 1st ` ( C 2ndF D ) ) ` <. x , y >. ) = ( 2nd ` <. x , y >. ) )
16 vex 
 |-  x e. _V
17 vex 
 |-  y e. _V
18 16 17 op2nd 
 |-  ( 2nd ` <. x , y >. ) = y
19 15 18 eqtrdi 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( ( 1st ` ( C 2ndF D ) ) ` <. x , y >. ) = y )
20 4 19 eqtrid 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) -> ( x ( 1st ` ( C 2ndF D ) ) y ) = y )
21 20 mpteq2dva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) |-> ( x ( 1st ` ( C 2ndF D ) ) y ) ) = ( y e. ( Base ` D ) |-> y ) )
22 mptresid 
 |-  ( _I |` ( Base ` D ) ) = ( y e. ( Base ` D ) |-> y )
23 21 22 eqtr4di 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) |-> ( x ( 1st ` ( C 2ndF D ) ) y ) ) = ( _I |` ( Base ` D ) ) )
24 df-ov 
 |-  ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) = ( ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) ` <. ( ( Id ` C ) ` x ) , f >. )
25 10 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> C e. Cat )
26 11 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> D e. Cat )
27 14 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> <. x , y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
28 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> x e. ( Base ` C ) )
29 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> z e. ( Base ` D ) )
30 28 29 opelxpd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> <. x , z >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
31 5 8 9 25 26 12 27 30 2ndf2 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) = ( 2nd |` ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) ) )
32 31 fveq1d 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) ` <. ( ( Id ` C ) ` x ) , f >. ) = ( ( 2nd |` ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) ) ` <. ( ( Id ` C ) ` x ) , f >. ) )
33 24 32 eqtrid 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) = ( ( 2nd |` ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) ) ` <. ( ( Id ` C ) ` x ) , f >. ) )
34 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
35 eqid 
 |-  ( Id ` C ) = ( Id ` C )
36 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
37 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
38 6 34 35 36 37 catidcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
39 38 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
40 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> f e. ( y ( Hom ` D ) z ) )
41 39 40 opelxpd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> <. ( ( Id ` C ) ` x ) , f >. e. ( ( x ( Hom ` C ) x ) X. ( y ( Hom ` D ) z ) ) )
42 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
43 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> y e. ( Base ` D ) )
44 5 6 7 34 42 28 43 28 29 9 xpchom2 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) = ( ( x ( Hom ` C ) x ) X. ( y ( Hom ` D ) z ) ) )
45 41 44 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> <. ( ( Id ` C ) ` x ) , f >. e. ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) )
46 45 fvresd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( ( 2nd |` ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) ) ` <. ( ( Id ` C ) ` x ) , f >. ) = ( 2nd ` <. ( ( Id ` C ) ` x ) , f >. ) )
47 fvex 
 |-  ( ( Id ` C ) ` x ) e. _V
48 vex 
 |-  f e. _V
49 47 48 op2nd 
 |-  ( 2nd ` <. ( ( Id ` C ) ` x ) , f >. ) = f
50 46 49 eqtrdi 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( ( 2nd |` ( <. x , y >. ( Hom ` ( C Xc. D ) ) <. x , z >. ) ) ` <. ( ( Id ` C ) ` x ) , f >. ) = f )
51 33 50 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) /\ f e. ( y ( Hom ` D ) z ) ) -> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) = f )
52 51 mpteq2dva 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) -> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) = ( f e. ( y ( Hom ` D ) z ) |-> f ) )
53 mptresid 
 |-  ( _I |` ( y ( Hom ` D ) z ) ) = ( f e. ( y ( Hom ` D ) z ) |-> f )
54 52 53 eqtr4di 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) ) /\ z e. ( Base ` D ) ) -> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) = ( _I |` ( y ( Hom ` D ) z ) ) )
55 54 3impa 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` D ) /\ z e. ( Base ` D ) ) -> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) = ( _I |` ( y ( Hom ` D ) z ) ) )
56 55 mpoeq3dva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) ) = ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( _I |` ( y ( Hom ` D ) z ) ) ) )
57 fveq2 
 |-  ( u = <. y , z >. -> ( ( Hom ` D ) ` u ) = ( ( Hom ` D ) ` <. y , z >. ) )
58 df-ov 
 |-  ( y ( Hom ` D ) z ) = ( ( Hom ` D ) ` <. y , z >. )
59 57 58 eqtr4di 
 |-  ( u = <. y , z >. -> ( ( Hom ` D ) ` u ) = ( y ( Hom ` D ) z ) )
60 59 reseq2d 
 |-  ( u = <. y , z >. -> ( _I |` ( ( Hom ` D ) ` u ) ) = ( _I |` ( y ( Hom ` D ) z ) ) )
61 60 mpompt 
 |-  ( u e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( _I |` ( ( Hom ` D ) ` u ) ) ) = ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( _I |` ( y ( Hom ` D ) z ) ) )
62 56 61 eqtr4di 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) ) = ( u e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( _I |` ( ( Hom ` D ) ` u ) ) ) )
63 23 62 opeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( y e. ( Base ` D ) |-> ( x ( 1st ` ( C 2ndF D ) ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) ) >. = <. ( _I |` ( Base ` D ) ) , ( u e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( _I |` ( ( Hom ` D ) ` u ) ) ) >. )
64 eqid 
 |-  ( <. C , D >. curryF ( C 2ndF D ) ) = ( <. C , D >. curryF ( C 2ndF D ) )
65 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
66 5 2 3 12 2ndfcl 
 |-  ( ph -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) )
67 66 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) )
68 eqid 
 |-  ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) = ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x )
69 64 6 36 65 67 7 37 68 42 35 curf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) = <. ( y e. ( Base ` D ) |-> ( x ( 1st ` ( C 2ndF D ) ) y ) ) , ( y e. ( Base ` D ) , z e. ( Base ` D ) |-> ( f e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` x ) ( <. x , y >. ( 2nd ` ( C 2ndF D ) ) <. x , z >. ) f ) ) ) >. )
70 eqid 
 |-  ( idFunc ` D ) = ( idFunc ` D )
71 70 7 65 42 idfuval 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( idFunc ` D ) = <. ( _I |` ( Base ` D ) ) , ( u e. ( ( Base ` D ) X. ( Base ` D ) ) |-> ( _I |` ( ( Hom ` D ) ` u ) ) ) >. )
72 63 69 71 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) = ( idFunc ` D ) )
73 eqid 
 |-  ( Q DiagFunc C ) = ( Q DiagFunc C )
74 1 3 3 fuccat 
 |-  ( ph -> Q e. Cat )
75 74 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> Q e. Cat )
76 1 fucbas 
 |-  ( D Func D ) = ( Base ` Q )
77 70 idfucl 
 |-  ( D e. Cat -> ( idFunc ` D ) e. ( D Func D ) )
78 3 77 syl 
 |-  ( ph -> ( idFunc ` D ) e. ( D Func D ) )
79 78 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( idFunc ` D ) e. ( D Func D ) )
80 eqid 
 |-  ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) = ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) )
81 73 75 36 76 79 80 6 37 diag11 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ` x ) = ( idFunc ` D ) )
82 72 81 eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) = ( ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ` x ) )
83 82 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) ) = ( x e. ( Base ` C ) |-> ( ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ` x ) ) )
84 relfunc 
 |-  Rel ( C Func Q )
85 64 1 2 3 66 curfcl 
 |-  ( ph -> ( <. C , D >. curryF ( C 2ndF D ) ) e. ( C Func Q ) )
86 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ ( <. C , D >. curryF ( C 2ndF D ) ) e. ( C Func Q ) ) -> ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ( C Func Q ) ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) )
87 84 85 86 sylancr 
 |-  ( ph -> ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ( C Func Q ) ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) )
88 6 76 87 funcf1 
 |-  ( ph -> ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) : ( Base ` C ) --> ( D Func D ) )
89 88 feqmptd 
 |-  ( ph -> ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) = ( x e. ( Base ` C ) |-> ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) ) )
90 73 74 2 76 78 80 diag1cl 
 |-  ( ph -> ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) e. ( C Func Q ) )
91 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) e. ( C Func Q ) ) -> ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ( C Func Q ) ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) )
92 84 90 91 sylancr 
 |-  ( ph -> ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ( C Func Q ) ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) )
93 6 76 92 funcf1 
 |-  ( ph -> ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) : ( Base ` C ) --> ( D Func D ) )
94 93 feqmptd 
 |-  ( ph -> ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) = ( x e. ( Base ` C ) |-> ( ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ` x ) ) )
95 83 89 94 3eqtr4d 
 |-  ( ph -> ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) = ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) )
96 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> D e. Cat )
97 70 7 96 idfu1st 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( idFunc ` D ) ) = ( _I |` ( Base ` D ) ) )
98 97 coeq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( Id ` D ) o. ( 1st ` ( idFunc ` D ) ) ) = ( ( Id ` D ) o. ( _I |` ( Base ` D ) ) ) )
99 eqid 
 |-  ( Id ` Q ) = ( Id ` Q )
100 eqid 
 |-  ( Id ` D ) = ( Id ` D )
101 78 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( idFunc ` D ) e. ( D Func D ) )
102 1 99 100 101 fucid 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( Id ` Q ) ` ( idFunc ` D ) ) = ( ( Id ` D ) o. ( 1st ` ( idFunc ` D ) ) ) )
103 7 100 cidfn 
 |-  ( D e. Cat -> ( Id ` D ) Fn ( Base ` D ) )
104 96 103 syl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( Id ` D ) Fn ( Base ` D ) )
105 dffn2 
 |-  ( ( Id ` D ) Fn ( Base ` D ) <-> ( Id ` D ) : ( Base ` D ) --> _V )
106 104 105 sylib 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( Id ` D ) : ( Base ` D ) --> _V )
107 106 feqmptd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( Id ` D ) = ( z e. ( Base ` D ) |-> ( ( Id ` D ) ` z ) ) )
108 fcoi1 
 |-  ( ( Id ` D ) : ( Base ` D ) --> _V -> ( ( Id ` D ) o. ( _I |` ( Base ` D ) ) ) = ( Id ` D ) )
109 106 108 syl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( Id ` D ) o. ( _I |` ( Base ` D ) ) ) = ( Id ` D ) )
110 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> C e. Cat )
111 110 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> C e. Cat )
112 96 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> D e. Cat )
113 simplrl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
114 opelxpi 
 |-  ( ( x e. ( Base ` C ) /\ z e. ( Base ` D ) ) -> <. x , z >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
115 113 114 sylan 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> <. x , z >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
116 simplrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
117 opelxpi 
 |-  ( ( y e. ( Base ` C ) /\ z e. ( Base ` D ) ) -> <. y , z >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
118 116 117 sylan 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> <. y , z >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
119 5 8 9 111 112 12 115 118 2ndf2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) = ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) )
120 119 oveqd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( f ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) ( ( Id ` D ) ` z ) ) = ( f ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) ( ( Id ` D ) ` z ) ) )
121 df-ov 
 |-  ( f ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) ( ( Id ` D ) ` z ) ) = ( ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) ` <. f , ( ( Id ` D ) ` z ) >. )
122 simplr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> f e. ( x ( Hom ` C ) y ) )
123 simpr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> z e. ( Base ` D ) )
124 7 42 100 112 123 catidcl 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( Id ` D ) ` z ) e. ( z ( Hom ` D ) z ) )
125 122 124 opelxpd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> <. f , ( ( Id ` D ) ` z ) >. e. ( ( x ( Hom ` C ) y ) X. ( z ( Hom ` D ) z ) ) )
126 113 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> x e. ( Base ` C ) )
127 116 adantr 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> y e. ( Base ` C ) )
128 5 6 7 34 42 126 123 127 123 9 xpchom2 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) = ( ( x ( Hom ` C ) y ) X. ( z ( Hom ` D ) z ) ) )
129 125 128 eleqtrrd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> <. f , ( ( Id ` D ) ` z ) >. e. ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) )
130 129 fvresd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) ` <. f , ( ( Id ` D ) ` z ) >. ) = ( 2nd ` <. f , ( ( Id ` D ) ` z ) >. ) )
131 121 130 eqtrid 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( f ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) ( ( Id ` D ) ` z ) ) = ( 2nd ` <. f , ( ( Id ` D ) ` z ) >. ) )
132 fvex 
 |-  ( ( Id ` D ) ` z ) e. _V
133 48 132 op2nd 
 |-  ( 2nd ` <. f , ( ( Id ` D ) ` z ) >. ) = ( ( Id ` D ) ` z )
134 131 133 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( f ( 2nd |` ( <. x , z >. ( Hom ` ( C Xc. D ) ) <. y , z >. ) ) ( ( Id ` D ) ` z ) ) = ( ( Id ` D ) ` z ) )
135 120 134 eqtrd 
 |-  ( ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) /\ z e. ( Base ` D ) ) -> ( f ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) ( ( Id ` D ) ` z ) ) = ( ( Id ` D ) ` z ) )
136 135 mpteq2dva 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( z e. ( Base ` D ) |-> ( f ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) = ( z e. ( Base ` D ) |-> ( ( Id ` D ) ` z ) ) )
137 107 109 136 3eqtr4rd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( z e. ( Base ` D ) |-> ( f ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) = ( ( Id ` D ) o. ( _I |` ( Base ` D ) ) ) )
138 98 102 137 3eqtr4rd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( z e. ( Base ` D ) |-> ( f ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) = ( ( Id ` Q ) ` ( idFunc ` D ) ) )
139 66 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( C 2ndF D ) e. ( ( C Xc. D ) Func D ) )
140 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> f e. ( x ( Hom ` C ) y ) )
141 eqid 
 |-  ( ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ` f )
142 64 6 110 96 139 7 34 100 113 116 140 141 curf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ` f ) = ( z e. ( Base ` D ) |-> ( f ( <. x , z >. ( 2nd ` ( C 2ndF D ) ) <. y , z >. ) ( ( Id ` D ) ` z ) ) ) )
143 74 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> Q e. Cat )
144 73 143 110 76 101 80 6 113 34 99 116 140 diag12 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ` f ) = ( ( Id ` Q ) ` ( idFunc ` D ) ) )
145 138 142 144 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ` f ) )
146 145 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ` f ) ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ` f ) ) )
147 eqid 
 |-  ( D Nat D ) = ( D Nat D )
148 1 147 fuchom 
 |-  ( D Nat D ) = ( Hom ` Q )
149 87 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ( C Func Q ) ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) )
150 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
151 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
152 6 34 148 149 150 151 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` x ) ( D Nat D ) ( ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) ` y ) ) )
153 152 feqmptd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ` f ) ) )
154 92 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ( C Func Q ) ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) )
155 6 34 148 154 150 151 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ` x ) ( D Nat D ) ( ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) ` y ) ) )
156 155 feqmptd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ` f ) ) )
157 146 153 156 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) = ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) )
158 157 3impb 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) = ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) )
159 158 mpoeq3dva 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ) )
160 6 87 funcfn2 
 |-  ( ph -> ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
161 fnov 
 |-  ( ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ) )
162 160 161 sylib 
 |-  ( ph -> ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) y ) ) )
163 6 92 funcfn2 
 |-  ( ph -> ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
164 fnov 
 |-  ( ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ) )
165 163 164 sylib 
 |-  ( ph -> ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) y ) ) )
166 159 162 165 3eqtr4d 
 |-  ( ph -> ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) = ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) )
167 95 166 opeq12d 
 |-  ( ph -> <. ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) , ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) >. = <. ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) , ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) >. )
168 1st2nd 
 |-  ( ( Rel ( C Func Q ) /\ ( <. C , D >. curryF ( C 2ndF D ) ) e. ( C Func Q ) ) -> ( <. C , D >. curryF ( C 2ndF D ) ) = <. ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) , ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) >. )
169 84 85 168 sylancr 
 |-  ( ph -> ( <. C , D >. curryF ( C 2ndF D ) ) = <. ( 1st ` ( <. C , D >. curryF ( C 2ndF D ) ) ) , ( 2nd ` ( <. C , D >. curryF ( C 2ndF D ) ) ) >. )
170 1st2nd 
 |-  ( ( Rel ( C Func Q ) /\ ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) e. ( C Func Q ) ) -> ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) = <. ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) , ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) >. )
171 84 90 170 sylancr 
 |-  ( ph -> ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) = <. ( 1st ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) , ( 2nd ` ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) ) >. )
172 167 169 171 3eqtr4d 
 |-  ( ph -> ( <. C , D >. curryF ( C 2ndF D ) ) = ( ( 1st ` ( Q DiagFunc C ) ) ` ( idFunc ` D ) ) )