Definition df-nat 16603

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.)

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

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

This definition is referenced by:  natfval  16606