This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppchomfpropd

Description: If two categories have the same hom-sets, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypothesis oppchomfpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
Assertion oppchomfpropd 
|- ( ph -> ( Homf ` ( oppCat ` C ) ) = ( Homf ` ( oppCat ` D ) ) )

Proof

Step Hyp Ref Expression
1 oppchomfpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 1 tposeqd 
 |-  ( ph -> tpos ( Homf ` C ) = tpos ( Homf ` D ) )
3 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
4 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
5 3 4 oppchomf 
 |-  tpos ( Homf ` C ) = ( Homf ` ( oppCat ` C ) )
6 eqid 
 |-  ( oppCat ` D ) = ( oppCat ` D )
7 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
8 6 7 oppchomf 
 |-  tpos ( Homf ` D ) = ( Homf ` ( oppCat ` D ) )
9 2 5 8 3eqtr3g 
 |-  ( ph -> ( Homf ` ( oppCat ` C ) ) = ( Homf ` ( oppCat ` D ) ) )