Theorem funcixp

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

	Ref	Expression
Hypotheses	funcixp.b	$$⊢B={\mathrm{Base}}_D$$
	funcixp.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	funcixp.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
	funcixp.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
Assertion	funcixp	$$⊢\phi \to G\in \underset{z\in B\times B}{⨉}\left({\left(F\left(1^{st}\left(z\right)\right)JF\left(2^{nd}\left(z\right)\right)\right)}^{H\left(z\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcixp.b	$$⊢B={\mathrm{Base}}_D$$
2		funcixp.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
3		funcixp.j	$$⊢J=\mathrm{Hom}\left(E\right)$$
4		funcixp.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
5		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
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	4 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 5 2 3 6 7 8 9 14 15	isfunc	$$⊢\phi \to \left(F\left(D\mathrm{Func}E\right)G\leftrightarrow \left(F:B⟶{\mathrm{Base}}_E\wedge G\in \underset{z\in B\times B}{⨉}\left({\left(F\left(1^{st}\left(z\right)\right)JF\left(2^{nd}\left(z\right)\right)\right)}^{H\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(xHy\right)\forall n\in \left(yHz\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	4 16	mpbid	$$⊢\phi \to \left(F:B⟶{\mathrm{Base}}_E\wedge G\in \underset{z\in B\times B}{⨉}\left({\left(F\left(1^{st}\left(z\right)\right)JF\left(2^{nd}\left(z\right)\right)\right)}^{H\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(xHy\right)\forall n\in \left(yHz\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	simp2d	$$⊢\phi \to G\in \underset{z\in B\times B}{⨉}\left({\left(F\left(1^{st}\left(z\right)\right)JF\left(2^{nd}\left(z\right)\right)\right)}^{H\left(z\right)}\right)$$