Theorem elestrchom

Description: A morphism between extensible structures is a function 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	elestrchom	$$⊢\phi \to \left(F\in \left(XHY\right)\leftrightarrow F:A⟶B\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		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 4 5 6 7	estrchom	$$⊢\phi \to XHY=B^A$$
9	8	eleq2d	$$⊢\phi \to \left(F\in \left(XHY\right)\leftrightarrow F\in \left(B^A\right)\right)$$
10	7	fvexi	$$⊢B\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to B\in \mathrm{V}$$
12	6	fvexi	$$⊢A\in \mathrm{V}$$
13	12	a1i	$$⊢\phi \to A\in \mathrm{V}$$
14	11 13	elmapd	$$⊢\phi \to \left(F\in \left(B^A\right)\leftrightarrow F:A⟶B\right)$$
15	9 14	bitrd	$$⊢\phi \to \left(F\in \left(XHY\right)\leftrightarrow F:A⟶B\right)$$