Definition df-comf 17714

Description: Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
df-comf	⊢ compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))

Distinct variable group:   𝑓,𝑐,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-comf

Step	Hyp	Ref	Expression
1		ccomf 17710	. 2 class compf
2		vc	. . 3 setvar 𝑐
3		cvv 3480	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1539	. . . . . 6 class 𝑐
7		cbs 17247	. . . . . 6 class Base
8	6, 7	cfv 6561	. . . . 5 class (Base‘𝑐)
9	8, 8	cxp 5683	. . . 4 class ((Base‘𝑐) × (Base‘𝑐))
10		vg	. . . . 5 setvar 𝑔
11		vf	. . . . 5 setvar 𝑓
12	4	cv 1539	. . . . . . 7 class 𝑥
13		c2nd 8013	. . . . . . 7 class 2nd
14	12, 13	cfv 6561	. . . . . 6 class (2nd ‘𝑥)
15	5	cv 1539	. . . . . 6 class 𝑦
16		chom 17308	. . . . . . 7 class Hom
17	6, 16	cfv 6561	. . . . . 6 class (Hom ‘𝑐)
18	14, 15, 17	co 7431	. . . . 5 class ((2nd ‘𝑥)(Hom ‘𝑐)𝑦)
19	12, 17	cfv 6561	. . . . 5 class ((Hom ‘𝑐)‘𝑥)
20	10	cv 1539	. . . . . 6 class 𝑔
21	11	cv 1539	. . . . . 6 class 𝑓
22		cco 17309	. . . . . . . 8 class comp
23	6, 22	cfv 6561	. . . . . . 7 class (comp‘𝑐)
24	12, 15, 23	co 7431	. . . . . 6 class (𝑥(comp‘𝑐)𝑦)
25	20, 21, 24	co 7431	. . . . 5 class (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)
26	10, 11, 18, 19, 25	cmpo 7433	. . . 4 class (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))
27	4, 5, 9, 8, 26	cmpo 7433	. . 3 class (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓)))
28	2, 3, 27	cmpt 5225	. 2 class (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))
29	1, 28	wceq 1540	1 wff compf = (𝑐 ∈ V ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)𝑦), 𝑓 ∈ ((Hom ‘𝑐)‘𝑥) ↦ (𝑔(𝑥(comp‘𝑐)𝑦)𝑓))))

This definition is referenced by:  comfffval  17741