Definition df-cofu 17122

Description: Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017.)

Assertion

Ref	Expression
df-cofu	⊢ ∘func = (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩)

Distinct variable group:   𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-cofu

Step	Hyp	Ref	Expression
1		ccofu 17118	. 2 class ∘func
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3493	. . 3 class V
5	2	cv 1530	. . . . . 6 class 𝑔
6		c1st 7679	. . . . . 6 class 1st
7	5, 6	cfv 6348	. . . . 5 class (1st ‘𝑔)
8	3	cv 1530	. . . . . 6 class 𝑓
9	8, 6	cfv 6348	. . . . 5 class (1st ‘𝑓)
10	7, 9	ccom 5552	. . . 4 class ((1st ‘𝑔) ∘ (1st ‘𝑓))
11		vx	. . . . 5 setvar 𝑥
12		vy	. . . . 5 setvar 𝑦
13		c2nd 7680	. . . . . . . 8 class 2nd
14	8, 13	cfv 6348	. . . . . . 7 class (2nd ‘𝑓)
15	14	cdm 5548	. . . . . 6 class dom (2nd ‘𝑓)
16	15	cdm 5548	. . . . 5 class dom dom (2nd ‘𝑓)
17	11	cv 1530	. . . . . . . 8 class 𝑥
18	17, 9	cfv 6348	. . . . . . 7 class ((1st ‘𝑓)‘𝑥)
19	12	cv 1530	. . . . . . . 8 class 𝑦
20	19, 9	cfv 6348	. . . . . . 7 class ((1st ‘𝑓)‘𝑦)
21	5, 13	cfv 6348	. . . . . . 7 class (2nd ‘𝑔)
22	18, 20, 21	co 7148	. . . . . 6 class (((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦))
23	17, 19, 14	co 7148	. . . . . 6 class (𝑥(2nd ‘𝑓)𝑦)
24	22, 23	ccom 5552	. . . . 5 class ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦))
25	11, 12, 16, 16, 24	cmpo 7150	. . . 4 class (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))
26	10, 25	cop 4565	. . 3 class ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩
27	2, 3, 4, 4, 26	cmpo 7150	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩)
28	1, 27	wceq 1531	1 wff ∘func = (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩)

This definition is referenced by:  cofuval  17144