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=\mathrm{ExtStrCat}\left(U\right)$$
	estrcbas.u	$$⊢\phi \to U\in V$$
Assertion	estrcbas	$$⊢\phi \to U={\mathrm{Base}}_C$$

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
2		estrcbas.u	$$⊢\phi \to U\in V$$
3		catstr	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}\mathrm{Struct}⟨1,15⟩$$
4		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5		snsstp1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}$$
6	3 4 5	strfv	$$⊢U\in V\to U={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}}$$
7	2 6	syl	$$⊢\phi \to U={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}}$$
8		eqidd	$$⊢\phi \to \left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)=\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$
9		eqidd	$$⊢\phi \to \left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)=\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)$$
10	1 2 8 9	estrcval	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}$$
11	10	fveq2d	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(U\times U\right),z\in U⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}}$$
12	7 11	eqtr4d	$$⊢\phi \to U={\mathrm{Base}}_C$$