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 17202
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 17200 . 2 class FuncCat
2 vt . . 3 setvar 𝑡
3 vu . . 3 setvar 𝑢
4 ccat 16923 . . 3 class Cat
5 cnx 16468 . . . . . 6 class ndx
6 cbs 16471 . . . . . 6 class Base
75, 6cfv 6348 . . . . 5 class (Base‘ndx)
82cv 1527 . . . . . 6 class 𝑡
93cv 1527 . . . . . 6 class 𝑢
10 cfunc 17112 . . . . . 6 class Func
118, 9, 10co 7145 . . . . 5 class (𝑡 Func 𝑢)
127, 11cop 4563 . . . 4 class ⟨(Base‘ndx), (𝑡 Func 𝑢)⟩
13 chom 16564 . . . . . 6 class Hom
145, 13cfv 6348 . . . . 5 class (Hom ‘ndx)
15 cnat 17199 . . . . . 6 class Nat
168, 9, 15co 7145 . . . . 5 class (𝑡 Nat 𝑢)
1714, 16cop 4563 . . . 4 class ⟨(Hom ‘ndx), (𝑡 Nat 𝑢)⟩
18 cco 16565 . . . . . 6 class comp
195, 18cfv 6348 . . . . 5 class (comp‘ndx)
20 vv . . . . . 6 setvar 𝑣
21 vh . . . . . 6 setvar
2211, 11cxp 5546 . . . . . 6 class ((𝑡 Func 𝑢) × (𝑡 Func 𝑢))
23 vf . . . . . . 7 setvar 𝑓
2420cv 1527 . . . . . . . 8 class 𝑣
25 c1st 7676 . . . . . . . 8 class 1st
2624, 25cfv 6348 . . . . . . 7 class (1st𝑣)
27 vg . . . . . . . 8 setvar 𝑔
28 c2nd 7677 . . . . . . . . 9 class 2nd
2924, 28cfv 6348 . . . . . . . 8 class (2nd𝑣)
30 vb . . . . . . . . 9 setvar 𝑏
31 va . . . . . . . . 9 setvar 𝑎
3227cv 1527 . . . . . . . . . 10 class 𝑔
3321cv 1527 . . . . . . . . . 10 class
3432, 33, 16co 7145 . . . . . . . . 9 class (𝑔(𝑡 Nat 𝑢))
3523cv 1527 . . . . . . . . . 10 class 𝑓
3635, 32, 16co 7145 . . . . . . . . 9 class (𝑓(𝑡 Nat 𝑢)𝑔)
37 vx . . . . . . . . . 10 setvar 𝑥
388, 6cfv 6348 . . . . . . . . . 10 class (Base‘𝑡)
3937cv 1527 . . . . . . . . . . . 12 class 𝑥
4030cv 1527 . . . . . . . . . . . 12 class 𝑏
4139, 40cfv 6348 . . . . . . . . . . 11 class (𝑏𝑥)
4231cv 1527 . . . . . . . . . . . 12 class 𝑎
4339, 42cfv 6348 . . . . . . . . . . 11 class (𝑎𝑥)
4435, 25cfv 6348 . . . . . . . . . . . . . 14 class (1st𝑓)
4539, 44cfv 6348 . . . . . . . . . . . . 13 class ((1st𝑓)‘𝑥)
4632, 25cfv 6348 . . . . . . . . . . . . . 14 class (1st𝑔)
4739, 46cfv 6348 . . . . . . . . . . . . 13 class ((1st𝑔)‘𝑥)
4845, 47cop 4563 . . . . . . . . . . . 12 class ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩
4933, 25cfv 6348 . . . . . . . . . . . . 13 class (1st)
5039, 49cfv 6348 . . . . . . . . . . . 12 class ((1st)‘𝑥)
519, 18cfv 6348 . . . . . . . . . . . 12 class (comp‘𝑢)
5248, 50, 51co 7145 . . . . . . . . . . 11 class (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))
5341, 43, 52co 7145 . . . . . . . . . 10 class ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))
5437, 38, 53cmpt 5137 . . . . . . . . 9 class (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))
5530, 31, 34, 36, 54cmpo 7147 . . . . . . . 8 class (𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5627, 29, 55csb 3880 . . . . . . 7 class (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5723, 26, 56csb 3880 . . . . . 6 class (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥))))
5820, 21, 22, 11, 57cmpo 7147 . . . . 5 class (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))
5919, 58cop 4563 . . . 4 class ⟨(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ∈ (𝑡 Func 𝑢) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑢)((1st)‘𝑥))(𝑎𝑥)))))⟩
6012, 17, 59ctp 4561 . . 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 7147 . 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 1528 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  17203  fucval  17216
  Copyright terms: Public domain W3C validator