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 ) )

Metamath Proof Explorer

Theorem oppgoppcid

Proof