cofu2nd

Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval.b	$⊢ B = {Base}_{C}$
	cofuval.f	$⊢ φ \to F \in (C Func D)$
	cofuval.g	$⊢ φ \to G \in (D Func E)$
	cofu2nd.x	$⊢ φ \to X \in B$
	cofu2nd.y	$⊢ φ \to Y \in B$
Assertion	cofu2nd	$⊢ φ \to X 2^{nd} (G \circ_{func} F) Y = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)$

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	$⊢ B = {Base}_{C}$
2		cofuval.f	$⊢ φ \to F \in (C Func D)$
3		cofuval.g	$⊢ φ \to G \in (D Func E)$
4		cofu2nd.x	$⊢ φ \to X \in B$
5		cofu2nd.y	$⊢ φ \to Y \in B$
6	1 2 3	cofuval	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩$
7	6	fveq2d	$⊢ φ \to 2^{nd} (G \circ_{func} F) = 2^{nd} (⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩)$
8		fvex	$⊢ 1^{st} (G) \in V$
9		fvex	$⊢ 1^{st} (F) \in V$
10	8 9	coex	$⊢ 1^{st} (G) \circ 1^{st} (F) \in V$
11	1	fvexi	$⊢ B \in V$
12	11 11	mpoex	$⊢ (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) \in V$
13	10 12	op2nd	$⊢ 2^{nd} (⟨1^{st} (G) \circ 1^{st} (F), (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩) = (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))$
14	7 13	eqtrdi	$⊢ φ \to 2^{nd} (G \circ_{func} F) = (x \in B, y \in B ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))$
15		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
16	15	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to 1^{st} (F) (x) = 1^{st} (F) (X)$
17		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
18	17	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to 1^{st} (F) (y) = 1^{st} (F) (Y)$
19	16 18	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to 1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y) = 1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)$
20	15 17	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x 2^{nd} (F) y = X 2^{nd} (F) Y$
21	19 20	coeq12d	$⊢ (φ \land (x = X \land y = Y)) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y) = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)$
22		ovex	$⊢ 1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y) \in V$
23		ovex	$⊢ X 2^{nd} (F) Y \in V$
24	22 23	coex	$⊢ (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y) \in V$
25	24	a1i	$⊢ φ \to (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y) \in V$
26	14 21 4 5 25	ovmpod	$⊢ φ \to X 2^{nd} (G \circ_{func} F) Y = (1^{st} (F) (X) 2^{nd} (G) 1^{st} (F) (Y)) \circ (X 2^{nd} (F) Y)$

Metamath Proof Explorer

Theorem cofu2nd

Proof