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	|- ( ph -> C = ( MndToCat ` M ) )
	mndtccat.m	|- ( ph -> M e. Mnd )
	oppgoppchom.d	|- ( ph -> D = ( MndToCat ` ( oppG ` M ) ) )
	oppgoppchom.o	|- O = ( oppCat ` C )
	oppgoppchom.x	|- ( ph -> X e. ( Base ` D ) )
	oppgoppchom.y	|- ( ph -> Y e. ( Base ` O ) )
Assertion	oppgoppcid	|- ( ph -> ( ( Id ` D ) ` X ) = ( ( Id ` O ) ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		mndtccat.c	|- ( ph -> C = ( MndToCat ` M ) )
2		mndtccat.m	|- ( ph -> M e. Mnd )
3		oppgoppchom.d	|- ( ph -> D = ( MndToCat ` ( oppG ` M ) ) )
4		oppgoppchom.o	|- O = ( oppCat ` C )
5		oppgoppchom.x	|- ( ph -> X e. ( Base ` D ) )
6		oppgoppchom.y	|- ( ph -> Y e. ( Base ` O ) )
7		eqid	|- ( oppG ` M ) = ( oppG ` M )
8		eqid	|- ( 0g ` M ) = ( 0g ` M )
9	7 8	oppgid	|- ( 0g ` M ) = ( 0g ` ( oppG ` M ) )
10	9	a1i	|- ( ph -> ( 0g ` M ) = ( 0g ` ( oppG ` 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	|- ( ph -> ( Base ` O ) = ( Base ` C ) )
15	1 2	mndtccat	|- ( ph -> C e. Cat )
16		eqid	|- ( Id ` C ) = ( Id ` C )
17	4 16	oppcid	|- ( C e. Cat -> ( Id ` O ) = ( Id ` C ) )
18	15 17	syl	|- ( ph -> ( Id ` O ) = ( Id ` C ) )
19	1 2 14 6 18	mndtcid	|- ( ph -> ( ( Id ` O ) ` Y ) = ( 0g ` M ) )
20	7	oppgmnd	|- ( M e. Mnd -> ( oppG ` M ) e. Mnd )
21	2 20	syl	|- ( ph -> ( oppG ` M ) e. Mnd )
22		eqidd	|- ( ph -> ( Base ` D ) = ( Base ` D ) )
23		eqidd	|- ( ph -> ( Id ` D ) = ( Id ` D ) )
24	3 21 22 5 23	mndtcid	|- ( ph -> ( ( Id ` D ) ` X ) = ( 0g ` ( oppG ` M ) ) )
25	10 19 24	3eqtr4rd	|- ( ph -> ( ( Id ` D ) ` X ) = ( ( Id ` O ) ` Y ) )