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 17836
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 17834 . 2 class FuncCat
2 vt . . 3 setvar 𝑑
3 vu . . 3 setvar 𝑒
4 ccat 17549 . . 3 class Cat
5 cnx 17070 . . . . . 6 class ndx
6 cbs 17088 . . . . . 6 class Base
75, 6cfv 6497 . . . . 5 class (Baseβ€˜ndx)
82cv 1541 . . . . . 6 class 𝑑
93cv 1541 . . . . . 6 class 𝑒
10 cfunc 17745 . . . . . 6 class Func
118, 9, 10co 7358 . . . . 5 class (𝑑 Func 𝑒)
127, 11cop 4593 . . . 4 class ⟨(Baseβ€˜ndx), (𝑑 Func 𝑒)⟩
13 chom 17149 . . . . . 6 class Hom
145, 13cfv 6497 . . . . 5 class (Hom β€˜ndx)
15 cnat 17833 . . . . . 6 class Nat
168, 9, 15co 7358 . . . . 5 class (𝑑 Nat 𝑒)
1714, 16cop 4593 . . . 4 class ⟨(Hom β€˜ndx), (𝑑 Nat 𝑒)⟩
18 cco 17150 . . . . . 6 class comp
195, 18cfv 6497 . . . . 5 class (compβ€˜ndx)
20 vv . . . . . 6 setvar 𝑣
21 vh . . . . . 6 setvar β„Ž
2211, 11cxp 5632 . . . . . 6 class ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒))
23 vf . . . . . . 7 setvar 𝑓
2420cv 1541 . . . . . . . 8 class 𝑣
25 c1st 7920 . . . . . . . 8 class 1st
2624, 25cfv 6497 . . . . . . 7 class (1st β€˜π‘£)
27 vg . . . . . . . 8 setvar 𝑔
28 c2nd 7921 . . . . . . . . 9 class 2nd
2924, 28cfv 6497 . . . . . . . 8 class (2nd β€˜π‘£)
30 vb . . . . . . . . 9 setvar 𝑏
31 va . . . . . . . . 9 setvar π‘Ž
3227cv 1541 . . . . . . . . . 10 class 𝑔
3321cv 1541 . . . . . . . . . 10 class β„Ž
3432, 33, 16co 7358 . . . . . . . . 9 class (𝑔(𝑑 Nat 𝑒)β„Ž)
3523cv 1541 . . . . . . . . . 10 class 𝑓
3635, 32, 16co 7358 . . . . . . . . 9 class (𝑓(𝑑 Nat 𝑒)𝑔)
37 vx . . . . . . . . . 10 setvar π‘₯
388, 6cfv 6497 . . . . . . . . . 10 class (Baseβ€˜π‘‘)
3937cv 1541 . . . . . . . . . . . 12 class π‘₯
4030cv 1541 . . . . . . . . . . . 12 class 𝑏
4139, 40cfv 6497 . . . . . . . . . . 11 class (π‘β€˜π‘₯)
4231cv 1541 . . . . . . . . . . . 12 class π‘Ž
4339, 42cfv 6497 . . . . . . . . . . 11 class (π‘Žβ€˜π‘₯)
4435, 25cfv 6497 . . . . . . . . . . . . . 14 class (1st β€˜π‘“)
4539, 44cfv 6497 . . . . . . . . . . . . 13 class ((1st β€˜π‘“)β€˜π‘₯)
4632, 25cfv 6497 . . . . . . . . . . . . . 14 class (1st β€˜π‘”)
4739, 46cfv 6497 . . . . . . . . . . . . 13 class ((1st β€˜π‘”)β€˜π‘₯)
4845, 47cop 4593 . . . . . . . . . . . 12 class ⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩
4933, 25cfv 6497 . . . . . . . . . . . . 13 class (1st β€˜β„Ž)
5039, 49cfv 6497 . . . . . . . . . . . 12 class ((1st β€˜β„Ž)β€˜π‘₯)
519, 18cfv 6497 . . . . . . . . . . . 12 class (compβ€˜π‘’)
5248, 50, 51co 7358 . . . . . . . . . . 11 class (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))
5341, 43, 52co 7358 . . . . . . . . . 10 class ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))
5437, 38, 53cmpt 5189 . . . . . . . . 9 class (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))
5530, 31, 34, 36, 54cmpo 7360 . . . . . . . 8 class (𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))
5627, 29, 55csb 3856 . . . . . . 7 class ⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))
5723, 26, 56csb 3856 . . . . . 6 class ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))
5820, 21, 22, 11, 57cmpo 7360 . . . . 5 class (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))
5919, 58cop 4593 . . . 4 class ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩
6012, 17, 59ctp 4591 . . 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 7360 . 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 1542 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  17837  fucval  17851
  Copyright terms: Public domain W3C validator