Metamath Proof Explorer

Theorem cofulid

Description: The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofulid.g 
|- ( ph -> F e. ( C Func D ) )
cofulid.1 
|- I = ( idFunc ` D )
Assertion cofulid 
|- ( ph -> ( I o.func F ) = F )

Proof

Step Hyp Ref Expression
1 cofulid.g 
 |-  ( ph -> F e. ( C Func D ) )
2 cofulid.1 
 |-  I = ( idFunc ` D )
3 eqid 
 |-  ( Base ` D ) = ( Base ` D )
4 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
5 1 4 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
6 5 simprd 
 |-  ( ph -> D e. Cat )
7 2 3 6 idfu1st 
 |-  ( ph -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
8 7 coeq1d 
 |-  ( ph -> ( ( 1st ` I ) o. ( 1st ` F ) ) = ( ( _I |` ( Base ` D ) ) o. ( 1st ` F ) ) )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 relfunc 
 |-  Rel ( C Func D )
11 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
12 10 1 11 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
13 9 3 12 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
14 fcoi2 
 |-  ( ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) o. ( 1st ` F ) ) = ( 1st ` F ) )
15 13 14 syl 
 |-  ( ph -> ( ( _I |` ( Base ` D ) ) o. ( 1st ` F ) ) = ( 1st ` F ) )
16 8 15 eqtrd 
 |-  ( ph -> ( ( 1st ` I ) o. ( 1st ` F ) ) = ( 1st ` F ) )
17 6 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> D e. Cat )
18 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
19 13 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
20 19 3adant3 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
21 13 ffvelrnda 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
22 21 3adant2 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
23 2 3 17 18 20 22 idfu2nd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) = ( _I |` ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) ) )
24 23 coeq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) = ( ( _I |` ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) ) o. ( x ( 2nd ` F ) y ) ) )
25 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
26 12 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
27 simp2 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> x e. ( Base ` C ) )
28 simp3 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
29 9 25 18 26 27 28 funcf2 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
30 fcoi2 
 |-  ( ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) -> ( ( _I |` ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) ) o. ( x ( 2nd ` F ) y ) ) = ( x ( 2nd ` F ) y ) )
31 29 30 syl 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( _I |` ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) ) o. ( x ( 2nd ` F ) y ) ) = ( x ( 2nd ` F ) y ) )
32 24 31 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) = ( x ( 2nd ` F ) y ) )
33 32 mpoeq3dva 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
34 9 12 funcfn2 
 |-  ( ph -> ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
35 fnov 
 |-  ( ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
36 34 35 sylib 
 |-  ( ph -> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
37 33 36 eqtr4d 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) = ( 2nd ` F ) )
38 16 37 opeq12d 
 |-  ( ph -> <. ( ( 1st ` I ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. = <. ( 1st ` F ) , ( 2nd ` F ) >. )
39 2 idfucl 
 |-  ( D e. Cat -> I e. ( D Func D ) )
40 6 39 syl 
 |-  ( ph -> I e. ( D Func D ) )
41 9 1 40 cofuval 
 |-  ( ph -> ( I o.func F ) = <. ( ( 1st ` I ) o. ( 1st ` F ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` I ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
42 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
43 10 1 42 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
44 38 41 43 3eqtr4d 
 |-  ( ph -> ( I o.func F ) = F )