Theorem oppcco

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcco.b	$$⊢B={\mathrm{Base}}_C$$
	oppcco.c	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	oppcco.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcco.x	$$⊢\phi \to X\in B$$
	oppcco.y	$$⊢\phi \to Y\in B$$
	oppcco.z	$$⊢\phi \to Z\in B$$
Assertion	oppcco	$$⊢\phi \to G\left(⟨X,Y⟩\mathrm{comp}\left(O\right)Z\right)F=F\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)G$$

Proof

Step	Hyp	Ref	Expression
1		oppcco.b	$$⊢B={\mathrm{Base}}_C$$
2		oppcco.c	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
3		oppcco.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
4		oppcco.x	$$⊢\phi \to X\in B$$
5		oppcco.y	$$⊢\phi \to Y\in B$$
6		oppcco.z	$$⊢\phi \to Z\in B$$
7	1 2 3 4 5 6	oppccofval	$$⊢\phi \to ⟨X,Y⟩\mathrm{comp}\left(O\right)Z=tpos\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)$$
8	7	oveqd	$$⊢\phi \to G\left(⟨X,Y⟩\mathrm{comp}\left(O\right)Z\right)F=Gtpos\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)F$$
9		ovtpos	$$⊢Gtpos\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)F=F\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)G$$
10	8 9	eqtrdi	$$⊢\phi \to G\left(⟨X,Y⟩\mathrm{comp}\left(O\right)Z\right)F=F\left(⟨Z,Y⟩\underset{\dot{}}{·}X\right)G$$