This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2oppchomf

Description: The double opposite category has the same morphisms as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 ⊢ O = oppCat ⁡ C
Assertion 2oppchomf ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ O = oppCat ⁡ C
2 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
3 eqid ⊢ Base C = Base C
4 2 3 homffn ⊢ Hom 𝑓 ⁡ C Fn Base C × Base C
5 fnrel ⊢ Hom 𝑓 ⁡ C Fn Base C × Base C → Rel ⁡ Hom 𝑓 ⁡ C
6 4 5 ax-mp ⊢ Rel ⁡ Hom 𝑓 ⁡ C
7 relxp ⊢ Rel ⁡ Base C × Base C
8 4 fndmi ⊢ dom ⁡ Hom 𝑓 ⁡ C = Base C × Base C
9 8 releqi ⊢ Rel ⁡ dom ⁡ Hom 𝑓 ⁡ C ↔ Rel ⁡ Base C × Base C
10 7 9 mpbir ⊢ Rel ⁡ dom ⁡ Hom 𝑓 ⁡ C
11 tpostpos2 ⊢ Rel ⁡ Hom 𝑓 ⁡ C ∧ Rel ⁡ dom ⁡ Hom 𝑓 ⁡ C → tpos tpos Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
12 6 10 11 mp2an ⊢ tpos tpos Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
13 eqid ⊢ oppCat ⁡ O = oppCat ⁡ O
14 1 2 oppchomf ⊢ tpos Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ O
15 13 14 oppchomf ⊢ tpos tpos Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
16 12 15 eqtr3i ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O