Metamath Proof Explorer

Theorem mndtchom

Description: The only hom-set of the category built from a monoid is the base set of the monoid. (Contributed by Zhi Wang, 22-Sep-2024)

Ref Expression
Hypotheses mndtcbas.c 
|- ( ph -> C = ( MndToCat ` M ) )
mndtcbas.m 
|- ( ph -> M e. Mnd )
mndtcbas.b 
|- ( ph -> B = ( Base ` C ) )
mndtchom.x 
|- ( ph -> X e. B )
mndtchom.y 
|- ( ph -> Y e. B )
mndtchom.h 
|- ( ph -> H = ( Hom ` C ) )
Assertion mndtchom 
|- ( ph -> ( X H Y ) = ( Base ` M ) )

Proof

Step Hyp Ref Expression
1 mndtcbas.c 
 |-  ( ph -> C = ( MndToCat ` M ) )
2 mndtcbas.m 
 |-  ( ph -> M e. Mnd )
3 mndtcbas.b 
 |-  ( ph -> B = ( Base ` C ) )
4 mndtchom.x 
 |-  ( ph -> X e. B )
5 mndtchom.y 
 |-  ( ph -> Y e. B )
6 mndtchom.h 
 |-  ( ph -> H = ( Hom ` C ) )
7 1 2 mndtcval 
 |-  ( ph -> C = { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } )
8 catstr 
 |-  { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } Struct <. 1 , ; 1 5 >.
9 homid 
 |-  Hom = Slot ( Hom ` ndx )
10 snsstp2 
 |-  { <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. } C_ { <. ( Base ` ndx ) , { M } >. , <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. , <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. }
11 snex 
 |-  { <. M , M , ( Base ` M ) >. } e. _V
12 11 a1i 
 |-  ( ph -> { <. M , M , ( Base ` M ) >. } e. _V )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 7 8 9 10 12 13 strfv3 
 |-  ( ph -> ( Hom ` C ) = { <. M , M , ( Base ` M ) >. } )
15 6 14 eqtrd 
 |-  ( ph -> H = { <. M , M , ( Base ` M ) >. } )
16 1 2 3 4 mndtcob 
 |-  ( ph -> X = M )
17 1 2 3 5 mndtcob 
 |-  ( ph -> Y = M )
18 15 16 17 oveq123d 
 |-  ( ph -> ( X H Y ) = ( M { <. M , M , ( Base ` M ) >. } M ) )
19 df-ot 
 |-  <. M , M , ( Base ` M ) >. = <. <. M , M >. , ( Base ` M ) >.
20 19 sneqi 
 |-  { <. M , M , ( Base ` M ) >. } = { <. <. M , M >. , ( Base ` M ) >. }
21 20 oveqi 
 |-  ( M { <. M , M , ( Base ` M ) >. } M ) = ( M { <. <. M , M >. , ( Base ` M ) >. } M )
22 df-ov 
 |-  ( M { <. <. M , M >. , ( Base ` M ) >. } M ) = ( { <. <. M , M >. , ( Base ` M ) >. } ` <. M , M >. )
23 opex 
 |-  <. M , M >. e. _V
24 fvex 
 |-  ( Base ` M ) e. _V
25 23 24 fvsn 
 |-  ( { <. <. M , M >. , ( Base ` M ) >. } ` <. M , M >. ) = ( Base ` M )
26 21 22 25 3eqtri 
 |-  ( M { <. M , M , ( Base ` M ) >. } M ) = ( Base ` M )
27 18 26 eqtrdi 
 |-  ( ph -> ( X H Y ) = ( Base ` M ) )