Definition df-evlf 17721

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

Step	Hyp	Ref	Expression
1		cevlf 17717	. 2 class evalF
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		ccat 17167	. . 3 class Cat
5		vf	. . . . 5 setvar 𝑓
6		vx	. . . . 5 setvar 𝑥
7	2	cv 1542	. . . . . 6 class 𝑐
8	3	cv 1542	. . . . . 6 class 𝑑
9		cfunc 17360	. . . . . 6 class Func
10	7, 8, 9	co 7213	. . . . 5 class (𝑐 Func 𝑑)
11		cbs 16760	. . . . . 6 class Base
12	7, 11	cfv 6380	. . . . 5 class (Base‘𝑐)
13	6	cv 1542	. . . . . 6 class 𝑥
14	5	cv 1542	. . . . . . 7 class 𝑓
15		c1st 7759	. . . . . . 7 class 1st
16	14, 15	cfv 6380	. . . . . 6 class (1st ‘𝑓)
17	13, 16	cfv 6380	. . . . 5 class ((1st ‘𝑓)‘𝑥)
18	5, 6, 10, 12, 17	cmpo 7215	. . . 4 class (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1st ‘𝑓)‘𝑥))
19		vy	. . . . 5 setvar 𝑦
20	10, 12	cxp 5549	. . . . 5 class ((𝑐 Func 𝑑) × (Base‘𝑐))
21		vm	. . . . . 6 setvar 𝑚
22	13, 15	cfv 6380	. . . . . 6 class (1st ‘𝑥)
23		vn	. . . . . . 7 setvar 𝑛
24	19	cv 1542	. . . . . . . 8 class 𝑦
25	24, 15	cfv 6380	. . . . . . 7 class (1st ‘𝑦)
26		va	. . . . . . . 8 setvar 𝑎
27		vg	. . . . . . . 8 setvar 𝑔
28	21	cv 1542	. . . . . . . . 9 class 𝑚
29	23	cv 1542	. . . . . . . . 9 class 𝑛
30		cnat 17448	. . . . . . . . . 10 class Nat
31	7, 8, 30	co 7213	. . . . . . . . 9 class (𝑐 Nat 𝑑)
32	28, 29, 31	co 7213	. . . . . . . 8 class (𝑚(𝑐 Nat 𝑑)𝑛)
33		c2nd 7760	. . . . . . . . . 10 class 2nd
34	13, 33	cfv 6380	. . . . . . . . 9 class (2nd ‘𝑥)
35	24, 33	cfv 6380	. . . . . . . . 9 class (2nd ‘𝑦)
36		chom 16813	. . . . . . . . . 10 class Hom
37	7, 36	cfv 6380	. . . . . . . . 9 class (Hom ‘𝑐)
38	34, 35, 37	co 7213	. . . . . . . 8 class ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦))
39	26	cv 1542	. . . . . . . . . 10 class 𝑎
40	35, 39	cfv 6380	. . . . . . . . 9 class (𝑎‘(2nd ‘𝑦))
41	27	cv 1542	. . . . . . . . . 10 class 𝑔
42	28, 33	cfv 6380	. . . . . . . . . . 11 class (2nd ‘𝑚)
43	34, 35, 42	co 7213	. . . . . . . . . 10 class ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))
44	41, 43	cfv 6380	. . . . . . . . 9 class (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)
45	28, 15	cfv 6380	. . . . . . . . . . . 12 class (1st ‘𝑚)
46	34, 45	cfv 6380	. . . . . . . . . . 11 class ((1st ‘𝑚)‘(2nd ‘𝑥))
47	35, 45	cfv 6380	. . . . . . . . . . 11 class ((1st ‘𝑚)‘(2nd ‘𝑦))
48	46, 47	cop 4547	. . . . . . . . . 10 class ⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩
49	29, 15	cfv 6380	. . . . . . . . . . 11 class (1st ‘𝑛)
50	35, 49	cfv 6380	. . . . . . . . . 10 class ((1st ‘𝑛)‘(2nd ‘𝑦))
51		cco 16814	. . . . . . . . . . 11 class comp
52	8, 51	cfv 6380	. . . . . . . . . 10 class (comp‘𝑑)
53	48, 50, 52	co 7213	. . . . . . . . 9 class (⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))
54	40, 44, 53	co 7213	. . . . . . . 8 class ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))
55	26, 27, 32, 38, 54	cmpo 7215	. . . . . . 7 class (𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))
56	23, 25, 55	csb 3811	. . . . . 6 class ⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))
57	21, 22, 56	csb 3811	. . . . 5 class ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))
58	6, 19, 20, 20, 57	cmpo 7215	. . . 4 class (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝑑)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))
59	18, 58	cop 4547	. . 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 ‘𝑦))‘𝑔))))⟩
60	2, 3, 4, 4, 59	cmpo 7215	. 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 ‘𝑦))‘𝑔))))⟩)
61	1, 60	wceq 1543	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 ‘𝑦))‘𝑔))))⟩)

This definition is referenced by:  evlfval  17725