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 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
Assertion oppchomfpropd ( 𝜑 → ( Homf ‘ ( oppCat ‘ 𝐶 ) ) = ( Homf ‘ ( oppCat ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 oppchomfpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 1 tposeqd ⊢ ( 𝜑 → tpos ( Homf ‘ 𝐶 ) = tpos ( Homf ‘ 𝐷 ) )
3 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
4 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
5 3 4 oppchomf ⊢ tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝐶 ) )
6 eqid ⊢ ( oppCat ‘ 𝐷 ) = ( oppCat ‘ 𝐷 )
7 eqid ⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 )
8 6 7 oppchomf ⊢ tpos ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝐷 ) )
9 2 5 8 3eqtr3g ⊢ ( 𝜑 → ( Homf ‘ ( oppCat ‘ 𝐶 ) ) = ( Homf ‘ ( oppCat ‘ 𝐷 ) ) )