Theorem oppcco

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

	Ref	Expression
Hypotheses	oppcco.b	|- B = ( Base ` C )
	oppcco.c	|- .x. = ( comp ` C )
	oppcco.o	|- O = ( oppCat ` C )
	oppcco.x	|- ( ph -> X e. B )
	oppcco.y	|- ( ph -> Y e. B )
	oppcco.z	|- ( ph -> Z e. B )
Assertion	oppcco	|- ( ph -> ( G ( <. X , Y >. ( comp ` O ) Z ) F ) = ( F ( <. Z , Y >. .x. X ) G ) )

Proof

Step	Hyp	Ref	Expression
1		oppcco.b	|- B = ( Base ` C )
2		oppcco.c	|- .x. = ( comp ` C )
3		oppcco.o	|- O = ( oppCat ` C )
4		oppcco.x	|- ( ph -> X e. B )
5		oppcco.y	|- ( ph -> Y e. B )
6		oppcco.z	|- ( ph -> Z e. B )
7	1 2 3 4 5 6	oppccofval	|- ( ph -> ( <. X , Y >. ( comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )
8	7	oveqd	|- ( ph -> ( G ( <. X , Y >. ( comp ` O ) Z ) F ) = ( G tpos ( <. Z , Y >. .x. X ) F ) )
9		ovtpos	|- ( G tpos ( <. Z , Y >. .x. X ) F ) = ( F ( <. Z , Y >. .x. X ) G )
10	8 9	eqtrdi	|- ( ph -> ( G ( <. X , Y >. ( comp ` O ) Z ) F ) = ( F ( <. Z , Y >. .x. X ) G ) )