Metamath Proof Explorer

Theorem cofurid

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

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

Proof

Step Hyp Ref Expression
1 cofulid.g 
 |-  ( ph -> F e. ( C Func D ) )
2 cofurid.1 
 |-  I = ( idFunc ` C )
3 eqid 
 |-  ( Base ` C ) = ( Base ` C )
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 simpld 
 |-  ( ph -> C e. Cat )
7 2 3 6 idfu1st 
 |-  ( ph -> ( 1st ` I ) = ( _I |` ( Base ` C ) ) )
8 7 coeq2d 
 |-  ( ph -> ( ( 1st ` F ) o. ( 1st ` I ) ) = ( ( 1st ` F ) o. ( _I |` ( Base ` C ) ) ) )
9 eqid 
 |-  ( Base ` D ) = ( Base ` D )
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 3 9 12 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
14 fcoi1 
 |-  ( ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) -> ( ( 1st ` F ) o. ( _I |` ( Base ` C ) ) ) = ( 1st ` F ) )
15 13 14 syl 
 |-  ( ph -> ( ( 1st ` F ) o. ( _I |` ( Base ` C ) ) ) = ( 1st ` F ) )
16 8 15 eqtrd 
 |-  ( ph -> ( ( 1st ` F ) o. ( 1st ` I ) ) = ( 1st ` F ) )
17 7 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` I ) = ( _I |` ( Base ` C ) ) )
18 17 fveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` I ) ` x ) = ( ( _I |` ( Base ` C ) ) ` x ) )
19 fvresi 
 |-  ( x e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` x ) = x )
20 19 3ad2ant2 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( _I |` ( Base ` C ) ) ` x ) = x )
21 18 20 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` I ) ` x ) = x )
22 17 fveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` I ) ` y ) = ( ( _I |` ( Base ` C ) ) ` y ) )
23 fvresi 
 |-  ( y e. ( Base ` C ) -> ( ( _I |` ( Base ` C ) ) ` y ) = y )
24 23 3ad2ant3 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( _I |` ( Base ` C ) ) ` y ) = y )
25 22 24 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` I ) ` y ) = y )
26 21 25 oveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) = ( x ( 2nd ` F ) y ) )
27 6 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> C e. Cat )
28 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
29 simp2 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> x e. ( Base ` C ) )
30 simp3 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
31 2 3 27 28 29 30 idfu2nd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( 2nd ` I ) y ) = ( _I |` ( x ( Hom ` C ) y ) ) )
32 26 31 coeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) o. ( x ( 2nd ` I ) y ) ) = ( ( x ( 2nd ` F ) y ) o. ( _I |` ( x ( Hom ` C ) y ) ) ) )
33 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
34 12 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
35 3 28 33 34 29 30 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 ) ) )
36 fcoi1 
 |-  ( ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) -> ( ( x ( 2nd ` F ) y ) o. ( _I |` ( x ( Hom ` C ) y ) ) ) = ( x ( 2nd ` F ) y ) )
37 35 36 syl 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( x ( 2nd ` F ) y ) o. ( _I |` ( x ( Hom ` C ) y ) ) ) = ( x ( 2nd ` F ) y ) )
38 32 37 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) o. ( x ( 2nd ` I ) y ) ) = ( x ( 2nd ` F ) y ) )
39 38 mpoeq3dva 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) o. ( x ( 2nd ` I ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
40 3 12 funcfn2 
 |-  ( ph -> ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
41 fnov 
 |-  ( ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
42 40 41 sylib 
 |-  ( ph -> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
43 39 42 eqtr4d 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) o. ( x ( 2nd ` I ) y ) ) ) = ( 2nd ` F ) )
44 16 43 opeq12d 
 |-  ( ph -> <. ( ( 1st ` F ) o. ( 1st ` I ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) o. ( x ( 2nd ` I ) y ) ) ) >. = <. ( 1st ` F ) , ( 2nd ` F ) >. )
45 2 idfucl 
 |-  ( C e. Cat -> I e. ( C Func C ) )
46 6 45 syl 
 |-  ( ph -> I e. ( C Func C ) )
47 3 46 1 cofuval 
 |-  ( ph -> ( F o.func I ) = <. ( ( 1st ` F ) o. ( 1st ` I ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` I ) ` x ) ( 2nd ` F ) ( ( 1st ` I ) ` y ) ) o. ( x ( 2nd ` I ) y ) ) ) >. )
48 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
49 10 1 48 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
50 44 47 49 3eqtr4d 
 |-  ( ph -> ( F o.func I ) = F )