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

Definition df-fuc 17209
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 17207 . 2 class FuncCat
2 vt . . 3 setvar 𝑡
3 vu . . 3 setvar 𝑢
4 ccat 16930 . . 3 class Cat
5 cnx 16475 . . . . . 6 class ndx
6 cbs 16478 . . . . . 6 class Base
75, 6cfv 6328 . . . . 5 class (Base‘ndx)
82cv 1537 . . . . . 6 class 𝑡
93cv 1537 . . . . . 6 class 𝑢
10 cfunc 17119 . . . . . 6 class Func
118, 9, 10co 7139 . . . . 5 class (𝑡 Func 𝑢)
127, 11cop 4534 . . . 4 class ⟨(Base‘ndx), (𝑡 Func 𝑢)⟩
13 chom 16571 . . . . . 6 class Hom
145, 13cfv 6328 . . . . 5 class (Hom ‘ndx)
15 cnat 17206 . . . . . 6 class Nat
168, 9, 15co 7139 . . . . 5 class (𝑡 Nat 𝑢)
1714, 16cop 4534 . . . 4 class ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩
18 cco 16572 . . . . . 6 class comp
195, 18cfv 6328 . . . . 5 class (comp‘ndx)
20 vv . . . . . 6 setvar 𝑣
21 vh . . . . . 6 setvar
2211, 11cxp 5521 . . . . . 6 class ((𝑡 Func 𝑢) × (𝑡 Func 𝑢))
23 vf . . . . . . 7 setvar 𝑓
2420cv 1537 . . . . . . . 8 class 𝑣
25 c1st 7673 . . . . . . . 8 class 1st
2624, 25cfv 6328 . . . . . . 7 class (1st𝑣)
27 vg . . . . . . . 8 setvar 𝑔
28 c2nd 7674 . . . . . . . . 9 class 2nd
2924, 28cfv 6328 . . . . . . . 8 class (2nd𝑣)
30 vb . . . . . . . . 9 setvar 𝑏
31 va . . . . . . . . 9 setvar 𝑎
3227cv 1537 . . . . . . . . . 10 class 𝑔
3321cv 1537 . . . . . . . . . 10 class
3432, 33, 16co 7139 . . . . . . . . 9 class (𝑔(𝑡 Nat 𝑢))
3523cv 1537 . . . . . . . . . 10 class 𝑓
3635, 32, 16co 7139 . . . . . . . . 9 class (𝑓(𝑡 Nat 𝑢)𝑔)
37 vx . . . . . . . . . 10 setvar 𝑥
388, 6cfv 6328 . . . . . . . . . 10 class (Base‘𝑡)
3937cv 1537 . . . . . . . . . . . 12 class 𝑥
4030cv 1537 . . . . . . . . . . . 12 class 𝑏
4139, 40cfv 6328 . . . . . . . . . . 11 class (𝑏𝑥)
4231cv 1537 . . . . . . . . . . . 12 class 𝑎
4339, 42cfv 6328 . . . . . . . . . . 11 class (𝑎𝑥)
4435, 25cfv 6328 . . . . . . . . . . . . . 14 class (1st𝑓)
4539, 44cfv 6328 . . . . . . . . . . . . 13 class ((1st𝑓)‘𝑥)
4632, 25cfv 6328 . . . . . . . . . . . . . 14 class (1st𝑔)
4739, 46cfv 6328 . . . . . . . . . . . . 13 class ((1st𝑔)‘𝑥)
4845, 47cop 4534 . . . . . . . . . . . 12 class ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩
4933, 25cfv 6328 . . . . . . . . . . . . 13 class (1st)
5039, 49cfv 6328 . . . . . . . . . . . 12 class ((1st)‘𝑥)
519, 18cfv 6328 . . . . . . . . . . . 12 class (comp‘𝑢)
5248, 50, 51co 7139 . . . . . . . . . . 11 class (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))
5341, 43, 52co 7139 . . . . . . . . . 10 class ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))
5437, 38, 53cmpt 5113 . . . . . . . . 9 class (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))
5530, 31, 34, 36, 54cmpo 7141 . . . . . . . 8 class (𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5627, 29, 55csb 3831 . . . . . . 7 class (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5723, 26, 56csb 3831 . . . . . 6 class (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5820, 21, 22, 11, 57cmpo 7141 . . . . 5 class (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))
5919, 58cop 4534 . . . 4 class ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩
6012, 17, 59ctp 4532 . . 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, 60cmpo 7141 . 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 1538 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  17210  fucval  17223
  Copyright terms: Public domain W3C validator