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	$$⊢\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$$
	oppgoppchom.h	$$⊢\phi \to H=\mathrm{Hom}\left(D\right)$$
	oppgoppchom.j	$$⊢\phi \to J=\mathrm{Hom}\left(O\right)$$
Assertion	oppgoppchom	$$⊢\phi \to XHX=YJY$$

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		oppgoppchom.h	$$⊢\phi \to H=\mathrm{Hom}\left(D\right)$$
8		oppgoppchom.j	$$⊢\phi \to J=\mathrm{Hom}\left(O\right)$$
9		eqid	$$⊢{opp}_{𝑔}\left(M\right)={opp}_{𝑔}\left(M\right)$$
10		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
11	9 10	oppgbas	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{{opp}_{𝑔}\left(M\right)}$$
12	11	a1i	$$⊢\phi \to {\mathrm{Base}}_M={\mathrm{Base}}_{{opp}_{𝑔}\left(M\right)}$$
13		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
14	4 13	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
15	14	eqcomi	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_C$$
16	15	a1i	$$⊢\phi \to {\mathrm{Base}}_O={\mathrm{Base}}_C$$
17		eqidd	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
18	1 2 16 6 6 17	mndtchom	$$⊢\phi \to Y\mathrm{Hom}\left(C\right)Y={\mathrm{Base}}_M$$
19	9	oppgmnd	$$⊢M\in \mathrm{Mnd}\to {opp}_{𝑔}\left(M\right)\in \mathrm{Mnd}$$
20	2 19	syl	$$⊢\phi \to {opp}_{𝑔}\left(M\right)\in \mathrm{Mnd}$$
21		eqidd	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_D$$
22	3 20 21 5 5 7	mndtchom	$$⊢\phi \to XHX={\mathrm{Base}}_{{opp}_{𝑔}\left(M\right)}$$
23	12 18 22	3eqtr4rd	$$⊢\phi \to XHX=Y\mathrm{Hom}\left(C\right)Y$$
24		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
25	24 4	oppchom	$$⊢Y\mathrm{Hom}\left(O\right)Y=Y\mathrm{Hom}\left(C\right)Y$$
26	23 25	eqtr4di	$$⊢\phi \to XHX=Y\mathrm{Hom}\left(O\right)Y$$
27	8	oveqd	$$⊢\phi \to YJY=Y\mathrm{Hom}\left(O\right)Y$$
28	26 27	eqtr4d	$$⊢\phi \to XHX=YJY$$