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 ‘ 𝐷 ) ) )