# Metamath Proof Explorer

## Theorem funcfn2

Description: The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses funcfn2.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
funcfn2.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
Assertion funcfn2 ${⊢}{\phi }\to {G}Fn\left({B}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 funcfn2.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
2 funcfn2.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
3 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
4 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
5 1 3 4 2 funcixp ${⊢}{\phi }\to {G}\in \underset{{x}\in {B}×{B}}{⨉}\left({\left({F}\left({1}^{st}\left({x}\right)\right)\mathrm{Hom}\left({E}\right){F}\left({2}^{nd}\left({x}\right)\right)\right)}^{\mathrm{Hom}\left({D}\right)\left({x}\right)}\right)$
6 ixpfn ${⊢}{G}\in \underset{{x}\in {B}×{B}}{⨉}\left({\left({F}\left({1}^{st}\left({x}\right)\right)\mathrm{Hom}\left({E}\right){F}\left({2}^{nd}\left({x}\right)\right)\right)}^{\mathrm{Hom}\left({D}\right)\left({x}\right)}\right)\to {G}Fn\left({B}×{B}\right)$
7 5 6 syl ${⊢}{\phi }\to {G}Fn\left({B}×{B}\right)$