MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cofurid Structured version   Unicode version

Theorem cofurid 14788
Description: The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017.)
Hypotheses
Ref Expression
cofulid.g  |-  ( ph  ->  F  e.  ( C 
Func  D ) )
cofurid.1  |-  I  =  (idfunc `  C )
Assertion
Ref Expression
cofurid  |-  ( ph  ->  ( F  o.func  I )  =  F )

Proof of Theorem cofurid
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cofurid.1 . . . . . 6  |-  I  =  (idfunc `  C )
2 eqid 2437 . . . . . 6  |-  ( Base `  C )  =  (
Base `  C )
3 cofulid.g . . . . . . . 8  |-  ( ph  ->  F  e.  ( C 
Func  D ) )
4 funcrcl 14760 . . . . . . . 8  |-  ( F  e.  ( C  Func  D )  ->  ( C  e.  Cat  /\  D  e. 
Cat ) )
53, 4syl 16 . . . . . . 7  |-  ( ph  ->  ( C  e.  Cat  /\  D  e.  Cat )
)
65simpld 456 . . . . . 6  |-  ( ph  ->  C  e.  Cat )
71, 2, 6idfu1st 14776 . . . . 5  |-  ( ph  ->  ( 1st `  I
)  =  (  _I  |`  ( Base `  C
) ) )
87coeq2d 4993 . . . 4  |-  ( ph  ->  ( ( 1st `  F
)  o.  ( 1st `  I ) )  =  ( ( 1st `  F
)  o.  (  _I  |`  ( Base `  C
) ) ) )
9 eqid 2437 . . . . . 6  |-  ( Base `  D )  =  (
Base `  D )
10 relfunc 14759 . . . . . . 7  |-  Rel  ( C  Func  D )
11 1st2ndbr 6616 . . . . . . 7  |-  ( ( Rel  ( C  Func  D )  /\  F  e.  ( C  Func  D
) )  ->  ( 1st `  F ) ( C  Func  D )
( 2nd `  F
) )
1210, 3, 11sylancr 658 . . . . . 6  |-  ( ph  ->  ( 1st `  F
) ( C  Func  D ) ( 2nd `  F
) )
132, 9, 12funcf1 14763 . . . . 5  |-  ( ph  ->  ( 1st `  F
) : ( Base `  C ) --> ( Base `  D ) )
14 fcoi1 5577 . . . . 5  |-  ( ( 1st `  F ) : ( Base `  C
) --> ( Base `  D
)  ->  ( ( 1st `  F )  o.  (  _I  |`  ( Base `  C ) ) )  =  ( 1st `  F ) )
1513, 14syl 16 . . . 4  |-  ( ph  ->  ( ( 1st `  F
)  o.  (  _I  |`  ( Base `  C
) ) )  =  ( 1st `  F
) )
168, 15eqtrd 2469 . . 3  |-  ( ph  ->  ( ( 1st `  F
)  o.  ( 1st `  I ) )  =  ( 1st `  F
) )
1773ad2ant1 1004 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( 1st `  I
)  =  (  _I  |`  ( Base `  C
) ) )
1817fveq1d 5685 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( ( 1st `  I ) `  x
)  =  ( (  _I  |`  ( Base `  C ) ) `  x ) )
19 fvresi 5895 . . . . . . . . . 10  |-  ( x  e.  ( Base `  C
)  ->  ( (  _I  |`  ( Base `  C
) ) `  x
)  =  x )
20193ad2ant2 1005 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( (  _I  |`  ( Base `  C
) ) `  x
)  =  x )
2118, 20eqtrd 2469 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( ( 1st `  I ) `  x
)  =  x )
2217fveq1d 5685 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( ( 1st `  I ) `  y
)  =  ( (  _I  |`  ( Base `  C ) ) `  y ) )
23 fvresi 5895 . . . . . . . . . 10  |-  ( y  e.  ( Base `  C
)  ->  ( (  _I  |`  ( Base `  C
) ) `  y
)  =  y )
24233ad2ant3 1006 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( (  _I  |`  ( Base `  C
) ) `  y
)  =  y )
2522, 24eqtrd 2469 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( ( 1st `  I ) `  y
)  =  y )
2621, 25oveq12d 6102 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( ( ( 1st `  I ) `
 x ) ( 2nd `  F ) ( ( 1st `  I
) `  y )
)  =  ( x ( 2nd `  F
) y ) )
2763ad2ant1 1004 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  C  e.  Cat )
28 eqid 2437 . . . . . . . 8  |-  ( Hom  `  C )  =  ( Hom  `  C )
29 simp2 984 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  x  e.  (
Base `  C )
)
30 simp3 985 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  y  e.  (
Base `  C )
)
311, 2, 27, 28, 29, 30idfu2nd 14774 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( x ( 2nd `  I ) y )  =  (  _I  |`  ( x
( Hom  `  C ) y ) ) )
3226, 31coeq12d 4995 . . . . . 6  |-  ( (
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 2437 . . . . . . . 8  |-  ( Hom  `  D )  =  ( Hom  `  D )
34123ad2ant1 1004 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( 1st `  F
) ( C  Func  D ) ( 2nd `  F
) )
352, 28, 33, 34, 29, 30funcf2 14765 . . . . . . 7  |-  ( (
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 5577 . . . . . . 7  |-  ( ( 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 ) )
3735, 36syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( Base `  C )  /\  y  e.  ( Base `  C ) )  ->  ( ( x ( 2nd `  F
) y )  o.  (  _I  |`  (
x ( Hom  `  C
) y ) ) )  =  ( x ( 2nd `  F
) y ) )
3832, 37eqtrd 2469 . . . . 5  |-  ( (
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 ) )
3938mpt2eq3dva 6143 . . . 4  |-  ( 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 ) ) )
402, 12funcfn2 14766 . . . . 5  |-  ( ph  ->  ( 2nd `  F
)  Fn  ( (
Base `  C )  X.  ( Base `  C
) ) )
41 fnov 6191 . . . . 5  |-  ( ( 2nd `  F )  Fn  ( ( Base `  C )  X.  ( Base `  C ) )  <-> 
( 2nd `  F
)  =  ( x  e.  ( Base `  C
) ,  y  e.  ( Base `  C
)  |->  ( x ( 2nd `  F ) y ) ) )
4240, 41sylib 196 . . . 4  |-  ( ph  ->  ( 2nd `  F
)  =  ( x  e.  ( Base `  C
) ,  y  e.  ( Base `  C
)  |->  ( x ( 2nd `  F ) y ) ) )
4339, 42eqtr4d 2472 . . 3  |-  ( ph  ->  ( x  e.  (
Base `  C ) ,  y  e.  ( Base `  C )  |->  ( ( ( ( 1st `  I ) `  x
) ( 2nd `  F
) ( ( 1st `  I ) `  y
) )  o.  (
x ( 2nd `  I
) y ) ) )  =  ( 2nd `  F ) )
4416, 43opeq12d 4059 . 2  |-  ( 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
) >. )
451idfucl 14778 . . . 4  |-  ( C  e.  Cat  ->  I  e.  ( C  Func  C
) )
466, 45syl 16 . . 3  |-  ( ph  ->  I  e.  ( C 
Func  C ) )
472, 46, 3cofuval 14779 . 2  |-  ( 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 6613 . . 3  |-  ( ( Rel  ( C  Func  D )  /\  F  e.  ( C  Func  D
) )  ->  F  =  <. ( 1st `  F
) ,  ( 2nd `  F ) >. )
4910, 3, 48sylancr 658 . 2  |-  ( ph  ->  F  =  <. ( 1st `  F ) ,  ( 2nd `  F
) >. )
5044, 47, 493eqtr4d 2479 1  |-  ( ph  ->  ( F  o.func  I )  =  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1757   <.cop 3875   class class class wbr 4284    _I cid 4622    X. cxp 4829    |` cres 4833    o. ccom 4835   Rel wrel 4836    Fn wfn 5405   -->wf 5406   ` cfv 5410  (class class class)co 6084    e. cmpt2 6086   1stc1st 6568   2ndc2nd 6569   Basecbs 14161   Hom chom 14236   Catccat 14589    Func cfunc 14751  idfunccidfu 14752    o.func ccofu 14753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-rep 4395  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-op 3876  df-uni 4084  df-iun 4165  df-br 4285  df-opab 4343  df-mpt 4344  df-id 4627  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-riota 6043  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6570  df-2nd 6571  df-map 7208  df-ixp 7256  df-cat 14593  df-cid 14594  df-func 14755  df-idfu 14756  df-cofu 14757
This theorem is referenced by:  catccatid  14957
  Copyright terms: Public domain W3C validator