Metamath Proof Explorer

Definition df-idfu

Description: Define the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-idfu 
|- idFunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cidfu 
 |-  idFunc
1 vt 
 |-  t
2 ccat 
 |-  Cat
3 cbs 
 |-  Base
4 1 cv 
 |-  t
5 4 3 cfv 
 |-  ( Base ` t )
6 vb 
 |-  b
7 cid 
 |-  _I
8 6 cv 
 |-  b
9 7 8 cres 
 |-  ( _I |` b )
10 vz 
 |-  z
11 8 8 cxp 
 |-  ( b X. b )
12 chom 
 |-  Hom
13 4 12 cfv 
 |-  ( Hom ` t )
14 10 cv 
 |-  z
15 14 13 cfv 
 |-  ( ( Hom ` t ) ` z )
16 7 15 cres 
 |-  ( _I |` ( ( Hom ` t ) ` z ) )
17 10 11 16 cmpt 
 |-  ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) )
18 9 17 cop 
 |-  <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >.
19 6 5 18 csb 
 |-  [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >.
20 1 2 19 cmpt 
 |-  ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )
21 0 20 wceq 
 |-  idFunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )