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	$⊢ φ \to C = MndToCat (M)$
	mndtccat.m	$⊢ φ \to M \in Mnd$
	oppgoppchom.d	$⊢ φ \to D = MndToCat ({opp}_{𝑔} (M))$
	oppgoppchom.o	$⊢ O = oppCat (C)$
	oppgoppchom.x	$⊢ φ \to X \in {Base}_{D}$
	oppgoppchom.y	$⊢ φ \to Y \in {Base}_{O}$
Assertion	oppgoppcid	$⊢ φ \to Id (D) (X) = Id (O) (Y)$

Proof

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

Metamath Proof Explorer

Theorem oppgoppcid

Proof