Theorem oppchom

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppchom.h	|- H = ( Hom ` C )
	oppchom.o	|- O = ( oppCat ` C )
Assertion	oppchom	|- ( X ( Hom ` O ) Y ) = ( Y H X )

Proof

Step	Hyp	Ref	Expression
1		oppchom.h	|- H = ( Hom ` C )
2		oppchom.o	|- O = ( oppCat ` C )
3	1 2	oppchomfval	|- tpos H = ( Hom ` O )
4	3	oveqi	|- ( X tpos H Y ) = ( X ( Hom ` O ) Y )
5		ovtpos	|- ( X tpos H Y ) = ( Y H X )
6	4 5	eqtr3i	|- ( X ( Hom ` O ) Y ) = ( Y H X )