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

Metamath Proof Explorer

Theorem comfffn

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

Ref Expression
Hypotheses comfffn.o ⊢ O = comp 𝑓 ⁡ C
comfffn.b ⊢ B = Base C
Assertion comfffn ⊢ O Fn B × B × B

Proof

Step Hyp Ref Expression
1 comfffn.o ⊢ O = comp 𝑓 ⁡ C
2 comfffn.b ⊢ B = Base C
3 eqid ⊢ Hom ⁡ C = Hom ⁡ C
4 eqid ⊢ comp ⁡ C = comp ⁡ C
5 1 2 3 4 comfffval ⊢ O = x ∈ B × B , y ∈ B ⟼ g ∈ 2 nd ⁡ x Hom ⁡ C y , f ∈ Hom ⁡ C ⁡ x ⟼ g x comp ⁡ C y f
6 ovex ⊢ 2 nd ⁡ x Hom ⁡ C y ∈ V
7 fvex ⊢ Hom ⁡ C ⁡ x ∈ V
8 6 7 mpoex ⊢ g ∈ 2 nd ⁡ x Hom ⁡ C y , f ∈ Hom ⁡ C ⁡ x ⟼ g x comp ⁡ C y f ∈ V
9 5 8 fnmpoi ⊢ O Fn B × B × B