Theorem funcid

Description: A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	funcid.b	$$⊢B={\mathrm{Base}}_D$$
	funcid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(D\right)$$
	funcid.i	$$⊢I=\mathrm{Id}\left(E\right)$$
	funcid.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	funcid.x	$$⊢\phi \to X\in B$$
Assertion	funcid	$$⊢\phi \to \left(XGX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)=I\left(F\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcid.b	$$⊢B={\mathrm{Base}}_D$$
2		funcid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(D\right)$$
3		funcid.i	$$⊢I=\mathrm{Id}\left(E\right)$$
4		funcid.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
5		funcid.x	$$⊢\phi \to X\in B$$
6		id	$$⊢x=X\to x=X$$
7	6 6	oveq12d	$$⊢x=X\to xGx=XGX$$
8		fveq2	$$⊢x=X\to \underset{\dot{}}{1}\left(x\right)=\underset{\dot{}}{1}\left(X\right)$$
9	7 8	fveq12d	$$⊢x=X\to \left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=\left(XGX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)$$
10		2fveq3	$$⊢x=X\to I\left(F\left(x\right)\right)=I\left(F\left(X\right)\right)$$
11	9 10	eqeq12d	$$⊢x=X\to \left(\left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\left(F\left(x\right)\right)\leftrightarrow \left(XGX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)=I\left(F\left(X\right)\right)\right)$$
12		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
13		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
14		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
15		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
16		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
17		df-br	$$⊢F\left(D\mathrm{Func}E\right)G\leftrightarrow ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
18	4 17	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
19		funcrcl	$$⊢⟨F,G⟩\in \left(D\mathrm{Func}E\right)\to \left(D\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
20	18 19	syl	$$⊢\phi \to \left(D\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
21	20	simpld	$$⊢\phi \to D\in \mathrm{Cat}$$
22	20	simprd	$$⊢\phi \to E\in \mathrm{Cat}$$
23	1 12 13 14 2 3 15 16 21 22	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)\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(\underset{\dot{}}{1}\left(x\right)\right)=I\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)$$
24	4 23	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)\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(\underset{\dot{}}{1}\left(x\right)\right)=I\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)$$
25	24	simp3d	$$⊢\phi \to \forall x\in B\left(\left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\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)$$
26		simpl	$$⊢\left(\left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\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)\to \left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\left(F\left(x\right)\right)$$
27	26	ralimi	$$⊢\forall x\in B\left(\left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\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)\to \forall x\in B\left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\left(F\left(x\right)\right)$$
28	25 27	syl	$$⊢\phi \to \forall x\in B\left(xGx\right)\left(\underset{\dot{}}{1}\left(x\right)\right)=I\left(F\left(x\right)\right)$$
29	11 28 5	rspcdva	$$⊢\phi \to \left(XGX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)=I\left(F\left(X\right)\right)$$