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

Proof

Step	Hyp	Ref	Expression
1		estrchomfn.c	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2		estrchomfn.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		estrchomfn.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		eqid	⊢ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) )
5		ovex	⊢ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ∈ V
6	4 5	fnmpoi	⊢ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) Fn ( 𝑈 × 𝑈 )
7	1 2 3	estrchomfval	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
8	7	fneq1d	⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑈 × 𝑈 ) ↔ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) Fn ( 𝑈 × 𝑈 ) ) )
9	6 8	mpbiri	⊢ ( 𝜑 → 𝐻 Fn ( 𝑈 × 𝑈 ) )