Theorem estrchomfval

Description: Set of morphisms ("arrows") 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$$
	estrchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	estrchomfval	$$⊢\phi \to H=\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$

Proof

Step	Hyp	Ref	Expression
1		estrcbas.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
2		estrcbas.u	$$⊢\phi \to U\in V$$
3		estrchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		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)$$
5		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)$$
6	1 2 4 5	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\}$$
7		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⟩$$
8		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
9		snsstp2	$$⊢\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩\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\}$$
10		mpoexga	$$⊢\left(U\in V\wedge U\in V\right)\to \left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)\in \mathrm{V}$$
11	2 2 10	syl2anc	$$⊢\phi \to \left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)\in \mathrm{V}$$
12	6 7 8 9 11 3	strfv3	$$⊢\phi \to H=\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$