MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-idfu Unicode version

Definition df-idfu 13749
Description: Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-idfu  |- idfunc  =  ( t  e. 
Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
Distinct variable group:    t, b, z

Detailed syntax breakdown of Definition df-idfu
StepHypRef Expression
1 cidfu 13745 . 2  class idfunc
2 vt . . 3  set  t
3 ccat 13582 . . 3  class  Cat
4 vb . . . 4  set  b
52cv 1631 . . . . 5  class  t
6 cbs 13164 . . . . 5  class  Base
75, 6cfv 5271 . . . 4  class  ( Base `  t )
8 cid 4320 . . . . . 6  class  _I
94cv 1631 . . . . . 6  class  b
108, 9cres 4707 . . . . 5  class  (  _I  |`  b )
11 vz . . . . . 6  set  z
129, 9cxp 4703 . . . . . 6  class  ( b  X.  b )
1311cv 1631 . . . . . . . 8  class  z
14 chom 13235 . . . . . . . . 9  class  Hom
155, 14cfv 5271 . . . . . . . 8  class  (  Hom  `  t )
1613, 15cfv 5271 . . . . . . 7  class  ( (  Hom  `  t ) `  z )
178, 16cres 4707 . . . . . 6  class  (  _I  |`  ( (  Hom  `  t
) `  z )
)
1811, 12, 17cmpt 4093 . . . . 5  class  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) )
1910, 18cop 3656 . . . 4  class  <. (  _I  |`  b ) ,  ( z  e.  ( b  X.  b ) 
|->  (  _I  |`  (
(  Hom  `  t ) `
 z ) ) ) >.
204, 7, 19csb 3094 . . 3  class  [_ ( Base `  t )  / 
b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >.
212, 3, 20cmpt 4093 . 2  class  ( t  e.  Cat  |->  [_ ( Base `  t )  / 
b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
221, 21wceq 1632 1  wff idfunc  =  ( t  e. 
Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
Colors of variables: wff set class
This definition is referenced by:  idfuval  13766
  Copyright terms: Public domain W3C validator