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 GFn\left(B\times 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\times 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\times 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 GFn\left(B\times B\right)$$
7	5 6	syl	$$⊢\phi \to GFn\left(B\times B\right)$$