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\leftrightarrow ⟨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\leftrightarrow \left(F:B⟶C\wedge G\in \underset{z\in B\times 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\left(\left(xGx\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\forall z\in B\forall m\in \left(x\mathrm{Hom}\left(D\right)y\right)\forall n\in \left(y\mathrm{Hom}\left(D\right)z\right)\left(xGz\right)\left(n\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)m\right)=\left(yGz\right)\left(n\right)\left(⟨F\left(x\right),F\left(y\right)⟩\mathrm{comp}\left(E\right)F\left(z\right)\right)\left(xGy\right)\left(m\right)\right)\right)\right)$$
17	3 16	mpbid	$$⊢\phi \to \left(F:B⟶C\wedge G\in \underset{z\in B\times 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\left(\left(xGx\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\forall z\in B\forall m\in \left(x\mathrm{Hom}\left(D\right)y\right)\forall n\in \left(y\mathrm{Hom}\left(D\right)z\right)\left(xGz\right)\left(n\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)m\right)=\left(yGz\right)\left(n\right)\left(⟨F\left(x\right),F\left(y\right)⟩\mathrm{comp}\left(E\right)F\left(z\right)\right)\left(xGy\right)\left(m\right)\right)\right)$$
18	17	simp1d	$$⊢\phi \to F:B⟶C$$