Metamath Proof Explorer

Theorem estrcbas

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

		Ref	Expression
	Hypotheses	estrcbas.c	$⊢ C = ExtStrCat (U)$
		estrcbas.u	$⊢ φ \to U \in V$
	Assertion	estrcbas	$⊢ φ \to U = {Base}_{C}$

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	$⊢ C = ExtStrCat (U)$
2		estrcbas.u	$⊢ φ \to U \in V$
3		catstr	$⊢ \{⟨{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))⟩\} Struct ⟨1, 15⟩$
4		baseid	$⊢ Base = Slot {Base}_{ndx}$
5		snsstp1	$⊢ \{⟨{Base}_{ndx}, U⟩\} \subseteq \{⟨{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	3 4 5	strfv	$⊢ U \in V \to U = {Base}_{\{⟨{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))⟩\}}$
7	2 6	syl	$⊢ φ \to U = {Base}_{\{⟨{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))⟩\}}$
8		eqidd	$⊢ φ \to (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}}) = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
9		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))$
10	1 2 8 9	estrcval	$⊢ φ \to C = \{⟨{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))⟩\}$
11	10	fveq2d	$⊢ φ \to {Base}_{C} = {Base}_{\{⟨{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))⟩\}}$
12	7 11	eqtr4d	$⊢ φ \to U = {Base}_{C}$