Metamath Proof Explorer

Definition df-cid

Description: Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-cid 
|- Id = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccid 
 |-  Id
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 cbs 
 |-  Base
4 1 cv 
 |-  c
5 4 3 cfv 
 |-  ( Base ` c )
6 vb 
 |-  b
7 chom 
 |-  Hom
8 4 7 cfv 
 |-  ( Hom ` c )
9 vh 
 |-  h
10 cco 
 |-  comp
11 4 10 cfv 
 |-  ( comp ` c )
12 vo 
 |-  o
13 vx 
 |-  x
14 6 cv 
 |-  b
15 vg 
 |-  g
16 13 cv 
 |-  x
17 9 cv 
 |-  h
18 16 16 17 co 
 |-  ( x h x )
19 vy 
 |-  y
20 vf 
 |-  f
21 19 cv 
 |-  y
22 21 16 17 co 
 |-  ( y h x )
23 15 cv 
 |-  g
24 21 16 cop 
 |-  <. y , x >.
25 12 cv 
 |-  o
26 24 16 25 co 
 |-  ( <. y , x >. o x )
27 20 cv 
 |-  f
28 23 27 26 co 
 |-  ( g ( <. y , x >. o x ) f )
29 28 27 wceq 
 |-  ( g ( <. y , x >. o x ) f ) = f
30 29 20 22 wral 
 |-  A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f
31 16 21 17 co 
 |-  ( x h y )
32 16 16 cop 
 |-  <. x , x >.
33 32 21 25 co 
 |-  ( <. x , x >. o y )
34 27 23 33 co 
 |-  ( f ( <. x , x >. o y ) g )
35 34 27 wceq 
 |-  ( f ( <. x , x >. o y ) g ) = f
36 35 20 31 wral 
 |-  A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f
37 30 36 wa 
 |-  ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
38 37 19 14 wral 
 |-  A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f )
39 38 15 18 crio 
 |-  ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) )
40 13 14 39 cmpt 
 |-  ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
41 12 11 40 csb 
 |-  [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
42 9 8 41 csb 
 |-  [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
43 6 5 42 csb 
 |-  [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) )
44 1 2 43 cmpt 
 |-  ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )
45 0 44 wceq 
 |-  Id = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )