Metamath Proof Explorer

Definition df-nat

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 . Definition 6.1 in Adamek p. 83, and definition in Lang p. 65. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnat 
 |-  Nat
1 vt 
 |-  t
2 ccat 
 |-  Cat
3 vu 
 |-  u
4 vf 
 |-  f
5 1 cv 
 |-  t
6 cfunc 
 |-  Func
7 3 cv 
 |-  u
8 5 7 6 co 
 |-  ( t Func u )
9 vg 
 |-  g
10 c1st 
 |-  1st
11 4 cv 
 |-  f
12 11 10 cfv 
 |-  ( 1st ` f )
13 vr 
 |-  r
14 9 cv 
 |-  g
15 14 10 cfv 
 |-  ( 1st ` g )
16 vs 
 |-  s
17 va 
 |-  a
18 vx 
 |-  x
19 cbs 
 |-  Base
20 5 19 cfv 
 |-  ( Base ` t )
21 13 cv 
 |-  r
22 18 cv 
 |-  x
23 22 21 cfv 
 |-  ( r ` x )
24 chom 
 |-  Hom
25 7 24 cfv 
 |-  ( Hom ` u )
26 16 cv 
 |-  s
27 22 26 cfv 
 |-  ( s ` x )
28 23 27 25 co 
 |-  ( ( r ` x ) ( Hom ` u ) ( s ` x ) )
29 18 20 28 cixp 
 |-  X_ x e. ( Base ` t ) ( ( r ` x ) ( Hom ` u ) ( s ` x ) )
30 vy 
 |-  y
31 vh 
 |-  h
32 5 24 cfv 
 |-  ( Hom ` t )
33 30 cv 
 |-  y
34 22 33 32 co 
 |-  ( x ( Hom ` t ) y )
35 17 cv 
 |-  a
36 33 35 cfv 
 |-  ( a ` y )
37 33 21 cfv 
 |-  ( r ` y )
38 23 37 cop 
 |-  <. ( r ` x ) , ( r ` y ) >.
39 cco 
 |-  comp
40 7 39 cfv 
 |-  ( comp ` u )
41 33 26 cfv 
 |-  ( s ` y )
42 38 41 40 co 
 |-  ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) )
43 c2nd 
 |-  2nd
44 11 43 cfv 
 |-  ( 2nd ` f )
45 22 33 44 co 
 |-  ( x ( 2nd ` f ) y )
46 31 cv 
 |-  h
47 46 45 cfv 
 |-  ( ( x ( 2nd ` f ) y ) ` h )
48 36 47 42 co 
 |-  ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` u ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) )
49 14 43 cfv 
 |-  ( 2nd ` g )
50 22 33 49 co 
 |-  ( x ( 2nd ` g ) y )
51 46 50 cfv 
 |-  ( ( x ( 2nd ` g ) y ) ` h )
52 23 27 cop 
 |-  <. ( r ` x ) , ( s ` x ) >.
53 52 41 40 co 
 |-  ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) )
54 22 35 cfv 
 |-  ( a ` x )
55 51 54 53 co 
 |-  ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` u ) ( s ` y ) ) ( a ` x ) )
56 48 55 wceq 
 |-  ( ( 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 ) )
57 56 31 34 wral 
 |-  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 ) )
58 57 30 20 wral 
 |-  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 ) )
59 58 18 20 wral 
 |-  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 ) )
60 59 17 29 crab 
 |-  { 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 ) ) }
61 16 15 60 csb 
 |-  [_ ( 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 ) ) }
62 13 12 61 csb 
 |-  [_ ( 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 ) ) }
63 4 9 8 8 62 cmpo 
 |-  ( 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 ) ) } )
64 1 3 2 2 63 cmpo 
 |-  ( 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 ) ) } ) )
65 0 64 wceq 
 |-  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 ) ) } ) )