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

Definition df-fuc 16427
 Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in [Adamek] p. 87. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
df-fuc FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩})
Distinct variable group:   𝑎,𝑏,𝑓,𝑔,,𝑡,𝑢,𝑣,𝑥

Detailed syntax breakdown of Definition df-fuc
StepHypRef Expression
1 cfuc 16425 . 2 class FuncCat
2 vt . . 3 setvar 𝑡
3 vu . . 3 setvar 𝑢
4 ccat 16148 . . 3 class Cat
5 cnx 15692 . . . . . 6 class ndx
6 cbs 15695 . . . . . 6 class Base
75, 6cfv 5804 . . . . 5 class (Base‘ndx)
82cv 1474 . . . . . 6 class 𝑡
93cv 1474 . . . . . 6 class 𝑢
10 cfunc 16337 . . . . . 6 class Func
118, 9, 10co 6549 . . . . 5 class (𝑡 Func 𝑢)
127, 11cop 4131 . . . 4 class ⟨(Base‘ndx), (𝑡 Func 𝑢)⟩
13 chom 15779 . . . . . 6 class Hom
145, 13cfv 5804 . . . . 5 class (Hom ‘ndx)
15 cnat 16424 . . . . . 6 class Nat
168, 9, 15co 6549 . . . . 5 class (𝑡 Nat 𝑢)
1714, 16cop 4131 . . . 4 class ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩
18 cco 15780 . . . . . 6 class comp
195, 18cfv 5804 . . . . 5 class (comp‘ndx)
20 vv . . . . . 6 setvar 𝑣
21 vh . . . . . 6 setvar
2211, 11cxp 5036 . . . . . 6 class ((𝑡 Func 𝑢) × (𝑡 Func 𝑢))
23 vf . . . . . . 7 setvar 𝑓
2420cv 1474 . . . . . . . 8 class 𝑣
25 c1st 7057 . . . . . . . 8 class 1st
2624, 25cfv 5804 . . . . . . 7 class (1st𝑣)
27 vg . . . . . . . 8 setvar 𝑔
28 c2nd 7058 . . . . . . . . 9 class 2nd
2924, 28cfv 5804 . . . . . . . 8 class (2nd𝑣)
30 vb . . . . . . . . 9 setvar 𝑏
31 va . . . . . . . . 9 setvar 𝑎
3227cv 1474 . . . . . . . . . 10 class 𝑔
3321cv 1474 . . . . . . . . . 10 class
3432, 33, 16co 6549 . . . . . . . . 9 class (𝑔(𝑡 Nat 𝑢))
3523cv 1474 . . . . . . . . . 10 class 𝑓
3635, 32, 16co 6549 . . . . . . . . 9 class (𝑓(𝑡 Nat 𝑢)𝑔)
37 vx . . . . . . . . . 10 setvar 𝑥
388, 6cfv 5804 . . . . . . . . . 10 class (Base‘𝑡)
3937cv 1474 . . . . . . . . . . . 12 class 𝑥
4030cv 1474 . . . . . . . . . . . 12 class 𝑏
4139, 40cfv 5804 . . . . . . . . . . 11 class (𝑏𝑥)
4231cv 1474 . . . . . . . . . . . 12 class 𝑎
4339, 42cfv 5804 . . . . . . . . . . 11 class (𝑎𝑥)
4435, 25cfv 5804 . . . . . . . . . . . . . 14 class (1st𝑓)
4539, 44cfv 5804 . . . . . . . . . . . . 13 class ((1st𝑓)‘𝑥)
4632, 25cfv 5804 . . . . . . . . . . . . . 14 class (1st𝑔)
4739, 46cfv 5804 . . . . . . . . . . . . 13 class ((1st𝑔)‘𝑥)
4845, 47cop 4131 . . . . . . . . . . . 12 class ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩
4933, 25cfv 5804 . . . . . . . . . . . . 13 class (1st)
5039, 49cfv 5804 . . . . . . . . . . . 12 class ((1st)‘𝑥)
519, 18cfv 5804 . . . . . . . . . . . 12 class (comp‘𝑢)
5248, 50, 51co 6549 . . . . . . . . . . 11 class (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))
5341, 43, 52co 6549 . . . . . . . . . 10 class ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))
5437, 38, 53cmpt 4643 . . . . . . . . 9 class (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))
5530, 31, 34, 36, 54cmpt2 6551 . . . . . . . 8 class (𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5627, 29, 55csb 3499 . . . . . . 7 class (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5723, 26, 56csb 3499 . . . . . 6 class (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5820, 21, 22, 11, 57cmpt2 6551 . . . . 5 class (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))
5919, 58cop 4131 . . . 4 class ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩
6012, 17, 59ctp 4129 . . 3 class {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩}
612, 3, 4, 4, 60cmpt2 6551 . 2 class (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩})
621, 61wceq 1475 1 wff FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨(Base‘ndx), (𝑡 Func 𝑢)⟩, ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩})
 Colors of variables: wff setvar class This definition is referenced by:  fnfuc  16428  fucval  16441
 Copyright terms: Public domain W3C validator