Metamath Proof Explorer

Theorem sgrpnmndex

Description: There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020)

Ref Expression
Assertion sgrpnmndex 
|- E. m e. Smgrp m e/ Mnd

Proof

Step Hyp Ref Expression
1 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
2 eqid 
 |-  { 0 , 1 } = { 0 , 1 }
3 prex 
 |-  { 0 , 1 } e. _V
4 eqeq1 
 |-  ( x = u -> ( x = 0 <-> u = 0 ) )
5 4 ifbid 
 |-  ( x = u -> if ( x = 0 , 0 , 1 ) = if ( u = 0 , 0 , 1 ) )
6 eqidd 
 |-  ( y = v -> if ( u = 0 , 0 , 1 ) = if ( u = 0 , 0 , 1 ) )
7 5 6 cbvmpov 
 |-  ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) = ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) )
8 7 opeq2i 
 |-  <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. = <. ( +g ` ndx ) , ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) ) >.
9 8 preq2i 
 |-  { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) ) >. }
10 9 grpbase 
 |-  ( { 0 , 1 } e. _V -> { 0 , 1 } = ( Base ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } ) )
11 3 10 ax-mp 
 |-  { 0 , 1 } = ( Base ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } )
12 11 eqcomi 
 |-  ( Base ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } ) = { 0 , 1 }
13 3 3 mpoex 
 |-  ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) ) e. _V
14 9 grpplusg 
 |-  ( ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) ) e. _V -> ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) ) = ( +g ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } ) )
15 13 14 ax-mp 
 |-  ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) ) = ( +g ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } )
16 15 eqcomi 
 |-  ( +g ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } ) = ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( u = 0 , 0 , 1 ) )
17 2 12 16 sgrp2nmndlem4 
 |-  ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } e. Smgrp )
18 neleq1 
 |-  ( m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } -> ( m e/ Mnd <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } e/ Mnd ) )
19 18 adantl 
 |-  ( ( ( # ` { 0 , 1 } ) = 2 /\ m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } ) -> ( m e/ Mnd <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } e/ Mnd ) )
20 2 12 16 sgrp2nmndlem5 
 |-  ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( x = 0 , 0 , 1 ) ) >. } e/ Mnd )
21 17 19 20 rspcedvd 
 |-  ( ( # ` { 0 , 1 } ) = 2 -> E. m e. Smgrp m e/ Mnd )
22 1 21 ax-mp 
 |-  E. m e. Smgrp m e/ Mnd