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

Definition df-idfu 14781
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 14777 . 2  class idfunc
2 vt . . 3  setvar  t
3 ccat 14614 . . 3  class  Cat
4 vb . . . 4  setvar  b
52cv 1368 . . . . 5  class  t
6 cbs 14186 . . . . 5  class  Base
75, 6cfv 5430 . . . 4  class  ( Base `  t )
8 cid 4643 . . . . . 6  class  _I
94cv 1368 . . . . . 6  class  b
108, 9cres 4854 . . . . 5  class  (  _I  |`  b )
11 vz . . . . . 6  setvar  z
129, 9cxp 4850 . . . . . 6  class  ( b  X.  b )
1311cv 1368 . . . . . . . 8  class  z
14 chom 14261 . . . . . . . . 9  class  Hom
155, 14cfv 5430 . . . . . . . 8  class  ( Hom  `  t )
1613, 15cfv 5430 . . . . . . 7  class  ( ( Hom  `  t ) `  z )
178, 16cres 4854 . . . . . 6  class  (  _I  |`  ( ( Hom  `  t
) `  z )
)
1811, 12, 17cmpt 4362 . . . . 5  class  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( ( Hom  `  t
) `  z )
) )
1910, 18cop 3895 . . . 4  class  <. (  _I  |`  b ) ,  ( z  e.  ( b  X.  b ) 
|->  (  _I  |`  (
( Hom  `  t ) `
 z ) ) ) >.
204, 7, 19csb 3300 . . 3  class  [_ ( Base `  t )  / 
b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( ( Hom  `  t
) `  z )
) ) >.
212, 3, 20cmpt 4362 . 2  class  ( t  e.  Cat  |->  [_ ( Base `  t )  / 
b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( ( Hom  `  t
) `  z )
) ) >. )
221, 21wceq 1369 1  wff idfunc  =  ( t  e. 
Cat  |->  [_ ( Base `  t
)  /  b ]_ <. (  _I  |`  b
) ,  ( z  e.  ( b  X.  b )  |->  (  _I  |`  ( ( Hom  `  t
) `  z )
) ) >. )
Colors of variables: wff setvar class
This definition is referenced by:  idfuval  14798
  Copyright terms: Public domain W3C validator