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 ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
oppgoppchom.d ⊢ ( 𝜑 → 𝐷 = ( MndToCat ‘ ( oppg ‘ 𝑀 ) ) )
oppgoppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppgoppchom.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
oppgoppchom.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑂 ) )
oppgoppchom.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐷 ) )
oppgoppchom.j ⊢ ( 𝜑 → 𝐽 = ( Hom ‘ 𝑂 ) )
Assertion oppgoppchom ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( 𝑌 𝐽 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mndtccat.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2 mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 oppgoppchom.d ⊢ ( 𝜑 → 𝐷 = ( MndToCat ‘ ( oppg ‘ 𝑀 ) ) )
4 oppgoppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5 oppgoppchom.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
6 oppgoppchom.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑂 ) )
7 oppgoppchom.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐷 ) )
8 oppgoppchom.j ⊢ ( 𝜑 → 𝐽 = ( Hom ‘ 𝑂 ) )
9 eqid ⊢ ( oppg ‘ 𝑀 ) = ( oppg ‘ 𝑀 )
10 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
11 9 10 oppgbas ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ ( oppg ‘ 𝑀 ) )
12 11 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑀 ) = ( Base ‘ ( oppg ‘ 𝑀 ) ) )
13 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14 4 13 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
15 14 eqcomi ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝐶 )
16 15 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝐶 ) )
17 eqidd ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
18 1 2 16 6 6 17 mndtchom ⊢ ( 𝜑 → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑌 ) = ( Base ‘ 𝑀 ) )
19 9 oppgmnd ⊢ ( 𝑀 ∈ Mnd → ( oppg ‘ 𝑀 ) ∈ Mnd )
20 2 19 syl ⊢ ( 𝜑 → ( oppg ‘ 𝑀 ) ∈ Mnd )
21 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
22 3 20 21 5 5 7 mndtchom ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( Base ‘ ( oppg ‘ 𝑀 ) ) )
23 12 18 22 3eqtr4rd ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( 𝑌 ( Hom ‘ 𝐶 ) 𝑌 ) )
24 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
25 24 4 oppchom ⊢ ( 𝑌 ( Hom ‘ 𝑂 ) 𝑌 ) = ( 𝑌 ( Hom ‘ 𝐶 ) 𝑌 )
26 23 25 eqtr4di ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( 𝑌 ( Hom ‘ 𝑂 ) 𝑌 ) )
27 8 oveqd ⊢ ( 𝜑 → ( 𝑌 𝐽 𝑌 ) = ( 𝑌 ( Hom ‘ 𝑂 ) 𝑌 ) )
28 26 27 eqtr4d ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( 𝑌 𝐽 𝑌 ) )