df-cofu

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

		Ref	Expression
	Assertion	df-cofu	$⊢ \circ_{func} = (g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$

Step	Hyp	Ref	Expression
0		ccofu	$class \circ_{func}$
1		vg	$setvar g$
2		cvv	$class V$
3		vf	$setvar f$
4		c1st	$class 1^{st}$
5	1	cv	$setvar g$
6	5 4	cfv	$class 1^{st} (g)$
7	3	cv	$setvar f$
8	7 4	cfv	$class 1^{st} (f)$
9	6 8	ccom	$class (1^{st} (g) \circ 1^{st} (f))$
10		vx	$setvar x$
11		c2nd	$class 2^{nd}$
12	7 11	cfv	$class 2^{nd} (f)$
13	12	cdm	$class dom 2^{nd} (f)$
14	13	cdm	$class dom dom 2^{nd} (f)$
15		vy	$setvar y$
16	10	cv	$setvar x$
17	16 8	cfv	$class 1^{st} (f) (x)$
18	5 11	cfv	$class 2^{nd} (g)$
19	15	cv	$setvar y$
20	19 8	cfv	$class 1^{st} (f) (y)$
21	17 20 18	co	$class (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y))$
22	16 19 12	co	$class (x 2^{nd} (f) y)$
23	21 22	ccom	$class ((1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))$
24	10 15 14 14 23	cmpo	$class (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))$
25	9 24	cop	$class ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩$
26	1 3 2 2 25	cmpo	$class (g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$
27	0 26	wceq	$wff \circ_{func} = (g \in V, f \in V ⟼ ⟨1^{st} (g) \circ 1^{st} (f), (x \in dom dom 2^{nd} (f), y \in dom dom 2^{nd} (f) ⟼ (1^{st} (f) (x) 2^{nd} (g) 1^{st} (f) (y)) \circ (x 2^{nd} (f) y))⟩)$

Metamath Proof Explorer