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

Definition df-cid 13587
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.)
Assertion
Ref Expression
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 ) ) ) )
Distinct variable group:    b, c, f, g, h, o, x, y

Detailed syntax breakdown of Definition df-cid
StepHypRef Expression
1 ccid 13583 . 2  class  Id
2 vc . . 3  set  c
3 ccat 13582 . . 3  class  Cat
4 vb . . . 4  set  b
52cv 1631 . . . . 5  class  c
6 cbs 13164 . . . . 5  class  Base
75, 6cfv 5271 . . . 4  class  ( Base `  c )
8 vh . . . . 5  set  h
9 chom 13235 . . . . . 6  class  Hom
105, 9cfv 5271 . . . . 5  class  (  Hom  `  c )
11 vo . . . . . 6  set  o
12 cco 13236 . . . . . . 7  class comp
135, 12cfv 5271 . . . . . 6  class  (comp `  c )
14 vx . . . . . . 7  set  x
154cv 1631 . . . . . . 7  class  b
16 vg . . . . . . . . . . . . . 14  set  g
1716cv 1631 . . . . . . . . . . . . 13  class  g
18 vf . . . . . . . . . . . . . 14  set  f
1918cv 1631 . . . . . . . . . . . . 13  class  f
20 vy . . . . . . . . . . . . . . . 16  set  y
2120cv 1631 . . . . . . . . . . . . . . 15  class  y
2214cv 1631 . . . . . . . . . . . . . . 15  class  x
2321, 22cop 3656 . . . . . . . . . . . . . 14  class  <. y ,  x >.
2411cv 1631 . . . . . . . . . . . . . 14  class  o
2523, 22, 24co 5874 . . . . . . . . . . . . 13  class  ( <.
y ,  x >. o x )
2617, 19, 25co 5874 . . . . . . . . . . . 12  class  ( g ( <. y ,  x >. o x ) f )
2726, 19wceq 1632 . . . . . . . . . . 11  wff  ( g ( <. y ,  x >. o x ) f )  =  f
288cv 1631 . . . . . . . . . . . 12  class  h
2921, 22, 28co 5874 . . . . . . . . . . 11  class  ( y h x )
3027, 18, 29wral 2556 . . . . . . . . . 10  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
3122, 22cop 3656 . . . . . . . . . . . . . 14  class  <. x ,  x >.
3231, 21, 24co 5874 . . . . . . . . . . . . 13  class  ( <.
x ,  x >. o y )
3319, 17, 32co 5874 . . . . . . . . . . . 12  class  ( f ( <. x ,  x >. o y ) g )
3433, 19wceq 1632 . . . . . . . . . . 11  wff  ( f ( <. x ,  x >. o y ) g )  =  f
3522, 21, 28co 5874 . . . . . . . . . . 11  class  ( x h y )
3634, 18, 35wral 2556 . . . . . . . . . 10  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
3730, 36wa 358 . . . . . . . . 9  wff  ( 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 )
3837, 20, 15wral 2556 . . . . . . . 8  wff  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 )
3922, 22, 28co 5874 . . . . . . . 8  class  ( x h x )
4038, 16, 39crio 6313 . . . . . . 7  class  ( 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 ) )
4114, 15, 40cmpt 4093 . . . . . 6  class  ( 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 ) ) )
4211, 13, 41csb 3094 . . . . 5  class  [_ (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 ) ) )
438, 10, 42csb 3094 . . . 4  class  [_ (  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 ) ) )
444, 7, 43csb 3094 . . 3  class  [_ ( 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 ) ) )
452, 3, 44cmpt 4093 . 2  class  ( 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 ) ) ) )
461, 45wceq 1632 1  wff  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 ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  cidfval  13594  cidffn  13596
  Copyright terms: Public domain W3C validator