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 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
Assertion oppchomfpropd ⊢ φ → Hom 𝑓 ⁡ oppCat ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ D

Proof

Step Hyp Ref Expression
1 oppchomfpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
2 1 tposeqd ⊢ φ → tpos Hom 𝑓 ⁡ C = tpos Hom 𝑓 ⁡ D
3 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
4 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
5 3 4 oppchomf ⊢ tpos Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ C
6 eqid ⊢ oppCat ⁡ D = oppCat ⁡ D
7 eqid ⊢ Hom 𝑓 ⁡ D = Hom 𝑓 ⁡ D
8 6 7 oppchomf ⊢ tpos Hom 𝑓 ⁡ D = Hom 𝑓 ⁡ oppCat ⁡ D
9 2 5 8 3eqtr3g ⊢ φ → Hom 𝑓 ⁡ oppCat ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ D