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

Definition df-cid 13822
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 13818 . 2  class  Id
2 vc . . 3  set  c
3 ccat 13817 . . 3  class  Cat
4 vb . . . 4  set  b
52cv 1648 . . . . 5  class  c
6 cbs 13397 . . . . 5  class  Base
75, 6cfv 5395 . . . 4  class  ( Base `  c )
8 vh . . . . 5  set  h
9 chom 13468 . . . . . 6  class  Hom
105, 9cfv 5395 . . . . 5  class  (  Hom  `  c )
11 vo . . . . . 6  set  o
12 cco 13469 . . . . . . 7  class comp
135, 12cfv 5395 . . . . . 6  class  (comp `  c )
14 vx . . . . . . 7  set  x
154cv 1648 . . . . . . 7  class  b
16 vg . . . . . . . . . . . . . 14  set  g
1716cv 1648 . . . . . . . . . . . . 13  class  g
18 vf . . . . . . . . . . . . . 14  set  f
1918cv 1648 . . . . . . . . . . . . 13  class  f
20 vy . . . . . . . . . . . . . . . 16  set  y
2120cv 1648 . . . . . . . . . . . . . . 15  class  y
2214cv 1648 . . . . . . . . . . . . . . 15  class  x
2321, 22cop 3761 . . . . . . . . . . . . . 14  class  <. y ,  x >.
2411cv 1648 . . . . . . . . . . . . . 14  class  o
2523, 22, 24co 6021 . . . . . . . . . . . . 13  class  ( <.
y ,  x >. o x )
2617, 19, 25co 6021 . . . . . . . . . . . 12  class  ( g ( <. y ,  x >. o x ) f )
2726, 19wceq 1649 . . . . . . . . . . 11  wff  ( g ( <. y ,  x >. o x ) f )  =  f
288cv 1648 . . . . . . . . . . . 12  class  h
2921, 22, 28co 6021 . . . . . . . . . . 11  class  ( y h x )
3027, 18, 29wral 2650 . . . . . . . . . 10  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
3122, 22cop 3761 . . . . . . . . . . . . . 14  class  <. x ,  x >.
3231, 21, 24co 6021 . . . . . . . . . . . . 13  class  ( <.
x ,  x >. o y )
3319, 17, 32co 6021 . . . . . . . . . . . 12  class  ( f ( <. x ,  x >. o y ) g )
3433, 19wceq 1649 . . . . . . . . . . 11  wff  ( f ( <. x ,  x >. o y ) g )  =  f
3522, 21, 28co 6021 . . . . . . . . . . 11  class  ( x h y )
3634, 18, 35wral 2650 . . . . . . . . . 10  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
3730, 36wa 359 . . . . . . . . 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 2650 . . . . . . . 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 6021 . . . . . . . 8  class  ( x h x )
4038, 16, 39crio 6479 . . . . . . 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 4208 . . . . . 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 3195 . . . . 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 3195 . . . 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 3195 . . 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 4208 . 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 1649 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  13829  cidffn  13831
  Copyright terms: Public domain W3C validator