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

Metamath Proof Explorer

Theorem oppgoppchom

Description: The converted opposite monoid has the same hom-set as that of the opposite category. Example 3.6(2) of Adamek p. 25. (Contributed by Zhi Wang, 21-Sep-2025)

Ref Expression
Hypotheses mndtccat.c ⊢ φ → C = MndToCat ⁡ M
mndtccat.m ⊢ φ → M ∈ Mnd
oppgoppchom.d ⊢ φ → D = MndToCat ⁡ opp 𝑔 ⁡ M
oppgoppchom.o ⊢ O = oppCat ⁡ C
oppgoppchom.x ⊢ φ → X ∈ Base D
oppgoppchom.y ⊢ φ → Y ∈ Base O
oppgoppchom.h ⊢ φ → H = Hom ⁡ D
oppgoppchom.j ⊢ φ → J = Hom ⁡ O
Assertion oppgoppchom ⊢ φ → X H X = Y J Y

Proof

Step Hyp Ref Expression
1 mndtccat.c ⊢ φ → C = MndToCat ⁡ M
2 mndtccat.m ⊢ φ → M ∈ Mnd
3 oppgoppchom.d ⊢ φ → D = MndToCat ⁡ opp 𝑔 ⁡ M
4 oppgoppchom.o ⊢ O = oppCat ⁡ C
5 oppgoppchom.x ⊢ φ → X ∈ Base D
6 oppgoppchom.y ⊢ φ → Y ∈ Base O
7 oppgoppchom.h ⊢ φ → H = Hom ⁡ D
8 oppgoppchom.j ⊢ φ → J = Hom ⁡ O
9 eqid ⊢ opp 𝑔 ⁡ M = opp 𝑔 ⁡ M
10 eqid ⊢ Base M = Base M
11 9 10 oppgbas ⊢ Base M = Base opp 𝑔 ⁡ M
12 11 a1i ⊢ φ → Base M = Base opp 𝑔 ⁡ M
13 eqid ⊢ Base C = Base C
14 4 13 oppcbas ⊢ Base C = Base O
15 14 eqcomi ⊢ Base O = Base C
16 15 a1i ⊢ φ → Base O = Base C
17 eqidd ⊢ φ → Hom ⁡ C = Hom ⁡ C
18 1 2 16 6 6 17 mndtchom ⊢ φ → Y Hom ⁡ C Y = Base M
19 9 oppgmnd ⊢ M ∈ Mnd → opp 𝑔 ⁡ M ∈ Mnd
20 2 19 syl ⊢ φ → opp 𝑔 ⁡ M ∈ Mnd
21 eqidd ⊢ φ → Base D = Base D
22 3 20 21 5 5 7 mndtchom ⊢ φ → X H X = Base opp 𝑔 ⁡ M
23 12 18 22 3eqtr4rd ⊢ φ → X H X = Y Hom ⁡ C Y
24 eqid ⊢ Hom ⁡ C = Hom ⁡ C
25 24 4 oppchom ⊢ Y Hom ⁡ O Y = Y Hom ⁡ C Y
26 23 25 eqtr4di ⊢ φ → X H X = Y Hom ⁡ O Y
27 8 oveqd ⊢ φ → Y J Y = Y Hom ⁡ O Y
28 26 27 eqtr4d ⊢ φ → X H X = Y J Y