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

Metamath Proof Explorer

Theorem oppgoppcid

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

Ref Expression
Hypotheses mndtccat.c ⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
mndtccat.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
oppgoppchom.d ⊢ ( 𝜑 → 𝐷 = ( MndToCat ‘ ( oppg ‘ 𝑀 ) ) )
oppgoppchom.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppgoppchom.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
oppgoppchom.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑂 ) )
Assertion oppgoppcid ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑌 ) )

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 eqid ⊢ ( oppg ‘ 𝑀 ) = ( oppg ‘ 𝑀 )
8 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
9 7 8 oppgid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ ( oppg ‘ 𝑀 ) )
10 9 a1i ⊢ ( 𝜑 → ( 0g ‘ 𝑀 ) = ( 0g ‘ ( oppg ‘ 𝑀 ) ) )
11 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12 4 11 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
13 12 eqcomi ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝐶 )
14 13 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝐶 ) )
15 1 2 mndtccat ⊢ ( 𝜑 → 𝐶 ∈ Cat )
16 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
17 4 16 oppcid ⊢ ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
18 15 17 syl ⊢ ( 𝜑 → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
19 1 2 14 6 18 mndtcid ⊢ ( 𝜑 → ( ( Id ‘ 𝑂 ) ‘ 𝑌 ) = ( 0g ‘ 𝑀 ) )
20 7 oppgmnd ⊢ ( 𝑀 ∈ Mnd → ( oppg ‘ 𝑀 ) ∈ Mnd )
21 2 20 syl ⊢ ( 𝜑 → ( oppg ‘ 𝑀 ) ∈ Mnd )
22 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
23 eqidd ⊢ ( 𝜑 → ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 ) )
24 3 21 22 5 23 mndtcid ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) = ( 0g ‘ ( oppg ‘ 𝑀 ) ) )
25 10 19 24 3eqtr4rd ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑌 ) )