estrcval

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

	Ref	Expression
Hypotheses	estrcval.c	$⊢ C = ExtStrCat (U)$
	estrcval.u	$⊢ φ \to U \in V$
	estrcval.h	$⊢ φ \to H = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
	estrcval.o	$⊢ φ \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))$
Assertion	estrcval	$⊢ φ \to C = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		estrcval.c	$⊢ C = ExtStrCat (U)$
2		estrcval.u	$⊢ φ \to U \in V$
3		estrcval.h	$⊢ φ \to H = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
4		estrcval.o	$⊢ φ \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))$
5		df-estrc	$⊢ ExtStrCat = (u \in V ⟼ \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ {Base}_{y}^{{Base}_{x}})⟩, ⟨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))⟩\})$
6		simpr	$⊢ (φ \land u = U) \to u = U$
7	6	opeq2d	$⊢ (φ \land u = U) \to ⟨{Base}_{ndx}, u⟩ = ⟨{Base}_{ndx}, U⟩$
8		eqidd	$⊢ (φ \land u = U) \to {Base}_{y}^{{Base}_{x}} = {Base}_{y}^{{Base}_{x}}$
9	6 6 8	mpoeq123dv	$⊢ (φ \land u = U) \to (x \in u, y \in u ⟼ {Base}_{y}^{{Base}_{x}}) = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
10	3	adantr	$⊢ (φ \land u = U) \to H = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
11	9 10	eqtr4d	$⊢ (φ \land u = U) \to (x \in u, y \in u ⟼ {Base}_{y}^{{Base}_{x}}) = H$
12	11	opeq2d	$⊢ (φ \land u = U) \to ⟨Hom (ndx), (x \in u, y \in u ⟼ {Base}_{y}^{{Base}_{x}})⟩ = ⟨Hom (ndx), H⟩$
13	6	sqxpeqd	$⊢ (φ \land u = U) \to u \times u = U \times U$
14		eqidd	$⊢ (φ \land u = U) \to (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f) = (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f)$
15	13 6 14	mpoeq123dv	$⊢ (φ \land u = U) \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))$
16	4	adantr	$⊢ (φ \land u = U) \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))$
17	15 16	eqtr4d	$⊢ (φ \land u = U) \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)) = \underset{˙}{\cdot}$
18	17	opeq2d	$⊢ (φ \land u = U) \to ⟨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))⟩ = ⟨comp (ndx), \underset{˙}{\cdot}⟩$
19	7 12 18	tpeq123d	$⊢ (φ \land u = U) \to \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ {Base}_{y}^{{Base}_{x}})⟩, ⟨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))⟩\} = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
20	2	elexd	$⊢ φ \to U \in V$
21		tpex	$⊢ \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
22	21	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
23	5 19 20 22	fvmptd2	$⊢ φ \to ExtStrCat (U) = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
24	1 23	eqtrid	$⊢ φ \to C = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Metamath Proof Explorer

Theorem estrcval

Proof