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	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
	estrchomfn.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	estrchomfn.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	estrchomfeqhom	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		estrchomfn.c	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2		estrchomfn.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		estrchomfn.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4	1 2 3	estrchomfn	⊢ ( 𝜑 → 𝐻 Fn ( 𝑈 × 𝑈 ) )
5	1 2	estrcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐶 ) )
6	5	eqcomd	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = 𝑈 )
7	6	sqxpeqd	⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ( 𝑈 × 𝑈 ) )
8	7	fneq2d	⊢ ( 𝜑 → ( 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ 𝐻 Fn ( 𝑈 × 𝑈 ) ) )
9	4 8	mpbird	⊢ ( 𝜑 → 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
10		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12	10 11 3	fnhomeqhomf	⊢ ( 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) → ( Homf ‘ 𝐶 ) = 𝐻 )
13	9 12	syl	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = 𝐻 )