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

Definition df-cid 15653
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 15649 . 2  class  Id
2 vc . . 3  setvar  c
3 ccat 15648 . . 3  class  Cat
4 vb . . . 4  setvar  b
52cv 1451 . . . . 5  class  c
6 cbs 15199 . . . . 5  class  Base
75, 6cfv 5589 . . . 4  class  ( Base `  c )
8 vh . . . . 5  setvar  h
9 chom 15279 . . . . . 6  class  Hom
105, 9cfv 5589 . . . . 5  class  ( Hom  `  c )
11 vo . . . . . 6  setvar  o
12 cco 15280 . . . . . . 7  class comp
135, 12cfv 5589 . . . . . 6  class  (comp `  c )
14 vx . . . . . . 7  setvar  x
154cv 1451 . . . . . . 7  class  b
16 vg . . . . . . . . . . . . . 14  setvar  g
1716cv 1451 . . . . . . . . . . . . 13  class  g
18 vf . . . . . . . . . . . . . 14  setvar  f
1918cv 1451 . . . . . . . . . . . . 13  class  f
20 vy . . . . . . . . . . . . . . . 16  setvar  y
2120cv 1451 . . . . . . . . . . . . . . 15  class  y
2214cv 1451 . . . . . . . . . . . . . . 15  class  x
2321, 22cop 3965 . . . . . . . . . . . . . 14  class  <. y ,  x >.
2411cv 1451 . . . . . . . . . . . . . 14  class  o
2523, 22, 24co 6308 . . . . . . . . . . . . 13  class  ( <.
y ,  x >. o x )
2617, 19, 25co 6308 . . . . . . . . . . . 12  class  ( g ( <. y ,  x >. o x ) f )
2726, 19wceq 1452 . . . . . . . . . . 11  wff  ( g ( <. y ,  x >. o x ) f )  =  f
288cv 1451 . . . . . . . . . . . 12  class  h
2921, 22, 28co 6308 . . . . . . . . . . 11  class  ( y h x )
3027, 18, 29wral 2756 . . . . . . . . . 10  wff  A. f  e.  ( y h x ) ( g (
<. y ,  x >. o x ) f )  =  f
3122, 22cop 3965 . . . . . . . . . . . . . 14  class  <. x ,  x >.
3231, 21, 24co 6308 . . . . . . . . . . . . 13  class  ( <.
x ,  x >. o y )
3319, 17, 32co 6308 . . . . . . . . . . . 12  class  ( f ( <. x ,  x >. o y ) g )
3433, 19wceq 1452 . . . . . . . . . . 11  wff  ( f ( <. x ,  x >. o y ) g )  =  f
3522, 21, 28co 6308 . . . . . . . . . . 11  class  ( x h y )
3634, 18, 35wral 2756 . . . . . . . . . 10  wff  A. f  e.  ( x h y ) ( f (
<. x ,  x >. o y ) g )  =  f
3730, 36wa 376 . . . . . . . . 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 2756 . . . . . . . 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 6308 . . . . . . . 8  class  ( x h x )
4038, 16, 39crio 6269 . . . . . . 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 4454 . . . . . 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 3349 . . . . 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 3349 . . . 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 3349 . . 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 4454 . 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 1452 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  15660  cidffn  15662
  Copyright terms: Public domain W3C validator