Theorem 2oppccomf

Description: The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypothesis	oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
3	1 2	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
4		eqid	$$⊢\mathrm{comp}\left(O\right)=\mathrm{comp}\left(O\right)$$
5		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
6		simpr1	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\to x\in {\mathrm{Base}}_C$$
7		simpr2	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\to y\in {\mathrm{Base}}_C$$
8		simpr3	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\to z\in {\mathrm{Base}}_C$$
9	3 4 5 6 7 8	oppcco	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\to g\left(⟨x,y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(O\right)\right)z\right)f=f\left(⟨z,y⟩\mathrm{comp}\left(O\right)x\right)g$$
10		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
11	2 10 1 8 7 6	oppcco	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\to f\left(⟨z,y⟩\mathrm{comp}\left(O\right)x\right)g=g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f$$
12	9 11	eqtr2d	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\to g\left(⟨x,y⟩\mathrm{comp}\left(C\right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(O\right)\right)z\right)f$$
13	12	ralrimivw	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\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(\mathrm{oppCat}\left(O\right)\right)z\right)f$$
14	13	ralrimivw	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_C\wedge y\in {\mathrm{Base}}_C\wedge z\in {\mathrm{Base}}_C\right)\right)\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(\mathrm{oppCat}\left(O\right)\right)z\right)f$$
15	14	ralrimivvva	$$⊢\top \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(\mathrm{oppCat}\left(O\right)\right)z\right)f$$
16		eqid	$$⊢\mathrm{comp}\left(\mathrm{oppCat}\left(O\right)\right)=\mathrm{comp}\left(\mathrm{oppCat}\left(O\right)\right)$$
17		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
18		eqidd	$$⊢\top \to {\mathrm{Base}}_C={\mathrm{Base}}_C$$
19	1 2	2oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\mathrm{oppCat}\left(O\right)}$$
20	19	a1i	$$⊢\top \to {\mathrm{Base}}_C={\mathrm{Base}}_{\mathrm{oppCat}\left(O\right)}$$
21	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
22	21	a1i	$$⊢\top \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
23	10 16 17 18 20 22	comfeq	$$⊢\top \to \left({\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\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(\mathrm{oppCat}\left(O\right)\right)z\right)f\right)$$
24	15 23	mpbird	$$⊢\top \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
25	24	mptru	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$