Theorem cofulid

Description: The identity functor is a left identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofulid.g	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	cofulid.1	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
Assertion	cofulid	$$⊢\phi \to I{\circ }_{\mathrm{func}}F=F$$

Proof

Step	Hyp	Ref	Expression
1		cofulid.g	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
2		cofulid.1	$$⊢I={id}_{\mathrm{func}}\left(D\right)$$
3		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
4		funcrcl	$$⊢F\in \left(C\mathrm{Func}D\right)\to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)$$
5	1 4	syl	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)$$
6	5	simprd	$$⊢\phi \to D\in \mathrm{Cat}$$
7	2 3 6	idfu1st	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}$$
8	7	coeq1d	$$⊢\phi \to 1^{st}\left(I\right)\circ 1^{st}\left(F\right)=\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\circ 1^{st}\left(F\right)$$
9		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
10		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
11		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
12	10 1 11	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
13	9 3 12	funcf1	$$⊢\phi \to 1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D$$
14		fcoi2	$$⊢1^{st}\left(F\right):{\mathrm{Base}}_C⟶{\mathrm{Base}}_D\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\circ 1^{st}\left(F\right)=1^{st}\left(F\right)$$
15	13 14	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\circ 1^{st}\left(F\right)=1^{st}\left(F\right)$$
16	8 15	eqtrd	$$⊢\phi \to 1^{st}\left(I\right)\circ 1^{st}\left(F\right)=1^{st}\left(F\right)$$
17	6	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to D\in \mathrm{Cat}$$
18		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
19	13	ffvelcdmda	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_D$$
20	19	3adant3	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(x\right)\in {\mathrm{Base}}_D$$
21	13	ffvelcdmda	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(y\right)\in {\mathrm{Base}}_D$$
22	21	3adant2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(y\right)\in {\mathrm{Base}}_D$$
23	2 3 17 18 20 22	idfu2nd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)={\mathrm{I}\upharpoonright }_{\left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(y\right)\right)}$$
24	23	coeq1d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)=\left({\mathrm{I}\upharpoonright }_{\left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(y\right)\right)}\right)\circ \left(x{2}^{nd}\left(F\right)y\right)$$
25		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
26	12	3ad2ant1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
27		simp2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to x\in {\mathrm{Base}}_C$$
28		simp3	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to y\in {\mathrm{Base}}_C$$
29	9 25 18 26 27 28	funcf2	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to \left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(C\right)y⟶1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(y\right)$$
30		fcoi2	$$⊢\left(x{2}^{nd}\left(F\right)y\right):x\mathrm{Hom}\left(C\right)y⟶1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(y\right)\to \left({\mathrm{I}\upharpoonright }_{\left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(y\right)\right)}\right)\circ \left(x{2}^{nd}\left(F\right)y\right)=x{2}^{nd}\left(F\right)y$$
31	29 30	syl	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to \left({\mathrm{I}\upharpoonright }_{\left(1^{st}\left(F\right)\left(x\right)\mathrm{Hom}\left(D\right)1^{st}\left(F\right)\left(y\right)\right)}\right)\circ \left(x{2}^{nd}\left(F\right)y\right)=x{2}^{nd}\left(F\right)y$$
32	24 31	eqtrd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\right)\to \left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)=x{2}^{nd}\left(F\right)y$$
33	32	mpoeq3dva	$$⊢\phi \to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x{2}^{nd}\left(F\right)y\right)$$
34	9 12	funcfn2	$$⊢\phi \to 2^{nd}\left(F\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
35		fnov	$$⊢2^{nd}\left(F\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\leftrightarrow 2^{nd}\left(F\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x{2}^{nd}\left(F\right)y\right)$$
36	34 35	sylib	$$⊢\phi \to 2^{nd}\left(F\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼x{2}^{nd}\left(F\right)y\right)$$
37	33 36	eqtr4d	$$⊢\phi \to \left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)=2^{nd}\left(F\right)$$
38	16 37	opeq12d	$$⊢\phi \to ⟨1^{st}\left(I\right)\circ 1^{st}\left(F\right),\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
39	2	idfucl	$$⊢D\in \mathrm{Cat}\to I\in \left(D\mathrm{Func}D\right)$$
40	6 39	syl	$$⊢\phi \to I\in \left(D\mathrm{Func}D\right)$$
41	9 1 40	cofuval	$$⊢\phi \to I{\circ }_{\mathrm{func}}F=⟨1^{st}\left(I\right)\circ 1^{st}\left(F\right),\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(I\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩$$
42		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
43	10 1 42	sylancr	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
44	38 41 43	3eqtr4d	$$⊢\phi \to I{\circ }_{\mathrm{func}}F=F$$