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 φ 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
Assertion oppgoppcid φ Id D X = Id O 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 eqid opp 𝑔 M = opp 𝑔 M
8 eqid 0 M = 0 M
9 7 8 oppgid 0 M = 0 opp 𝑔 M
10 9 a1i φ 0 M = 0 opp 𝑔 M
11 eqid Base C = Base C
12 4 11 oppcbas Base C = Base O
13 12 eqcomi Base O = Base C
14 13 a1i φ Base O = Base C
15 1 2 mndtccat φ C Cat
16 eqid Id C = Id C
17 4 16 oppcid C Cat Id O = Id C
18 15 17 syl φ Id O = Id C
19 1 2 14 6 18 mndtcid φ Id O Y = 0 M
20 7 oppgmnd M Mnd opp 𝑔 M Mnd
21 2 20 syl φ opp 𝑔 M Mnd
22 eqidd φ Base D = Base D
23 eqidd φ Id D = Id D
24 3 21 22 5 23 mndtcid φ Id D X = 0 opp 𝑔 M
25 10 19 24 3eqtr4rd φ Id D X = Id O Y