Theorem fnhomeqhomf

Description: If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020)

	Ref	Expression
Hypotheses	homffval.f	⊢ 𝐹 = ( Homf ‘ 𝐶 )
	homffval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	homffval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	fnhomeqhomf	⊢ ( 𝐻 Fn ( 𝐵 × 𝐵 ) → 𝐹 = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		homffval.f	⊢ 𝐹 = ( Homf ‘ 𝐶 )
2		homffval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		homffval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		fnov	⊢ ( 𝐻 Fn ( 𝐵 × 𝐵 ) ↔ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) )
5	1 2 3	homffval	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) )
6		eqeq2	⊢ ( 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) → ( 𝐹 = 𝐻 ↔ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) ) )
7	5 6	mpbiri	⊢ ( 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) → 𝐹 = 𝐻 )
8	4 7	sylbi	⊢ ( 𝐻 Fn ( 𝐵 × 𝐵 ) → 𝐹 = 𝐻 )