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

Definition df-nat 13833
Description: Definition of a natural transformation between two functors. A natural transformation  A : F --> G is a collection of arrows  A ( x ) : F ( x ) --> G ( x ), such that  A ( y )  o.  F ( h )  =  G ( h )  o.  A ( x ) for each morphism  h : x --> y. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
df-nat  |- Nat  =  ( t  e.  Cat ,  u  e.  Cat  |->  ( f  e.  ( t  Func  u ) ,  g  e.  ( t  Func  u
)  |->  [_ ( 1st `  f
)  /  r ]_ [_ ( 1st `  g
)  /  s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) } ) )
Distinct variable group:    f, a, g, h, r, s, t, u, x, y

Detailed syntax breakdown of Definition df-nat
StepHypRef Expression
1 cnat 13831 . 2  class Nat
2 vt . . 3  set  t
3 vu . . 3  set  u
4 ccat 13582 . . 3  class  Cat
5 vf . . . 4  set  f
6 vg . . . 4  set  g
72cv 1631 . . . . 5  class  t
83cv 1631 . . . . 5  class  u
9 cfunc 13744 . . . . 5  class  Func
107, 8, 9co 5874 . . . 4  class  ( t 
Func  u )
11 vr . . . . 5  set  r
125cv 1631 . . . . . 6  class  f
13 c1st 6136 . . . . . 6  class  1st
1412, 13cfv 5271 . . . . 5  class  ( 1st `  f )
15 vs . . . . . 6  set  s
166cv 1631 . . . . . . 7  class  g
1716, 13cfv 5271 . . . . . 6  class  ( 1st `  g )
18 vy . . . . . . . . . . . . . 14  set  y
1918cv 1631 . . . . . . . . . . . . 13  class  y
20 va . . . . . . . . . . . . . 14  set  a
2120cv 1631 . . . . . . . . . . . . 13  class  a
2219, 21cfv 5271 . . . . . . . . . . . 12  class  ( a `
 y )
23 vh . . . . . . . . . . . . . 14  set  h
2423cv 1631 . . . . . . . . . . . . 13  class  h
25 vx . . . . . . . . . . . . . . 15  set  x
2625cv 1631 . . . . . . . . . . . . . 14  class  x
27 c2nd 6137 . . . . . . . . . . . . . . 15  class  2nd
2812, 27cfv 5271 . . . . . . . . . . . . . 14  class  ( 2nd `  f )
2926, 19, 28co 5874 . . . . . . . . . . . . 13  class  ( x ( 2nd `  f
) y )
3024, 29cfv 5271 . . . . . . . . . . . 12  class  ( ( x ( 2nd `  f
) y ) `  h )
3111cv 1631 . . . . . . . . . . . . . . 15  class  r
3226, 31cfv 5271 . . . . . . . . . . . . . 14  class  ( r `
 x )
3319, 31cfv 5271 . . . . . . . . . . . . . 14  class  ( r `
 y )
3432, 33cop 3656 . . . . . . . . . . . . 13  class  <. (
r `  x ) ,  ( r `  y ) >.
3515cv 1631 . . . . . . . . . . . . . 14  class  s
3619, 35cfv 5271 . . . . . . . . . . . . 13  class  ( s `
 y )
37 cco 13236 . . . . . . . . . . . . . 14  class comp
388, 37cfv 5271 . . . . . . . . . . . . 13  class  (comp `  u )
3934, 36, 38co 5874 . . . . . . . . . . . 12  class  ( <.
( r `  x
) ,  ( r `
 y ) >.
(comp `  u )
( s `  y
) )
4022, 30, 39co 5874 . . . . . . . . . . 11  class  ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )
4116, 27cfv 5271 . . . . . . . . . . . . . 14  class  ( 2nd `  g )
4226, 19, 41co 5874 . . . . . . . . . . . . 13  class  ( x ( 2nd `  g
) y )
4324, 42cfv 5271 . . . . . . . . . . . 12  class  ( ( x ( 2nd `  g
) y ) `  h )
4426, 21cfv 5271 . . . . . . . . . . . 12  class  ( a `
 x )
4526, 35cfv 5271 . . . . . . . . . . . . . 14  class  ( s `
 x )
4632, 45cop 3656 . . . . . . . . . . . . 13  class  <. (
r `  x ) ,  ( s `  x ) >.
4746, 36, 38co 5874 . . . . . . . . . . . 12  class  ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) )
4843, 44, 47co 5874 . . . . . . . . . . 11  class  ( ( ( x ( 2nd `  g ) y ) `
 h ) (
<. ( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) )
4940, 48wceq 1632 . . . . . . . . . 10  wff  ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) )
50 chom 13235 . . . . . . . . . . . 12  class  Hom
517, 50cfv 5271 . . . . . . . . . . 11  class  (  Hom  `  t )
5226, 19, 51co 5874 . . . . . . . . . 10  class  ( x (  Hom  `  t
) y )
5349, 23, 52wral 2556 . . . . . . . . 9  wff  A. h  e.  ( x (  Hom  `  t ) y ) ( ( a `  y ) ( <.
( r `  x
) ,  ( r `
 y ) >.
(comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) )
54 cbs 13164 . . . . . . . . . 10  class  Base
557, 54cfv 5271 . . . . . . . . 9  class  ( Base `  t )
5653, 18, 55wral 2556 . . . . . . . 8  wff  A. y  e.  ( Base `  t
) A. h  e.  ( x (  Hom  `  t ) y ) ( ( a `  y ) ( <.
( r `  x
) ,  ( r `
 y ) >.
(comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) )
5756, 25, 55wral 2556 . . . . . . 7  wff  A. x  e.  ( Base `  t
) A. y  e.  ( Base `  t
) A. h  e.  ( x (  Hom  `  t ) y ) ( ( a `  y ) ( <.
( r `  x
) ,  ( r `
 y ) >.
(comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) )
588, 50cfv 5271 . . . . . . . . 9  class  (  Hom  `  u )
5932, 45, 58co 5874 . . . . . . . 8  class  ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )
6025, 55, 59cixp 6833 . . . . . . 7  class  X_ x  e.  ( Base `  t
) ( ( r `
 x ) (  Hom  `  u )
( s `  x
) )
6157, 20, 60crab 2560 . . . . . 6  class  { a  e.  X_ x  e.  (
Base `  t )
( ( r `  x ) (  Hom  `  u ) ( s `
 x ) )  |  A. x  e.  ( Base `  t
) A. y  e.  ( Base `  t
) A. h  e.  ( x (  Hom  `  t ) y ) ( ( a `  y ) ( <.
( r `  x
) ,  ( r `
 y ) >.
(comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) }
6215, 17, 61csb 3094 . . . . 5  class  [_ ( 1st `  g )  / 
s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x
) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) }
6311, 14, 62csb 3094 . . . 4  class  [_ ( 1st `  f )  / 
r ]_ [_ ( 1st `  g )  /  s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) }
645, 6, 10, 10, 63cmpt2 5876 . . 3  class  ( f  e.  ( t  Func  u ) ,  g  e.  ( t  Func  u
)  |->  [_ ( 1st `  f
)  /  r ]_ [_ ( 1st `  g
)  /  s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) } )
652, 3, 4, 4, 64cmpt2 5876 . 2  class  ( t  e.  Cat ,  u  e.  Cat  |->  ( f  e.  ( t  Func  u
) ,  g  e.  ( t  Func  u
)  |->  [_ ( 1st `  f
)  /  r ]_ [_ ( 1st `  g
)  /  s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) } ) )
661, 65wceq 1632 1  wff Nat  =  ( t  e.  Cat ,  u  e.  Cat  |->  ( f  e.  ( t  Func  u ) ,  g  e.  ( t  Func  u
)  |->  [_ ( 1st `  f
)  /  r ]_ [_ ( 1st `  g
)  /  s ]_ { a  e.  X_ x  e.  ( Base `  t ) ( ( r `  x ) (  Hom  `  u
) ( s `  x ) )  | 
A. x  e.  (
Base `  t ) A. y  e.  ( Base `  t ) A. h  e.  ( x
(  Hom  `  t ) y ) ( ( a `  y ) ( <. ( r `  x ) ,  ( r `  y )
>. (comp `  u )
( s `  y
) ) ( ( x ( 2nd `  f
) y ) `  h ) )  =  ( ( ( x ( 2nd `  g
) y ) `  h ) ( <.
( r `  x
) ,  ( s `
 x ) >.
(comp `  u )
( s `  y
) ) ( a `
 x ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  natfval  13836
  Copyright terms: Public domain W3C validator