Theorem comfeqd

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfeqd.1	$$⊢\phi \to \mathrm{comp}\left(C\right)=\mathrm{comp}\left(D\right)$$
	comfeqd.2	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
Assertion	comfeqd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		comfeqd.1	$$⊢\phi \to \mathrm{comp}\left(C\right)=\mathrm{comp}\left(D\right)$$
2		comfeqd.2	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
3	1	oveqd	$$⊢\phi \to ⟨x,y⟩\mathrm{comp}\left(C\right)z=⟨x,y⟩\mathrm{comp}\left(D\right)z$$
4	3	oveqd	$$⊢\phi \to g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
5	4	ralrimivw	$$⊢\phi \to \forall g\in \left(y\mathrm{Hom}\left(C\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
6	5	ralrimivw	$$⊢\phi \to \forall f\in \left(x\mathrm{Hom}\left(C\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(C\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
7	6	ralrimivw	$$⊢\phi \to \forall z\in {\mathrm{Base}}_C\forall f\in \left(x\mathrm{Hom}\left(C\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(C\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
8	7	ralrimivw	$$⊢\phi \to \forall y\in {\mathrm{Base}}_C\forall z\in {\mathrm{Base}}_C\forall f\in \left(x\mathrm{Hom}\left(C\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(C\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
9	8	ralrimivw	$$⊢\phi \to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in {\mathrm{Base}}_C\forall f\in \left(x\mathrm{Hom}\left(C\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(C\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f$$
10		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
11		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
12		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
13		eqidd	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_C$$
14	2	homfeqbas	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$
15	10 11 12 13 14 2	comfeq	$$⊢\phi \to \left({\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)\leftrightarrow \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall z\in {\mathrm{Base}}_C\forall f\in \left(x\mathrm{Hom}\left(C\right)y\right)\forall g\in \left(y\mathrm{Hom}\left(C\right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(D\right)z\right)f\right)$$
16	9 15	mpbird	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$