Metamath Proof Explorer

Theorem idfucl

Description: The identity functor is a functor. Example 3.20(1) of Adamek p. 30. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis idfucl.i 
|- I = ( idFunc ` C )
Assertion idfucl 
|- ( C e. Cat -> I e. ( C Func C ) )

Proof

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