Definition df-nat 17575

Description: Definition of a natural transformation between two functors. A natural transformation 𝐴:𝐹⟶𝐺 is a collection of arrows 𝐴(𝑥):𝐹(𝑥)⟶𝐺(𝑥), such that 𝐴(𝑦) ∘ 𝐹(ℎ) = 𝐺(ℎ) ∘ 𝐴(𝑥) for each morphism ℎ:𝑥⟶𝑦. 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 = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}))

Distinct variable group:   𝑓,𝑎,𝑔,ℎ,𝑟,𝑠,𝑡,𝑢,𝑥,𝑦

Detailed syntax breakdown of Definition df-nat

Step	Hyp	Ref	Expression
1		cnat 17573	. 2 class Nat
2		vt	. . 3 setvar 𝑡
3		vu	. . 3 setvar 𝑢
4		ccat 17290	. . 3 class Cat
5		vf	. . . 4 setvar 𝑓
6		vg	. . . 4 setvar 𝑔
7	2	cv 1538	. . . . 5 class 𝑡
8	3	cv 1538	. . . . 5 class 𝑢
9		cfunc 17485	. . . . 5 class Func
10	7, 8, 9	co 7255	. . . 4 class (𝑡 Func 𝑢)
11		vr	. . . . 5 setvar 𝑟
12	5	cv 1538	. . . . . 6 class 𝑓
13		c1st 7802	. . . . . 6 class 1st
14	12, 13	cfv 6418	. . . . 5 class (1st ‘𝑓)
15		vs	. . . . . 6 setvar 𝑠
16	6	cv 1538	. . . . . . 7 class 𝑔
17	16, 13	cfv 6418	. . . . . 6 class (1st ‘𝑔)
18		vy	. . . . . . . . . . . . . 14 setvar 𝑦
19	18	cv 1538	. . . . . . . . . . . . 13 class 𝑦
20		va	. . . . . . . . . . . . . 14 setvar 𝑎
21	20	cv 1538	. . . . . . . . . . . . 13 class 𝑎
22	19, 21	cfv 6418	. . . . . . . . . . . 12 class (𝑎‘𝑦)
23		vh	. . . . . . . . . . . . . 14 setvar ℎ
24	23	cv 1538	. . . . . . . . . . . . 13 class ℎ
25		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
26	25	cv 1538	. . . . . . . . . . . . . 14 class 𝑥
27		c2nd 7803	. . . . . . . . . . . . . . 15 class 2nd
28	12, 27	cfv 6418	. . . . . . . . . . . . . 14 class (2nd ‘𝑓)
29	26, 19, 28	co 7255	. . . . . . . . . . . . 13 class (𝑥(2nd ‘𝑓)𝑦)
30	24, 29	cfv 6418	. . . . . . . . . . . 12 class ((𝑥(2nd ‘𝑓)𝑦)‘ℎ)
31	11	cv 1538	. . . . . . . . . . . . . . 15 class 𝑟
32	26, 31	cfv 6418	. . . . . . . . . . . . . 14 class (𝑟‘𝑥)
33	19, 31	cfv 6418	. . . . . . . . . . . . . 14 class (𝑟‘𝑦)
34	32, 33	cop 4564	. . . . . . . . . . . . 13 class ⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩
35	15	cv 1538	. . . . . . . . . . . . . 14 class 𝑠
36	19, 35	cfv 6418	. . . . . . . . . . . . 13 class (𝑠‘𝑦)
37		cco 16900	. . . . . . . . . . . . . 14 class comp
38	8, 37	cfv 6418	. . . . . . . . . . . . 13 class (comp‘𝑢)
39	34, 36, 38	co 7255	. . . . . . . . . . . 12 class (⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))
40	22, 30, 39	co 7255	. . . . . . . . . . 11 class ((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ))
41	16, 27	cfv 6418	. . . . . . . . . . . . . 14 class (2nd ‘𝑔)
42	26, 19, 41	co 7255	. . . . . . . . . . . . 13 class (𝑥(2nd ‘𝑔)𝑦)
43	24, 42	cfv 6418	. . . . . . . . . . . 12 class ((𝑥(2nd ‘𝑔)𝑦)‘ℎ)
44	26, 21	cfv 6418	. . . . . . . . . . . 12 class (𝑎‘𝑥)
45	26, 35	cfv 6418	. . . . . . . . . . . . . 14 class (𝑠‘𝑥)
46	32, 45	cop 4564	. . . . . . . . . . . . 13 class ⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩
47	46, 36, 38	co 7255	. . . . . . . . . . . 12 class (⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))
48	43, 44, 47	co 7255	. . . . . . . . . . 11 class (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))
49	40, 48	wceq 1539	. . . . . . . . . 10 wff ((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))
50		chom 16899	. . . . . . . . . . . 12 class Hom
51	7, 50	cfv 6418	. . . . . . . . . . 11 class (Hom ‘𝑡)
52	26, 19, 51	co 7255	. . . . . . . . . 10 class (𝑥(Hom ‘𝑡)𝑦)
53	49, 23, 52	wral 3063	. . . . . . . . 9 wff ∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))
54		cbs 16840	. . . . . . . . . 10 class Base
55	7, 54	cfv 6418	. . . . . . . . 9 class (Base‘𝑡)
56	53, 18, 55	wral 3063	. . . . . . . 8 wff ∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))
57	56, 25, 55	wral 3063	. . . . . . 7 wff ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))
58	8, 50	cfv 6418	. . . . . . . . 9 class (Hom ‘𝑢)
59	32, 45, 58	co 7255	. . . . . . . 8 class ((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥))
60	25, 55, 59	cixp 8643	. . . . . . 7 class X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥))
61	57, 20, 60	crab 3067	. . . . . 6 class {𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}
62	15, 17, 61	csb 3828	. . . . 5 class ⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}
63	11, 14, 62	csb 3828	. . . 4 class ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}
64	5, 6, 10, 10, 63	cmpo 7257	. . 3 class (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))})
65	2, 3, 4, 4, 64	cmpo 7257	. 2 class (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}))
66	1, 65	wceq 1539	1 wff Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝑡)((𝑟‘𝑥)(Hom ‘𝑢)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ℎ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎‘𝑦)(⟨(𝑟‘𝑥), (𝑟‘𝑦)⟩(comp‘𝑢)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(⟨(𝑟‘𝑥), (𝑠‘𝑥)⟩(comp‘𝑢)(𝑠‘𝑦))(𝑎‘𝑥))}))

This definition is referenced by:  natfval  17578