This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem homffn

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

Ref Expression
Hypotheses homffn.f ⊢ F = Hom 𝑓 ⁡ C
homffn.b ⊢ B = Base C
Assertion homffn ⊢ F Fn B × B

Proof

Step Hyp Ref Expression
1 homffn.f ⊢ F = Hom 𝑓 ⁡ C
2 homffn.b ⊢ B = Base C
3 eqid ⊢ Hom ⁡ C = Hom ⁡ C
4 1 2 3 homffval ⊢ F = x ∈ B , y ∈ B ⟼ x Hom ⁡ C y
5 ovex ⊢ x Hom ⁡ C y ∈ V
6 4 5 fnmpoi ⊢ F Fn B × B