# 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}={\mathrm{comp}}_{𝑓}\left({C}\right)$
comfffn.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
comffn.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
comffn.x ${⊢}{\phi }\to {X}\in {B}$
comffn.y ${⊢}{\phi }\to {Y}\in {B}$
comffn.z ${⊢}{\phi }\to {Z}\in {B}$
Assertion comffn ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{O}{Z}\right)Fn\left(\left({Y}{H}{Z}\right)×\left({X}{H}{Y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 comfffn.o ${⊢}{O}={\mathrm{comp}}_{𝑓}\left({C}\right)$
2 comfffn.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 comffn.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
4 comffn.x ${⊢}{\phi }\to {X}\in {B}$
5 comffn.y ${⊢}{\phi }\to {Y}\in {B}$
6 comffn.z ${⊢}{\phi }\to {Z}\in {B}$
7 eqid ${⊢}\left({g}\in \left({Y}{H}{Z}\right),{f}\in \left({X}{H}{Y}\right)⟼{g}\left(⟨{X},{Y}⟩\mathrm{comp}\left({C}\right){Z}\right){f}\right)=\left({g}\in \left({Y}{H}{Z}\right),{f}\in \left({X}{H}{Y}\right)⟼{g}\left(⟨{X},{Y}⟩\mathrm{comp}\left({C}\right){Z}\right){f}\right)$
8 ovex ${⊢}{g}\left(⟨{X},{Y}⟩\mathrm{comp}\left({C}\right){Z}\right){f}\in \mathrm{V}$
9 7 8 fnmpoi ${⊢}\left({g}\in \left({Y}{H}{Z}\right),{f}\in \left({X}{H}{Y}\right)⟼{g}\left(⟨{X},{Y}⟩\mathrm{comp}\left({C}\right){Z}\right){f}\right)Fn\left(\left({Y}{H}{Z}\right)×\left({X}{H}{Y}\right)\right)$
10 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
11 1 2 3 10 4 5 6 comffval ${⊢}{\phi }\to ⟨{X},{Y}⟩{O}{Z}=\left({g}\in \left({Y}{H}{Z}\right),{f}\in \left({X}{H}{Y}\right)⟼{g}\left(⟨{X},{Y}⟩\mathrm{comp}\left({C}\right){Z}\right){f}\right)$
12 11 fneq1d ${⊢}{\phi }\to \left(\left(⟨{X},{Y}⟩{O}{Z}\right)Fn\left(\left({Y}{H}{Z}\right)×\left({X}{H}{Y}\right)\right)↔\left({g}\in \left({Y}{H}{Z}\right),{f}\in \left({X}{H}{Y}\right)⟼{g}\left(⟨{X},{Y}⟩\mathrm{comp}\left({C}\right){Z}\right){f}\right)Fn\left(\left({Y}{H}{Z}\right)×\left({X}{H}{Y}\right)\right)\right)$
13 9 12 mpbiri ${⊢}{\phi }\to \left(⟨{X},{Y}⟩{O}{Z}\right)Fn\left(\left({Y}{H}{Z}\right)×\left({X}{H}{Y}\right)\right)$