Theorem oppchom

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

	Ref	Expression
Hypotheses	oppchom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	oppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	oppchom	$$⊢X\mathrm{Hom}\left(O\right)Y=YHX$$

Proof

Step	Hyp	Ref	Expression
1		oppchom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
2		oppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
3	1 2	oppchomfval	$$⊢tposH=\mathrm{Hom}\left(O\right)$$
4	3	oveqi	$$⊢XtposHY=X\mathrm{Hom}\left(O\right)Y$$
5		ovtpos	$$⊢XtposHY=YHX$$
6	4 5	eqtr3i	$$⊢X\mathrm{Hom}\left(O\right)Y=YHX$$