Metamath Proof Explorer

Theorem estrccofval

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

		Ref	Expression
	Hypotheses	estrcbas.c	$⊢ C = ExtStrCat (U)$
		estrcbas.u	$⊢ φ \to U \in V$
		estrcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	Assertion	estrccofval	$⊢ φ \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))$

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	$⊢ C = ExtStrCat (U)$
2		estrcbas.u	$⊢ φ \to U \in V$
3		estrcco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
4		eqid	$⊢ Hom (C) = Hom (C)$
5	1 2 4	estrchomfval	$⊢ φ \to Hom (C) = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
6		eqidd	$⊢ φ \to (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f)) = (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))$
7	1 2 5 6	estrcval	$⊢ φ \to C = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))⟩\}$
8		catstr	$⊢ \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))⟩\} Struct ⟨1, 15⟩$
9		ccoid	$⊢ comp = Slot comp (ndx)$
10		snsstp3	$⊢ \{⟨comp (ndx), (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))⟩\} \subseteq \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), Hom (C)⟩, ⟨comp (ndx), (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))⟩\}$
11	2 2	xpexd	$⊢ φ \to U \times U \in V$
12		mpoexga	$⊢ (U \times U \in V \land U \in V) \to (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f)) \in V$
13	11 2 12	syl2anc	$⊢ φ \to (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f)) \in V$
14	7 8 9 10 13 3	strfv3	$⊢ φ \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))$