Theorem estrchom

Description: The morphisms between extensible structures are mappings between their base sets. (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)$$
	estrchom.x	$$⊢\phi \to X\in U$$
	estrchom.y	$$⊢\phi \to Y\in U$$
	estrchom.a	$$⊢A={\mathrm{Base}}_X$$
	estrchom.b	$$⊢B={\mathrm{Base}}_Y$$
Assertion	estrchom	$$⊢\phi \to XHY=B^A$$

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		estrchom.x	$$⊢\phi \to X\in U$$
5		estrchom.y	$$⊢\phi \to Y\in U$$
6		estrchom.a	$$⊢A={\mathrm{Base}}_X$$
7		estrchom.b	$$⊢B={\mathrm{Base}}_Y$$
8	1 2 3	estrchomfval	$$⊢\phi \to H=\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$
9		fveq2	$$⊢y=Y\to {\mathrm{Base}}_y={\mathrm{Base}}_Y$$
10		fveq2	$$⊢x=X\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
11	9 10	oveqan12rd	$$⊢\left(x=X\wedge y=Y\right)\to {{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
12	7 6	oveq12i	$$⊢B^A={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
13	11 12	eqtr4di	$$⊢\left(x=X\wedge y=Y\right)\to {{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}=B^A$$
14	13	adantl	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to {{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}=B^A$$
15		ovexd	$$⊢\phi \to B^A\in \mathrm{V}$$
16	8 14 4 5 15	ovmpod	$$⊢\phi \to XHY=B^A$$