Metamath Proof Explorer

Theorem catccofval

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)$
	Assertion	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))$

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	1 2 3	catcbas	$⊢ φ \to B = U \cap Cat$
6		eqid	$⊢ Hom (C) = Hom (C)$
7	1 2 3 6	catchomfval	$⊢ φ \to Hom (C) = (x \in B, y \in B ⟼ x Func y)$
8		eqidd	$⊢ φ \to (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) = (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))$
9	1 3 5 7 8	catcval	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\}$
10	9	fveq2d	$⊢ φ \to comp (C) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$
11	2	fvexi	$⊢ B \in V$
12	11 11	xpex	$⊢ B \times B \in V$
13	12 11	mpoex	$⊢ (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) \in V$
14		catstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\} Struct ⟨1, 15⟩$
15		ccoid	$⊢ comp = Slot comp (ndx)$
16		snsstp3	$⊢ \{⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\}$
17	14 15 16	strfv	$⊢ (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) \in V \to (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$
18	13 17	ax-mp	$⊢ (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f)) = comp (\{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (B \times B), z \in B ⟼ (g \in (2^{nd} (v) Func z), f \in Func (v) ⟼ g \circ_{func} f))⟩\})$
19	10 4 18	3eqtr4g	$⊢ φ \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))$