Theorem estrchomfn

Description: The Hom-set operation in the category of extensible structures (in a universe) is a function. (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	estrchomfn	$$⊢\phi \to HFn\left(U\times U\right)$$

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		eqid	$$⊢\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		ovex	$$⊢{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\in \mathrm{V}$$
6	4 5	fnmpoi	$$⊢\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)Fn\left(U\times U\right)$$
7	1 2 3	estrchomfval	$$⊢\phi \to H=\left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$
8	7	fneq1d	$$⊢\phi \to \left(HFn\left(U\times U\right)\leftrightarrow \left(x\in U,y\in U⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)Fn\left(U\times U\right)\right)$$
9	6 8	mpbiri	$$⊢\phi \to HFn\left(U\times U\right)$$