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	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
	mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
	oppgoppchom.d	$$⊢\phi \to D=\mathrm{MndToCat}\left({opp}_{𝑔}\left(M\right)\right)$$
	oppgoppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppgoppchom.x	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
	oppgoppchom.y	$$⊢\phi \to Y\in {\mathrm{Base}}_O$$
Assertion	oppgoppcid	$$⊢\phi \to \mathrm{Id}\left(D\right)\left(X\right)=\mathrm{Id}\left(O\right)\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	$$⊢\phi \to C=\mathrm{MndToCat}\left(M\right)$$
2		mndtccat.m	$$⊢\phi \to M\in \mathrm{Mnd}$$
3		oppgoppchom.d	$$⊢\phi \to D=\mathrm{MndToCat}\left({opp}_{𝑔}\left(M\right)\right)$$
4		oppgoppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
5		oppgoppchom.x	$$⊢\phi \to X\in {\mathrm{Base}}_D$$
6		oppgoppchom.y	$$⊢\phi \to Y\in {\mathrm{Base}}_O$$
7		eqid	$$⊢{opp}_{𝑔}\left(M\right)={opp}_{𝑔}\left(M\right)$$
8		eqid	$$⊢0_M=0_M$$
9	7 8	oppgid	$$⊢0_M=0_{{opp}_{𝑔}\left(M\right)}$$
10	9	a1i	$$⊢\phi \to 0_M=0_{{opp}_{𝑔}\left(M\right)}$$
11		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
12	4 11	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
13	12	eqcomi	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_C$$
14	13	a1i	$$⊢\phi \to {\mathrm{Base}}_O={\mathrm{Base}}_C$$
15	1 2	mndtccat	$$⊢\phi \to C\in \mathrm{Cat}$$
16		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
17	4 16	oppcid	$$⊢C\in \mathrm{Cat}\to \mathrm{Id}\left(O\right)=\mathrm{Id}\left(C\right)$$
18	15 17	syl	$$⊢\phi \to \mathrm{Id}\left(O\right)=\mathrm{Id}\left(C\right)$$
19	1 2 14 6 18	mndtcid	$$⊢\phi \to \mathrm{Id}\left(O\right)\left(Y\right)=0_M$$
20	7	oppgmnd	$$⊢M\in \mathrm{Mnd}\to {opp}_{𝑔}\left(M\right)\in \mathrm{Mnd}$$
21	2 20	syl	$$⊢\phi \to {opp}_{𝑔}\left(M\right)\in \mathrm{Mnd}$$
22		eqidd	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_D$$
23		eqidd	$$⊢\phi \to \mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
24	3 21 22 5 23	mndtcid	$$⊢\phi \to \mathrm{Id}\left(D\right)\left(X\right)=0_{{opp}_{𝑔}\left(M\right)}$$
25	10 19 24	3eqtr4rd	$$⊢\phi \to \mathrm{Id}\left(D\right)\left(X\right)=\mathrm{Id}\left(O\right)\left(Y\right)$$