Metamath Proof Explorer

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 
|- ( 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 ) )
oppgoppchom.h 
|- ( ph -> H = ( Hom ` D ) )
oppgoppchom.j 
|- ( ph -> J = ( Hom ` O ) )
Assertion oppgoppchom 
|- ( ph -> ( X H X ) = ( Y J 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 oppgoppchom.h 
 |-  ( ph -> H = ( Hom ` D ) )
8 oppgoppchom.j 
 |-  ( ph -> J = ( Hom ` O ) )
9 eqid 
 |-  ( oppG ` M ) = ( oppG ` M )
10 eqid 
 |-  ( Base ` M ) = ( Base ` M )
11 9 10 oppgbas 
 |-  ( Base ` M ) = ( Base ` ( oppG ` M ) )
12 11 a1i 
 |-  ( ph -> ( Base ` M ) = ( Base ` ( oppG ` M ) ) )
13 eqid 
 |-  ( Base ` C ) = ( Base ` C )
14 4 13 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
15 14 eqcomi 
 |-  ( Base ` O ) = ( Base ` C )
16 15 a1i 
 |-  ( ph -> ( Base ` O ) = ( Base ` C ) )
17 eqidd 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` C ) )
18 1 2 16 6 6 17 mndtchom 
 |-  ( ph -> ( Y ( Hom ` C ) Y ) = ( Base ` M ) )
19 9 oppgmnd 
 |-  ( M e. Mnd -> ( oppG ` M ) e. Mnd )
20 2 19 syl 
 |-  ( ph -> ( oppG ` M ) e. Mnd )
21 eqidd 
 |-  ( ph -> ( Base ` D ) = ( Base ` D ) )
22 3 20 21 5 5 7 mndtchom 
 |-  ( ph -> ( X H X ) = ( Base ` ( oppG ` M ) ) )
23 12 18 22 3eqtr4rd 
 |-  ( ph -> ( X H X ) = ( Y ( Hom ` C ) Y ) )
24 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
25 24 4 oppchom 
 |-  ( Y ( Hom ` O ) Y ) = ( Y ( Hom ` C ) Y )
26 23 25 eqtr4di 
 |-  ( ph -> ( X H X ) = ( Y ( Hom ` O ) Y ) )
27 8 oveqd 
 |-  ( ph -> ( Y J Y ) = ( Y ( Hom ` O ) Y ) )
28 26 27 eqtr4d 
 |-  ( ph -> ( X H X ) = ( Y J Y ) )