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

Definition df-cid 15076
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 15072 . 2  class  Id
2 vc . . 3  setvar  c
3 ccat 15071 . . 3  class  Cat
4 vb . . . 4  setvar  b
52cv 1398 . . . . 5  class  c
6 cbs 14634 . . . . 5  class  Base
75, 6cfv 5496 . . . 4  class  ( Base `  c )
8 vh . . . . 5  setvar  h
9 chom 14713 . . . . . 6  class  Hom
105, 9cfv 5496 . . . . 5  class  ( Hom  `  c )
11 vo . . . . . 6  setvar  o
12 cco 14714 . . . . . . 7  class comp
135, 12cfv 5496 . . . . . 6  class  (comp `  c )
14 vx . . . . . . 7  setvar  x
154cv 1398 . . . . . . 7  class  b
16 vg . . . . . . . . . . . . . 14  setvar  g
1716cv 1398 . . . . . . . . . . . . 13  class  g
18 vf . . . . . . . . . . . . . 14  setvar  f
1918cv 1398 . . . . . . . . . . . . 13  class  f
20 vy . . . . . . . . . . . . . . . 16  setvar  y
2120cv 1398 . . . . . . . . . . . . . . 15  class  y
2214cv 1398 . . . . . . . . . . . . . . 15  class  x
2321, 22cop 3950 . . . . . . . . . . . . . 14  class  <. y ,  x >.
2411cv 1398 . . . . . . . . . . . . . 14  class  o
2523, 22, 24co 6196 . . . . . . . . . . . . 13  class  ( <.
y ,  x >. o x )
2617, 19, 25co 6196 . . . . . . . . . . . 12  class  ( g ( <. y ,  x >. o x ) f )
2726, 19wceq 1399 . . . . . . . . . . 11  wff  ( g ( <. y ,  x >. o x ) f )  =  f
288cv 1398 . . . . . . . . . . . 12  class  h
2921, 22, 28co 6196 . . . . . . . . . . 11  class  ( y h x )
3027, 18, 29wral 2732 . . . . . . . . . 10  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
3122, 22cop 3950 . . . . . . . . . . . . . 14  class  <. x ,  x >.
3231, 21, 24co 6196 . . . . . . . . . . . . 13  class  ( <.
x ,  x >. o y )
3319, 17, 32co 6196 . . . . . . . . . . . 12  class  ( f ( <. x ,  x >. o y ) g )
3433, 19wceq 1399 . . . . . . . . . . 11  wff  ( f ( <. x ,  x >. o y ) g )  =  f
3522, 21, 28co 6196 . . . . . . . . . . 11  class  ( x h y )
3634, 18, 35wral 2732 . . . . . . . . . 10  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
3730, 36wa 367 . . . . . . . . 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 2732 . . . . . . . 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 6196 . . . . . . . 8  class  ( x h x )
4038, 16, 39crio 6157 . . . . . . 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 4425 . . . . . 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 3348 . . . . 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 3348 . . . 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 3348 . . 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 4425 . 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 1399 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 setvar class
This definition is referenced by:  cidfval  15083  cidffn  15085
  Copyright terms: Public domain W3C validator