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 = ( ExtStrCat ` U )
	estrchomfn.u	|- ( ph -> U e. V )
	estrchomfn.h	|- H = ( Hom ` C )
Assertion	estrchomfn	|- ( ph -> H Fn ( U X. U ) )

Proof

Step	Hyp	Ref	Expression
1		estrchomfn.c	|- C = ( ExtStrCat ` U )
2		estrchomfn.u	|- ( ph -> U e. V )
3		estrchomfn.h	|- H = ( Hom ` C )
4		eqid	|- ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) )
5		ovex	|- ( ( Base ` y ) ^m ( Base ` x ) ) e. _V
6	4 5	fnmpoi	|- ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) Fn ( U X. U )
7	1 2 3	estrchomfval	|- ( ph -> H = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
8	7	fneq1d	|- ( ph -> ( H Fn ( U X. U ) <-> ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) Fn ( U X. U ) ) )
9	6 8	mpbiri	|- ( ph -> H Fn ( U X. U ) )