Theorem oppchom

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

	Ref	Expression
Hypotheses	oppchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	oppchom.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion	oppchom	⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) = ( 𝑌 𝐻 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		oppchom.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
2		oppchom.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3	1 2	oppchomfval	⊢ tpos 𝐻 = ( Hom ‘ 𝑂 )
4	3	oveqi	⊢ ( 𝑋 tpos 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 )
5		ovtpos	⊢ ( 𝑋 tpos 𝐻 𝑌 ) = ( 𝑌 𝐻 𝑋 )
6	4 5	eqtr3i	⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑌 ) = ( 𝑌 𝐻 𝑋 )