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

Definition df-nat 16372
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
StepHypRef Expression
1 cnat 16370 . 2 class Nat
2 vt . . 3 setvar 𝑡
3 vu . . 3 setvar 𝑢
4 ccat 16094 . . 3 class Cat
5 vf . . . 4 setvar 𝑓
6 vg . . . 4 setvar 𝑔
72cv 1473 . . . . 5 class 𝑡
83cv 1473 . . . . 5 class 𝑢
9 cfunc 16283 . . . . 5 class Func
107, 8, 9co 6527 . . . 4 class (𝑡 Func 𝑢)
11 vr . . . . 5 setvar 𝑟
125cv 1473 . . . . . 6 class 𝑓
13 c1st 7034 . . . . . 6 class 1st
1412, 13cfv 5790 . . . . 5 class (1st𝑓)
15 vs . . . . . 6 setvar 𝑠
166cv 1473 . . . . . . 7 class 𝑔
1716, 13cfv 5790 . . . . . 6 class (1st𝑔)
18 vy . . . . . . . . . . . . . 14 setvar 𝑦
1918cv 1473 . . . . . . . . . . . . 13 class 𝑦
20 va . . . . . . . . . . . . . 14 setvar 𝑎
2120cv 1473 . . . . . . . . . . . . 13 class 𝑎
2219, 21cfv 5790 . . . . . . . . . . . 12 class (𝑎𝑦)
23 vh . . . . . . . . . . . . . 14 setvar
2423cv 1473 . . . . . . . . . . . . 13 class
25 vx . . . . . . . . . . . . . . 15 setvar 𝑥
2625cv 1473 . . . . . . . . . . . . . 14 class 𝑥
27 c2nd 7035 . . . . . . . . . . . . . . 15 class 2nd
2812, 27cfv 5790 . . . . . . . . . . . . . 14 class (2nd𝑓)
2926, 19, 28co 6527 . . . . . . . . . . . . 13 class (𝑥(2nd𝑓)𝑦)
3024, 29cfv 5790 . . . . . . . . . . . 12 class ((𝑥(2nd𝑓)𝑦)‘)
3111cv 1473 . . . . . . . . . . . . . . 15 class 𝑟
3226, 31cfv 5790 . . . . . . . . . . . . . 14 class (𝑟𝑥)
3319, 31cfv 5790 . . . . . . . . . . . . . 14 class (𝑟𝑦)
3432, 33cop 4130 . . . . . . . . . . . . 13 class ⟨(𝑟𝑥), (𝑟𝑦)⟩
3515cv 1473 . . . . . . . . . . . . . 14 class 𝑠
3619, 35cfv 5790 . . . . . . . . . . . . 13 class (𝑠𝑦)
37 cco 15726 . . . . . . . . . . . . . 14 class comp
388, 37cfv 5790 . . . . . . . . . . . . 13 class (comp‘𝑢)
3934, 36, 38co 6527 . . . . . . . . . . . 12 class (⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))
4022, 30, 39co 6527 . . . . . . . . . . 11 class ((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘))
4116, 27cfv 5790 . . . . . . . . . . . . . 14 class (2nd𝑔)
4226, 19, 41co 6527 . . . . . . . . . . . . 13 class (𝑥(2nd𝑔)𝑦)
4324, 42cfv 5790 . . . . . . . . . . . 12 class ((𝑥(2nd𝑔)𝑦)‘)
4426, 21cfv 5790 . . . . . . . . . . . 12 class (𝑎𝑥)
4526, 35cfv 5790 . . . . . . . . . . . . . 14 class (𝑠𝑥)
4632, 45cop 4130 . . . . . . . . . . . . 13 class ⟨(𝑟𝑥), (𝑠𝑥)⟩
4746, 36, 38co 6527 . . . . . . . . . . . 12 class (⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))
4843, 44, 47co 6527 . . . . . . . . . . 11 class (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))
4940, 48wceq 1474 . . . . . . . . . 10 wff ((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))
50 chom 15725 . . . . . . . . . . . 12 class Hom
517, 50cfv 5790 . . . . . . . . . . 11 class (Hom ‘𝑡)
5226, 19, 51co 6527 . . . . . . . . . 10 class (𝑥(Hom ‘𝑡)𝑦)
5349, 23, 52wral 2895 . . . . . . . . 9 wff ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))
54 cbs 15641 . . . . . . . . . 10 class Base
557, 54cfv 5790 . . . . . . . . 9 class (Base‘𝑡)
5653, 18, 55wral 2895 . . . . . . . 8 wff 𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))
5756, 25, 55wral 2895 . . . . . . 7 wff 𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))
588, 50cfv 5790 . . . . . . . . 9 class (Hom ‘𝑢)
5932, 45, 58co 6527 . . . . . . . 8 class ((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥))
6025, 55, 59cixp 7771 . . . . . . 7 class X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥))
6157, 20, 60crab 2899 . . . . . 6 class {𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}
6215, 17, 61csb 3498 . . . . 5 class (1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}
6311, 14, 62csb 3498 . . . 4 class (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}
645, 6, 10, 10, 63cmpt2 6529 . . 3 class (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))})
652, 3, 4, 4, 64cmpt2 6529 . 2 class (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}))
661, 65wceq 1474 1 wff Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}))
Colors of variables: wff setvar class
This definition is referenced by:  natfval  16375
  Copyright terms: Public domain W3C validator