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 ‘ 𝑂 ) ‘ 𝑌 ) )