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

Definition df-cid 14590
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 14586 . 2  class  Id
2 vc . . 3  setvar  c
3 ccat 14585 . . 3  class  Cat
4 vb . . . 4  setvar  b
52cv 1361 . . . . 5  class  c
6 cbs 14157 . . . . 5  class  Base
75, 6cfv 5406 . . . 4  class  ( Base `  c )
8 vh . . . . 5  setvar  h
9 chom 14232 . . . . . 6  class  Hom
105, 9cfv 5406 . . . . 5  class  ( Hom  `  c )
11 vo . . . . . 6  setvar  o
12 cco 14233 . . . . . . 7  class comp
135, 12cfv 5406 . . . . . 6  class  (comp `  c )
14 vx . . . . . . 7  setvar  x
154cv 1361 . . . . . . 7  class  b
16 vg . . . . . . . . . . . . . 14  setvar  g
1716cv 1361 . . . . . . . . . . . . 13  class  g
18 vf . . . . . . . . . . . . . 14  setvar  f
1918cv 1361 . . . . . . . . . . . . 13  class  f
20 vy . . . . . . . . . . . . . . . 16  setvar  y
2120cv 1361 . . . . . . . . . . . . . . 15  class  y
2214cv 1361 . . . . . . . . . . . . . . 15  class  x
2321, 22cop 3871 . . . . . . . . . . . . . 14  class  <. y ,  x >.
2411cv 1361 . . . . . . . . . . . . . 14  class  o
2523, 22, 24co 6080 . . . . . . . . . . . . 13  class  ( <.
y ,  x >. o x )
2617, 19, 25co 6080 . . . . . . . . . . . 12  class  ( g ( <. y ,  x >. o x ) f )
2726, 19wceq 1362 . . . . . . . . . . 11  wff  ( g ( <. y ,  x >. o x ) f )  =  f
288cv 1361 . . . . . . . . . . . 12  class  h
2921, 22, 28co 6080 . . . . . . . . . . 11  class  ( y h x )
3027, 18, 29wral 2705 . . . . . . . . . 10  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
3122, 22cop 3871 . . . . . . . . . . . . . 14  class  <. x ,  x >.
3231, 21, 24co 6080 . . . . . . . . . . . . 13  class  ( <.
x ,  x >. o y )
3319, 17, 32co 6080 . . . . . . . . . . . 12  class  ( f ( <. x ,  x >. o y ) g )
3433, 19wceq 1362 . . . . . . . . . . 11  wff  ( f ( <. x ,  x >. o y ) g )  =  f
3522, 21, 28co 6080 . . . . . . . . . . 11  class  ( x h y )
3634, 18, 35wral 2705 . . . . . . . . . 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 2705 . . . . . . . 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 6080 . . . . . . . 8  class  ( x h x )
4038, 16, 39crio 6038 . . . . . . 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 4338 . . . . . 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 3276 . . . . 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 3276 . . . 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 3276 . . 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 4338 . 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 1362 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  14597  cidffn  14599
  Copyright terms: Public domain W3C validator