# Metamath Proof Explorer

## Theorem funcf1

Description: The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcf1.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
funcf1.c ${⊢}{C}={\mathrm{Base}}_{{E}}$
funcf1.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
Assertion funcf1 ${⊢}{\phi }\to {F}:{B}⟶{C}$

### Proof

Step Hyp Ref Expression
1 funcf1.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
2 funcf1.c ${⊢}{C}={\mathrm{Base}}_{{E}}$
3 funcf1.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
4 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
5 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
6 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
7 eqid ${⊢}\mathrm{Id}\left({E}\right)=\mathrm{Id}\left({E}\right)$
8 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
9 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
10 df-br ${⊢}{F}\left({D}\mathrm{Func}{E}\right){G}↔⟨{F},{G}⟩\in \left({D}\mathrm{Func}{E}\right)$
11 3 10 sylib ${⊢}{\phi }\to ⟨{F},{G}⟩\in \left({D}\mathrm{Func}{E}\right)$
12 funcrcl ${⊢}⟨{F},{G}⟩\in \left({D}\mathrm{Func}{E}\right)\to \left({D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
13 11 12 syl ${⊢}{\phi }\to \left({D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
14 13 simpld ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
15 13 simprd ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
16 1 2 4 5 6 7 8 9 14 15 isfunc ${⊢}{\phi }\to \left({F}\left({D}\mathrm{Func}{E}\right){G}↔\left({F}:{B}⟶{C}\wedge {G}\in \underset{{z}\in {B}×{B}}{⨉}\left({\left({F}\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){F}\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({D}\right)\left({z}\right)}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{G}{x}\right)\left(\mathrm{Id}\left({D}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({F}\left({x}\right)\right)\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {m}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\right)\left({n}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){m}\right)=\left({y}{G}{z}\right)\left({n}\right)\left(⟨{F}\left({x}\right),{F}\left({y}\right)⟩\mathrm{comp}\left({E}\right){F}\left({z}\right)\right)\left({x}{G}{y}\right)\left({m}\right)\right)\right)\right)$
17 3 16 mpbid ${⊢}{\phi }\to \left({F}:{B}⟶{C}\wedge {G}\in \underset{{z}\in {B}×{B}}{⨉}\left({\left({F}\left({1}^{st}\left({z}\right)\right)\mathrm{Hom}\left({E}\right){F}\left({2}^{nd}\left({z}\right)\right)\right)}^{\mathrm{Hom}\left({D}\right)\left({z}\right)}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({x}{G}{x}\right)\left(\mathrm{Id}\left({D}\right)\left({x}\right)\right)=\mathrm{Id}\left({E}\right)\left({F}\left({x}\right)\right)\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {m}\in \left({x}\mathrm{Hom}\left({D}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {n}\in \left({y}\mathrm{Hom}\left({D}\right){z}\right)\phantom{\rule{.4em}{0ex}}\left({x}{G}{z}\right)\left({n}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){m}\right)=\left({y}{G}{z}\right)\left({n}\right)\left(⟨{F}\left({x}\right),{F}\left({y}\right)⟩\mathrm{comp}\left({E}\right){F}\left({z}\right)\right)\left({x}{G}{y}\right)\left({m}\right)\right)\right)$
18 17 simp1d ${⊢}{\phi }\to {F}:{B}⟶{C}$