Theorem estrchomfeqhom

Description: The functionalized Hom-set operation equals the Hom-set operation in the category of extensible structures (in a universe). (Contributed by AV, 8-Mar-2020)

	Ref	Expression
Hypotheses	estrchomfn.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
	estrchomfn.u	$$⊢\phi \to U\in V$$
	estrchomfn.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	estrchomfeqhom	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)=H$$

Proof

Step	Hyp	Ref	Expression
1		estrchomfn.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
2		estrchomfn.u	$$⊢\phi \to U\in V$$
3		estrchomfn.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4	1 2 3	estrchomfn	$$⊢\phi \to HFn\left(U\times U\right)$$
5	1 2	estrcbas	$$⊢\phi \to U={\mathrm{Base}}_C$$
6	5	eqcomd	$$⊢\phi \to {\mathrm{Base}}_C=U$$
7	6	sqxpeqd	$$⊢\phi \to {\mathrm{Base}}_C\times {\mathrm{Base}}_C=U\times U$$
8	7	fneq2d	$$⊢\phi \to \left(HFn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\leftrightarrow HFn\left(U\times U\right)\right)$$
9	4 8	mpbird	$$⊢\phi \to HFn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
10		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
11		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
12	10 11 3	fnhomeqhomf	$$⊢HFn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)=H$$
13	9 12	syl	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)=H$$