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
|
ad5ant12 |
|- ( ( ( ( ( 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 ) ) ) |