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

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	1 2 3	estrchomfn	|- ( ph -> H Fn ( U X. U ) )
5	1 2	estrcbas	|- ( ph -> U = ( Base ` C ) )
6	5	eqcomd	|- ( ph -> ( Base ` C ) = U )
7	6	sqxpeqd	|- ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = ( U X. U ) )
8	7	fneq2d	|- ( ph -> ( H Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> H Fn ( U X. U ) ) )
9	4 8	mpbird	|- ( ph -> H Fn ( ( Base ` C ) X. ( Base ` C ) ) )
10		eqid	|- ( Homf ` C ) = ( Homf ` C )
11		eqid	|- ( Base ` C ) = ( Base ` C )
12	10 11 3	fnhomeqhomf	|- ( H Fn ( ( Base ` C ) X. ( Base ` C ) ) -> ( Homf ` C ) = H )
13	9 12	syl	|- ( ph -> ( Homf ` C ) = H )