Metamath Proof Explorer


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 )