Step |
Hyp |
Ref |
Expression |
1 |
|
idfucl.i |
|- I = ( idFunc ` C ) |
2 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
3 |
|
id |
|- ( C e. Cat -> C e. Cat ) |
4 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
5 |
1 2 3 4
|
idfuval |
|- ( C e. Cat -> I = <. ( _I |` ( Base ` C ) ) , ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. ) |
6 |
5
|
fveq2d |
|- ( C e. Cat -> ( 2nd ` I ) = ( 2nd ` <. ( _I |` ( Base ` C ) ) , ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. ) ) |
7 |
|
fvex |
|- ( Base ` C ) e. _V |
8 |
|
resiexg |
|- ( ( Base ` C ) e. _V -> ( _I |` ( Base ` C ) ) e. _V ) |
9 |
7 8
|
ax-mp |
|- ( _I |` ( Base ` C ) ) e. _V |
10 |
7 7
|
xpex |
|- ( ( Base ` C ) X. ( Base ` C ) ) e. _V |
11 |
10
|
mptex |
|- ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) e. _V |
12 |
9 11
|
op2nd |
|- ( 2nd ` <. ( _I |` ( Base ` C ) ) , ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. ) = ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) |
13 |
6 12
|
eqtrdi |
|- ( C e. Cat -> ( 2nd ` I ) = ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) ) |
14 |
13
|
opeq2d |
|- ( C e. Cat -> <. ( _I |` ( Base ` C ) ) , ( 2nd ` I ) >. = <. ( _I |` ( Base ` C ) ) , ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. ) |
15 |
5 14
|
eqtr4d |
|- ( C e. Cat -> I = <. ( _I |` ( Base ` C ) ) , ( 2nd ` I ) >. ) |
16 |
|
f1oi |
|- ( _I |` ( Base ` C ) ) : ( Base ` C ) -1-1-onto-> ( Base ` C ) |
17 |
|
f1of |
|- ( ( _I |` ( Base ` C ) ) : ( Base ` C ) -1-1-onto-> ( Base ` C ) -> ( _I |` ( Base ` C ) ) : ( Base ` C ) --> ( Base ` C ) ) |
18 |
16 17
|
mp1i |
|- ( C e. Cat -> ( _I |` ( Base ` C ) ) : ( Base ` C ) --> ( Base ` C ) ) |
19 |
|
f1oi |
|- ( _I |` ( ( Hom ` C ) ` z ) ) : ( ( Hom ` C ) ` z ) -1-1-onto-> ( ( Hom ` C ) ` z ) |
20 |
|
f1of |
|- ( ( _I |` ( ( Hom ` C ) ` z ) ) : ( ( Hom ` C ) ` z ) -1-1-onto-> ( ( Hom ` C ) ` z ) -> ( _I |` ( ( Hom ` C ) ` z ) ) : ( ( Hom ` C ) ` z ) --> ( ( Hom ` C ) ` z ) ) |
21 |
19 20
|
ax-mp |
|- ( _I |` ( ( Hom ` C ) ` z ) ) : ( ( Hom ` C ) ` z ) --> ( ( Hom ` C ) ` z ) |
22 |
|
fvex |
|- ( ( Hom ` C ) ` z ) e. _V |
23 |
22 22
|
elmap |
|- ( ( _I |` ( ( Hom ` C ) ` z ) ) e. ( ( ( Hom ` C ) ` z ) ^m ( ( Hom ` C ) ` z ) ) <-> ( _I |` ( ( Hom ` C ) ` z ) ) : ( ( Hom ` C ) ` z ) --> ( ( Hom ` C ) ` z ) ) |
24 |
21 23
|
mpbir |
|- ( _I |` ( ( Hom ` C ) ` z ) ) e. ( ( ( Hom ` C ) ` z ) ^m ( ( Hom ` C ) ` z ) ) |
25 |
|
xp1st |
|- ( z e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 1st ` z ) e. ( Base ` C ) ) |
26 |
25
|
adantl |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( 1st ` z ) e. ( Base ` C ) ) |
27 |
|
fvresi |
|- ( ( 1st ` z ) e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) = ( 1st ` z ) ) |
28 |
26 27
|
syl |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) = ( 1st ` z ) ) |
29 |
|
xp2nd |
|- ( z e. ( ( Base ` C ) X. ( Base ` C ) ) -> ( 2nd ` z ) e. ( Base ` C ) ) |
30 |
29
|
adantl |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( 2nd ` z ) e. ( Base ` C ) ) |
31 |
|
fvresi |
|- ( ( 2nd ` z ) e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) = ( 2nd ` z ) ) |
32 |
30 31
|
syl |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) = ( 2nd ` z ) ) |
33 |
28 32
|
oveq12d |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) = ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) ) |
34 |
|
df-ov |
|- ( ( 1st ` z ) ( Hom ` C ) ( 2nd ` z ) ) = ( ( Hom ` C ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
35 |
33 34
|
eqtrdi |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) = ( ( Hom ` C ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) |
36 |
|
1st2nd2 |
|- ( z e. ( ( Base ` C ) X. ( Base ` C ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
37 |
36
|
adantl |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
38 |
37
|
fveq2d |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( Hom ` C ) ` z ) = ( ( Hom ` C ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) |
39 |
35 38
|
eqtr4d |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) = ( ( Hom ` C ) ` z ) ) |
40 |
39
|
oveq1d |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) = ( ( ( Hom ` C ) ` z ) ^m ( ( Hom ` C ) ` z ) ) ) |
41 |
24 40
|
eleqtrrid |
|- ( ( C e. Cat /\ z e. ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( _I |` ( ( Hom ` C ) ` z ) ) e. ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) |
42 |
41
|
ralrimiva |
|- ( C e. Cat -> A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( _I |` ( ( Hom ` C ) ` z ) ) e. ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) |
43 |
|
mptelixpg |
|- ( ( ( Base ` C ) X. ( Base ` C ) ) e. _V -> ( ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( _I |` ( ( Hom ` C ) ` z ) ) e. ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) ) |
44 |
10 43
|
ax-mp |
|- ( ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) <-> A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( _I |` ( ( Hom ` C ) ` z ) ) e. ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) |
45 |
42 44
|
sylibr |
|- ( C e. Cat -> ( z e. ( ( Base ` C ) X. ( Base ` C ) ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) |
46 |
13 45
|
eqeltrd |
|- ( C e. Cat -> ( 2nd ` I ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) ) |
47 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
48 |
|
simpl |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> C e. Cat ) |
49 |
|
simpr |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) ) |
50 |
2 4 47 48 49
|
catidcl |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) ) |
51 |
|
fvresi |
|- ( ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) -> ( ( _I |` ( x ( Hom ` C ) x ) ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` x ) ) |
52 |
50 51
|
syl |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( _I |` ( x ( Hom ` C ) x ) ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` x ) ) |
53 |
1 2 48 4 49 49
|
idfu2nd |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( x ( 2nd ` I ) x ) = ( _I |` ( x ( Hom ` C ) x ) ) ) |
54 |
53
|
fveq1d |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` I ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( _I |` ( x ( Hom ` C ) x ) ) ` ( ( Id ` C ) ` x ) ) ) |
55 |
|
fvresi |
|- ( x e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` x ) = x ) |
56 |
55
|
adantl |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( _I |` ( Base ` C ) ) ` x ) = x ) |
57 |
56
|
fveq2d |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( Id ` C ) ` ( ( _I |` ( Base ` C ) ) ` x ) ) = ( ( Id ` C ) ` x ) ) |
58 |
52 54 57
|
3eqtr4d |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( x ( 2nd ` I ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` ( ( _I |` ( Base ` C ) ) ` x ) ) ) |
59 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
60 |
48
|
ad2antrr |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> C e. Cat ) |
61 |
49
|
ad2antrr |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> x e. ( Base ` C ) ) |
62 |
|
simplrl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> y e. ( Base ` C ) ) |
63 |
|
simplrr |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> z e. ( Base ` C ) ) |
64 |
|
simprl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> f e. ( x ( Hom ` C ) y ) ) |
65 |
|
simprr |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> g e. ( y ( Hom ` C ) z ) ) |
66 |
2 4 59 60 61 62 63 64 65
|
catcocl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) ) |
67 |
|
fvresi |
|- ( ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) -> ( ( _I |` ( x ( Hom ` C ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) ) |
68 |
66 67
|
syl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( _I |` ( x ( Hom ` C ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) ) |
69 |
1 2 60 4 61 63
|
idfu2nd |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( 2nd ` I ) z ) = ( _I |` ( x ( Hom ` C ) z ) ) ) |
70 |
69
|
fveq1d |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( _I |` ( x ( Hom ` C ) z ) ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) ) |
71 |
61 55
|
syl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( _I |` ( Base ` C ) ) ` x ) = x ) |
72 |
|
fvresi |
|- ( y e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` y ) = y ) |
73 |
62 72
|
syl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( _I |` ( Base ` C ) ) ` y ) = y ) |
74 |
71 73
|
opeq12d |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. = <. x , y >. ) |
75 |
|
fvresi |
|- ( z e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` z ) = z ) |
76 |
63 75
|
syl |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( _I |` ( Base ` C ) ) ` z ) = z ) |
77 |
74 76
|
oveq12d |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) = ( <. x , y >. ( comp ` C ) z ) ) |
78 |
1 2 60 4 62 63 65
|
idfu2 |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( y ( 2nd ` I ) z ) ` g ) = g ) |
79 |
1 2 60 4 61 62 64
|
idfu2 |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` I ) y ) ` f ) = f ) |
80 |
77 78 79
|
oveq123d |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) ) |
81 |
68 70 80
|
3eqtr4d |
|- ( ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) ) |
82 |
81
|
ralrimivva |
|- ( ( ( C e. Cat /\ x e. ( Base ` C ) ) /\ ( y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) ) |
83 |
82
|
ralrimivva |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) ) |
84 |
58 83
|
jca |
|- ( ( C e. Cat /\ x e. ( Base ` C ) ) -> ( ( ( x ( 2nd ` I ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` ( ( _I |` ( Base ` C ) ) ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) ) ) |
85 |
84
|
ralrimiva |
|- ( C e. Cat -> A. x e. ( Base ` C ) ( ( ( x ( 2nd ` I ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` ( ( _I |` ( Base ` C ) ) ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) ) ) |
86 |
2 2 4 4 47 47 59 59 3 3
|
isfunc |
|- ( C e. Cat -> ( ( _I |` ( Base ` C ) ) ( C Func C ) ( 2nd ` I ) <-> ( ( _I |` ( Base ` C ) ) : ( Base ` C ) --> ( Base ` C ) /\ ( 2nd ` I ) e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( ( _I |` ( Base ` C ) ) ` ( 1st ` z ) ) ( Hom ` C ) ( ( _I |` ( Base ` C ) ) ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) /\ A. x e. ( Base ` C ) ( ( ( x ( 2nd ` I ) x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` ( ( _I |` ( Base ` C ) ) ` x ) ) /\ A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( ( x ( 2nd ` I ) z ) ` ( g ( <. x , y >. ( comp ` C ) z ) f ) ) = ( ( ( y ( 2nd ` I ) z ) ` g ) ( <. ( ( _I |` ( Base ` C ) ) ` x ) , ( ( _I |` ( Base ` C ) ) ` y ) >. ( comp ` C ) ( ( _I |` ( Base ` C ) ) ` z ) ) ( ( x ( 2nd ` I ) y ) ` f ) ) ) ) ) ) |
87 |
18 46 85 86
|
mpbir3and |
|- ( C e. Cat -> ( _I |` ( Base ` C ) ) ( C Func C ) ( 2nd ` I ) ) |
88 |
|
df-br |
|- ( ( _I |` ( Base ` C ) ) ( C Func C ) ( 2nd ` I ) <-> <. ( _I |` ( Base ` C ) ) , ( 2nd ` I ) >. e. ( C Func C ) ) |
89 |
87 88
|
sylib |
|- ( C e. Cat -> <. ( _I |` ( Base ` C ) ) , ( 2nd ` I ) >. e. ( C Func C ) ) |
90 |
15 89
|
eqeltrd |
|- ( C e. Cat -> I e. ( C Func C ) ) |