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

Definition df-idfu 13733
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 13729 . 2  class idfunc
2 vt . . 3  set  t
3 ccat 13566 . . 3  class  Cat
4 vb . . . 4  set  b
52cv 1622 . . . . 5  class  t
6 cbs 13148 . . . . 5  class  Base
75, 6cfv 5255 . . . 4  class  ( Base `  t )
8 cid 4304 . . . . . 6  class  _I
94cv 1622 . . . . . 6  class  b
108, 9cres 4691 . . . . 5  class  (  _I  |`  b )
11 vz . . . . . 6  set  z
129, 9cxp 4687 . . . . . 6  class  ( b  X.  b )
1311cv 1622 . . . . . . . 8  class  z
14 chom 13219 . . . . . . . . 9  class  Hom
155, 14cfv 5255 . . . . . . . 8  class  (  Hom  `  t )
1613, 15cfv 5255 . . . . . . 7  class  ( (  Hom  `  t ) `  z )
178, 16cres 4691 . . . . . 6  class  (  _I  |`  ( (  Hom  `  t
) `  z )
)
1811, 12, 17cmpt 4077 . . . . 5  class  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) )
1910, 18cop 3643 . . . 4  class  <. (  _I  |`  b ) ,  ( z  e.  ( b  X.  b ) 
|->  (  _I  |`  (
(  Hom  `  t ) `
 z ) ) ) >.
204, 7, 19csb 3081 . . 3  class  [_ ( Base `  t )  / 
b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >.
212, 3, 20cmpt 4077 . 2  class  ( t  e.  Cat  |->  [_ ( Base `  t )  / 
b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( (  Hom  `  t
) `  z )
) ) >. )
221, 21wceq 1623 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  13750
  Copyright terms: Public domain W3C validator