catcco

Description: Composition in the category of categories. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	catcbas.c	$⊢ C = CatCat (U)$
	catcbas.b	$⊢ B = {Base}_{C}$
	catcbas.u	$⊢ φ \to U \in V$
	catcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	catcco.x	$⊢ φ \to X \in B$
	catcco.y	$⊢ φ \to Y \in B$
	catcco.z	$⊢ φ \to Z \in B$
	catcco.f	$⊢ φ \to F \in (X Func Y)$
	catcco.g	$⊢ φ \to G \in (Y Func Z)$
Assertion	catcco	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ_{func} F$

Proof

Step	Hyp	Ref	Expression
1		catcbas.c	$⊢ C = CatCat (U)$
2		catcbas.b	$⊢ B = {Base}_{C}$
3		catcbas.u	$⊢ φ \to U \in V$
4		catcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
5		catcco.x	$⊢ φ \to X \in B$
6		catcco.y	$⊢ φ \to Y \in B$
7		catcco.z	$⊢ φ \to Z \in B$
8		catcco.f	$⊢ φ \to F \in (X Func Y)$
9		catcco.g	$⊢ φ \to G \in (Y Func Z)$
10	1 2 3 4	catccofval	$⊢ φ \to \underset{˙}{\cdot} = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
11		simprl	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to v = ⟨X, Y⟩$
12	11	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = 2^{nd} (⟨X, Y⟩)$
13		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
14	5 6 13	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
15	14	adantr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
16	12 15	eqtrd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) = Y$
17		simprr	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to z = Z$
18	16 17	oveq12d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to 2^{nd} (v) Func z = Y Func Z$
19	11	fveq2d	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to Func (v) = Func (⟨X, Y⟩)$
20		df-ov	$⊢ X Func Y = Func (⟨X, Y⟩)$
21	19 20	eqtr4di	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to Func (v) = X Func Y$
22		eqidd	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to g \circ_{func} f = g \circ_{func} f$
23	18 21 22	mpoeq123dv	$⊢ (φ \land (v = ⟨X, Y⟩ \land z = Z)) \to (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f) = (g \in (Y Func Z), f \in (X Func Y) ⟼ g \circ_{func} f)$
24	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
25		ovex	$⊢ Y Func Z \in V$
26		ovex	$⊢ X Func Y \in V$
27	25 26	mpoex	$⊢ (g \in (Y Func Z), f \in (X Func Y) ⟼ g \circ_{func} f) \in V$
28	27	a1i	$⊢ φ \to (g \in (Y Func Z), f \in (X Func Y) ⟼ g \circ_{func} f) \in V$
29	10 23 24 7 28	ovmpod	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} Z = (g \in (Y Func Z), f \in (X Func Y) ⟼ g \circ_{func} f)$
30		oveq12	$⊢ (g = G \land f = F) \to g \circ_{func} f = G \circ_{func} F$
31	30	adantl	$⊢ (φ \land (g = G \land f = F)) \to g \circ_{func} f = G \circ_{func} F$
32		ovexd	$⊢ φ \to G \circ_{func} F \in V$
33	29 31 9 8 32	ovmpod	$⊢ φ \to G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F = G \circ_{func} F$

Metamath Proof Explorer

Theorem catcco

Proof