Metamath Proof Explorer

Theorem comffn

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
comffn.h ⊢ H = Hom ⁡ C
comffn.x ⊢ φ → X ∈ B
comffn.y ⊢ φ → Y ∈ B
comffn.z ⊢ φ → Z ∈ B
Assertion comffn ⊢ φ → X Y O Z Fn Y H Z × X H Y

Proof

Step Hyp Ref Expression
1 comfffn.o ⊢ O = comp 𝑓 ⁡ C
2 comfffn.b ⊢ B = Base C
3 comffn.h ⊢ H = Hom ⁡ C
4 comffn.x ⊢ φ → X ∈ B
5 comffn.y ⊢ φ → Y ∈ B
6 comffn.z ⊢ φ → Z ∈ B
7 eqid ⊢ g ∈ Y H Z , f ∈ X H Y ⟼ g X Y comp ⁡ C Z f = g ∈ Y H Z , f ∈ X H Y ⟼ g X Y comp ⁡ C Z f
8 ovex ⊢ g X Y comp ⁡ C Z f ∈ V
9 7 8 fnmpoi ⊢ g ∈ Y H Z , f ∈ X H Y ⟼ g X Y comp ⁡ C Z f Fn Y H Z × X H Y
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 1 2 3 10 4 5 6 comffval ⊢ φ → X Y O Z = g ∈ Y H Z , f ∈ X H Y ⟼ g X Y comp ⁡ C Z f
12 11 fneq1d ⊢ φ → X Y O Z Fn Y H Z × X H Y ↔ g ∈ Y H Z , f ∈ X H Y ⟼ g X Y comp ⁡ C Z f Fn Y H Z × X H Y
13 9 12 mpbiri ⊢ φ → X Y O Z Fn Y H Z × X H Y