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	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
Assertion	oppchomfpropd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(C\right)\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppchomfpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2	1	tposeqd	$$⊢\phi \to tpos{\mathrm{Hom}}_{𝑓}\left(C\right)=tpos{\mathrm{Hom}}_{𝑓}\left(D\right)$$
3		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
4		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
5	3 4	oppchomf	$$⊢tpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(C\right)\right)$$
6		eqid	$$⊢\mathrm{oppCat}\left(D\right)=\mathrm{oppCat}\left(D\right)$$
7		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
8	6 7	oppchomf	$$⊢tpos{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(D\right)\right)$$
9	2 5 8	3eqtr3g	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(C\right)\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(D\right)\right)$$