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 \in Cat, u \in Cat ⟼ (f \in (t Func u), g \in (t Func u) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) \| \forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x)\}))$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-nat

Detailed syntax breakdown