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

Metamath Proof Explorer

Theorem oppchomf

Description: Hom-sets of the opposite category. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses oppcbas.1 ⊢ O = oppCat ⁡ C
oppchomf.h ⊢ H = Hom 𝑓 ⁡ C
Assertion oppchomf ⊢ tpos H = Hom 𝑓 ⁡ O

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ O = oppCat ⁡ C
2 oppchomf.h ⊢ H = Hom 𝑓 ⁡ C
3 eqid ⊢ Hom ⁡ C = Hom ⁡ C
4 3 1 oppchom ⊢ y Hom ⁡ O x = x Hom ⁡ C y
5 4 a1i ⊢ y ∈ Base C ∧ x ∈ Base C → y Hom ⁡ O x = x Hom ⁡ C y
6 5 mpoeq3ia ⊢ y ∈ Base C , x ∈ Base C ⟼ y Hom ⁡ O x = y ∈ Base C , x ∈ Base C ⟼ x Hom ⁡ C y
7 eqid ⊢ Hom 𝑓 ⁡ O = Hom 𝑓 ⁡ O
8 eqid ⊢ Base C = Base C
9 1 8 oppcbas ⊢ Base C = Base O
10 eqid ⊢ Hom ⁡ O = Hom ⁡ O
11 7 9 10 homffval ⊢ Hom 𝑓 ⁡ O = y ∈ Base C , x ∈ Base C ⟼ y Hom ⁡ O x
12 2 8 3 homffval ⊢ H = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y
13 12 tposmpo ⊢ tpos H = y ∈ Base C , x ∈ Base C ⟼ x Hom ⁡ C y
14 6 11 13 3eqtr4ri ⊢ tpos H = Hom 𝑓 ⁡ O