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

Definition df-evlf 16676
Description: Define the evaluation functor, which is the extension of the evaluation map 𝑓, 𝑥 ↦ (𝑓𝑥) of functors, to a functor (𝐶𝐷) × 𝐶𝐷. (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-evlf evalF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩)
Distinct variable group:   𝑎,𝑐,𝑑,𝑓,𝑔,𝑚,𝑛,𝑥,𝑦

Detailed syntax breakdown of Definition df-evlf
StepHypRef Expression
1 cevlf 16672 . 2 class evalF
2 vc . . 3 setvar 𝑐
3 vd . . 3 setvar 𝑑
4 ccat 16148 . . 3 class Cat
5 vf . . . . 5 setvar 𝑓
6 vx . . . . 5 setvar 𝑥
72cv 1474 . . . . . 6 class 𝑐
83cv 1474 . . . . . 6 class 𝑑
9 cfunc 16337 . . . . . 6 class Func
107, 8, 9co 6549 . . . . 5 class (𝑐 Func 𝑑)
11 cbs 15695 . . . . . 6 class Base
127, 11cfv 5804 . . . . 5 class (Base‘𝑐)
136cv 1474 . . . . . 6 class 𝑥
145cv 1474 . . . . . . 7 class 𝑓
15 c1st 7057 . . . . . . 7 class 1st
1614, 15cfv 5804 . . . . . 6 class (1st𝑓)
1713, 16cfv 5804 . . . . 5 class ((1st𝑓)‘𝑥)
185, 6, 10, 12, 17cmpt2 6551 . . . 4 class (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st𝑓)‘𝑥))
19 vy . . . . 5 setvar 𝑦
2010, 12cxp 5036 . . . . 5 class ((𝑐 Func 𝑑) × (Base‘𝑐))
21 vm . . . . . 6 setvar 𝑚
2213, 15cfv 5804 . . . . . 6 class (1st𝑥)
23 vn . . . . . . 7 setvar 𝑛
2419cv 1474 . . . . . . . 8 class 𝑦
2524, 15cfv 5804 . . . . . . 7 class (1st𝑦)
26 va . . . . . . . 8 setvar 𝑎
27 vg . . . . . . . 8 setvar 𝑔
2821cv 1474 . . . . . . . . 9 class 𝑚
2923cv 1474 . . . . . . . . 9 class 𝑛
30 cnat 16424 . . . . . . . . . 10 class Nat
317, 8, 30co 6549 . . . . . . . . 9 class (𝑐 Nat 𝑑)
3228, 29, 31co 6549 . . . . . . . 8 class (𝑚(𝑐 Nat 𝑑)𝑛)
33 c2nd 7058 . . . . . . . . . 10 class 2nd
3413, 33cfv 5804 . . . . . . . . 9 class (2nd𝑥)
3524, 33cfv 5804 . . . . . . . . 9 class (2nd𝑦)
36 chom 15779 . . . . . . . . . 10 class Hom
377, 36cfv 5804 . . . . . . . . 9 class (Hom ‘𝑐)
3834, 35, 37co 6549 . . . . . . . 8 class ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦))
3926cv 1474 . . . . . . . . . 10 class 𝑎
4035, 39cfv 5804 . . . . . . . . 9 class (𝑎‘(2nd𝑦))
4127cv 1474 . . . . . . . . . 10 class 𝑔
4228, 33cfv 5804 . . . . . . . . . . 11 class (2nd𝑚)
4334, 35, 42co 6549 . . . . . . . . . 10 class ((2nd𝑥)(2nd𝑚)(2nd𝑦))
4441, 43cfv 5804 . . . . . . . . 9 class (((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)
4528, 15cfv 5804 . . . . . . . . . . . 12 class (1st𝑚)
4634, 45cfv 5804 . . . . . . . . . . 11 class ((1st𝑚)‘(2nd𝑥))
4735, 45cfv 5804 . . . . . . . . . . 11 class ((1st𝑚)‘(2nd𝑦))
4846, 47cop 4131 . . . . . . . . . 10 class ⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩
4929, 15cfv 5804 . . . . . . . . . . 11 class (1st𝑛)
5035, 49cfv 5804 . . . . . . . . . 10 class ((1st𝑛)‘(2nd𝑦))
51 cco 15780 . . . . . . . . . . 11 class comp
528, 51cfv 5804 . . . . . . . . . 10 class (comp‘𝑑)
5348, 50, 52co 6549 . . . . . . . . 9 class (⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))
5440, 44, 53co 6549 . . . . . . . 8 class ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))
5526, 27, 32, 38, 54cmpt2 6551 . . . . . . 7 class (𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))
5623, 25, 55csb 3499 . . . . . 6 class (1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))
5721, 22, 56csb 3499 . . . . 5 class (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))
586, 19, 20, 20, 57cmpt2 6551 . . . 4 class (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))
5918, 58cop 4131 . . 3 class ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩
602, 3, 4, 4, 59cmpt2 6551 . 2 class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩)
611, 60wceq 1475 1 wff evalF = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝑑)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩)
Colors of variables: wff setvar class
This definition is referenced by:  evlfval  16680
  Copyright terms: Public domain W3C validator