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