Theorem coccom

Description: A co-cone to a diagram commutes with the diagram. (Contributed by Zhi Wang, 13-Nov-2025)

	Ref	Expression
Hypotheses	islmd.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	islmd.a	$$⊢A={\mathrm{Base}}_C$$
	islmd.n	$$⊢N=D\mathrm{Nat}C$$
	islmd.b	$$⊢B={\mathrm{Base}}_D$$
	concl.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
	concl.x	$$⊢\phi \to X\in A$$
	concl.y	$$⊢\phi \to Y\in B$$
	concom.z	$$⊢\phi \to Z\in B$$
	concom.m	$$⊢\phi \to M\in \left(YJZ\right)$$
	concom.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	concom.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	coccom.r	$$⊢\phi \to R\in \left(FNK\right)$$
Assertion	coccom	$$⊢\phi \to R\left(Y\right)=R\left(Z\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}X\right)\left(Y{2}^{nd}\left(F\right)Z\right)\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		islmd.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		islmd.a	$$⊢A={\mathrm{Base}}_C$$
3		islmd.n	$$⊢N=D\mathrm{Nat}C$$
4		islmd.b	$$⊢B={\mathrm{Base}}_D$$
5		concl.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
6		concl.x	$$⊢\phi \to X\in A$$
7		concl.y	$$⊢\phi \to Y\in B$$
8		concom.z	$$⊢\phi \to Z\in B$$
9		concom.m	$$⊢\phi \to M\in \left(YJZ\right)$$
10		concom.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
11		concom.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
12		coccom.r	$$⊢\phi \to R\in \left(FNK\right)$$
13	3 12	nat1st2nd	$$⊢\phi \to R\in \left(⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩N⟨1^{st}\left(K\right),2^{nd}\left(K\right)⟩\right)$$
14	3 13 4 10 11 7 8 9	nati	$$⊢\phi \to R\left(Z\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)\right)\left(Y{2}^{nd}\left(F\right)Z\right)\left(M\right)=\left(Y{2}^{nd}\left(K\right)Z\right)\left(M\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(K\right)\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)\right)R\left(Y\right)$$
15	3 13	natrcl2	$$⊢\phi \to 1^{st}\left(F\right)\left(D\mathrm{Func}C\right)2^{nd}\left(F\right)$$
16	15	funcrcl3	$$⊢\phi \to C\in \mathrm{Cat}$$
17	15	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
18	1 16 17 2 6 5 4 8	diag11	$$⊢\phi \to 1^{st}\left(K\right)\left(Z\right)=X$$
19	18	oveq2d	$$⊢\phi \to ⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)=⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}X$$
20	19	oveqd	$$⊢\phi \to R\left(Z\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)\right)\left(Y{2}^{nd}\left(F\right)Z\right)\left(M\right)=R\left(Z\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}X\right)\left(Y{2}^{nd}\left(F\right)Z\right)\left(M\right)$$
21	1 16 17 2 6 5 4 7	diag11	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=X$$
22	21	opeq2d	$$⊢\phi \to ⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(K\right)\left(Y\right)⟩=⟨1^{st}\left(F\right)\left(Y\right),X⟩$$
23	22 18	oveq12d	$$⊢\phi \to ⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(K\right)\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)=⟨1^{st}\left(F\right)\left(Y\right),X⟩\underset{\dot{}}{·}X$$
24		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
25	1 16 17 2 6 5 4 7 10 24 8 9	diag12	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(M\right)=\mathrm{Id}\left(C\right)\left(X\right)$$
26		eqidd	$$⊢\phi \to R\left(Y\right)=R\left(Y\right)$$
27	23 25 26	oveq123d	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(M\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(K\right)\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)\right)R\left(Y\right)=\mathrm{Id}\left(C\right)\left(X\right)\left(⟨1^{st}\left(F\right)\left(Y\right),X⟩\underset{\dot{}}{·}X\right)R\left(Y\right)$$
28		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
29	4 2 15	funcf1	$$⊢\phi \to 1^{st}\left(F\right):B⟶A$$
30	29 7	ffvelcdmd	$$⊢\phi \to 1^{st}\left(F\right)\left(Y\right)\in A$$
31	1 2 3 4 5 6 7 28 12	coccl	$$⊢\phi \to R\left(Y\right)\in \left(1^{st}\left(F\right)\left(Y\right)\mathrm{Hom}\left(C\right)X\right)$$
32	2 28 24 16 30 11 6 31	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\left(⟨1^{st}\left(F\right)\left(Y\right),X⟩\underset{\dot{}}{·}X\right)R\left(Y\right)=R\left(Y\right)$$
33	27 32	eqtrd	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(M\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(K\right)\left(Y\right)⟩\underset{\dot{}}{·}{1}^{st}\left(K\right)\left(Z\right)\right)R\left(Y\right)=R\left(Y\right)$$
34	14 20 33	3eqtr3rd	$$⊢\phi \to R\left(Y\right)=R\left(Z\right)\left(⟨1^{st}\left(F\right)\left(Y\right),1^{st}\left(F\right)\left(Z\right)⟩\underset{\dot{}}{·}X\right)\left(Y{2}^{nd}\left(F\right)Z\right)\left(M\right)$$