Definition df-cofu 17905

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 17901	. 2 class ∘func
2		vg	. . 3 setvar 𝑔
3		vf	. . 3 setvar 𝑓
4		cvv 3480	. . 3 class V
5	2	cv 1539	. . . . . 6 class 𝑔
6		c1st 8012	. . . . . 6 class 1st
7	5, 6	cfv 6561	. . . . 5 class (1st ‘𝑔)
8	3	cv 1539	. . . . . 6 class 𝑓
9	8, 6	cfv 6561	. . . . 5 class (1st ‘𝑓)
10	7, 9	ccom 5689	. . . 4 class ((1st ‘𝑔) ∘ (1st ‘𝑓))
11		vx	. . . . 5 setvar 𝑥
12		vy	. . . . 5 setvar 𝑦
13		c2nd 8013	. . . . . . . 8 class 2nd
14	8, 13	cfv 6561	. . . . . . 7 class (2nd ‘𝑓)
15	14	cdm 5685	. . . . . 6 class dom (2nd ‘𝑓)
16	15	cdm 5685	. . . . 5 class dom dom (2nd ‘𝑓)
17	11	cv 1539	. . . . . . . 8 class 𝑥
18	17, 9	cfv 6561	. . . . . . 7 class ((1st ‘𝑓)‘𝑥)
19	12	cv 1539	. . . . . . . 8 class 𝑦
20	19, 9	cfv 6561	. . . . . . 7 class ((1st ‘𝑓)‘𝑦)
21	5, 13	cfv 6561	. . . . . . 7 class (2nd ‘𝑔)
22	18, 20, 21	co 7431	. . . . . 6 class (((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦))
23	17, 19, 14	co 7431	. . . . . 6 class (𝑥(2nd ‘𝑓)𝑦)
24	22, 23	ccom 5689	. . . . 5 class ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦))
25	11, 12, 16, 16, 24	cmpo 7433	. . . 4 class (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))
26	10, 25	cop 4632	. . 3 class ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩
27	2, 3, 4, 4, 26	cmpo 7433	. 2 class (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩)
28	1, 27	wceq 1540	1 wff ∘func = (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1st ‘𝑔) ∘ (1st ‘𝑓)), (𝑥 ∈ dom dom (2nd ‘𝑓), 𝑦 ∈ dom dom (2nd ‘𝑓) ↦ ((((1st ‘𝑓)‘𝑥)(2nd ‘𝑔)((1st ‘𝑓)‘𝑦)) ∘ (𝑥(2nd ‘𝑓)𝑦)))⟩)

This definition is referenced by:  cofuval  17927  rescofuf  48922  fucoelvv  49015