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

Definition df-cid 14610
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 14606 . 2  class  Id
2 vc . . 3  setvar  c
3 ccat 14605 . . 3  class  Cat
4 vb . . . 4  setvar  b
52cv 1368 . . . . 5  class  c
6 cbs 14177 . . . . 5  class  Base
75, 6cfv 5421 . . . 4  class  ( Base `  c )
8 vh . . . . 5  setvar  h
9 chom 14252 . . . . . 6  class  Hom
105, 9cfv 5421 . . . . 5  class  ( Hom  `  c )
11 vo . . . . . 6  setvar  o
12 cco 14253 . . . . . . 7  class comp
135, 12cfv 5421 . . . . . 6  class  (comp `  c )
14 vx . . . . . . 7  setvar  x
154cv 1368 . . . . . . 7  class  b
16 vg . . . . . . . . . . . . . 14  setvar  g
1716cv 1368 . . . . . . . . . . . . 13  class  g
18 vf . . . . . . . . . . . . . 14  setvar  f
1918cv 1368 . . . . . . . . . . . . 13  class  f
20 vy . . . . . . . . . . . . . . . 16  setvar  y
2120cv 1368 . . . . . . . . . . . . . . 15  class  y
2214cv 1368 . . . . . . . . . . . . . . 15  class  x
2321, 22cop 3886 . . . . . . . . . . . . . 14  class  <. y ,  x >.
2411cv 1368 . . . . . . . . . . . . . 14  class  o
2523, 22, 24co 6094 . . . . . . . . . . . . 13  class  ( <.
y ,  x >. o x )
2617, 19, 25co 6094 . . . . . . . . . . . 12  class  ( g ( <. y ,  x >. o x ) f )
2726, 19wceq 1369 . . . . . . . . . . 11  wff  ( g ( <. y ,  x >. o x ) f )  =  f
288cv 1368 . . . . . . . . . . . 12  class  h
2921, 22, 28co 6094 . . . . . . . . . . 11  class  ( y h x )
3027, 18, 29wral 2718 . . . . . . . . . 10  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
3122, 22cop 3886 . . . . . . . . . . . . . 14  class  <. x ,  x >.
3231, 21, 24co 6094 . . . . . . . . . . . . 13  class  ( <.
x ,  x >. o y )
3319, 17, 32co 6094 . . . . . . . . . . . 12  class  ( f ( <. x ,  x >. o y ) g )
3433, 19wceq 1369 . . . . . . . . . . 11  wff  ( f ( <. x ,  x >. o y ) g )  =  f
3522, 21, 28co 6094 . . . . . . . . . . 11  class  ( x h y )
3634, 18, 35wral 2718 . . . . . . . . . 10  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
3730, 36wa 369 . . . . . . . . 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 2718 . . . . . . . 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 6094 . . . . . . . 8  class  ( x h x )
4038, 16, 39crio 6054 . . . . . . 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 4353 . . . . . 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 3291 . . . . 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 3291 . . . 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 3291 . . 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 4353 . 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 1369 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  14617  cidffn  14619
  Copyright terms: Public domain W3C validator