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	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( 𝑌 𝐽 𝑌 ) )