Metamath Proof Explorer

Definition df-ida

Description: Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007) (Revised by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-ida 
|- IdA = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cida 
 |-  IdA
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  c
6 5 4 cfv 
 |-  ( Base ` c )
7 3 cv 
 |-  x
8 ccid 
 |-  Id
9 5 8 cfv 
 |-  ( Id ` c )
10 7 9 cfv 
 |-  ( ( Id ` c ) ` x )
11 7 7 10 cotp 
 |-  <. x , x , ( ( Id ` c ) ` x ) >.
12 3 6 11 cmpt 
 |-  ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. )
13 1 2 12 cmpt 
 |-  ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )
14 0 13 wceq 
 |-  IdA = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )