Theorem homffn

Description: The functionalized Hom-set operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	homffn.f	⊢ 𝐹 = ( Homf ‘ 𝐶 )
	homffn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	homffn	⊢ 𝐹 Fn ( 𝐵 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		homffn.f	⊢ 𝐹 = ( Homf ‘ 𝐶 )
2		homffn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4	1 2 3	homffval	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
5		ovex	⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
6	4 5	fnmpoi	⊢ 𝐹 Fn ( 𝐵 × 𝐵 )