Metamath Proof Explorer

Theorem mgmnsgrpex

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

Ref Expression
Assertion mgmnsgrpex 
|- E. m e. Mgm m e/ Smgrp

Proof

Step Hyp Ref Expression
1 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
2 c0ex 
 |-  0 e. _V
3 1ex 
 |-  1 e. _V
4 2 3 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
5 eqid 
 |-  { 0 , 1 } = { 0 , 1 }
6 prex 
 |-  { 0 , 1 } e. _V
7 eqeq1 
 |-  ( x = u -> ( x = 0 <-> u = 0 ) )
8 7 anbi1d 
 |-  ( x = u -> ( ( x = 0 /\ y = 0 ) <-> ( u = 0 /\ y = 0 ) ) )
9 8 ifbid 
 |-  ( x = u -> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) = if ( ( u = 0 /\ y = 0 ) , 1 , 0 ) )
10 eqeq1 
 |-  ( y = v -> ( y = 0 <-> v = 0 ) )
11 10 anbi2d 
 |-  ( y = v -> ( ( u = 0 /\ y = 0 ) <-> ( u = 0 /\ v = 0 ) ) )
12 11 ifbid 
 |-  ( y = v -> if ( ( u = 0 /\ y = 0 ) , 1 , 0 ) = if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) )
13 9 12 cbvmpov 
 |-  ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) = ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) )
14 13 opeq2i 
 |-  <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. = <. ( +g ` ndx ) , ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) ) >.
15 14 preq2i 
 |-  { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) ) >. }
16 15 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 /\ y = 0 ) , 1 , 0 ) ) >. } ) )
17 6 16 ax-mp 
 |-  { 0 , 1 } = ( Base ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } )
18 17 eqcomi 
 |-  ( Base ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } ) = { 0 , 1 }
19 6 6 mpoex 
 |-  ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) ) e. _V
20 15 grpplusg 
 |-  ( ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) ) e. _V -> ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) ) = ( +g ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } ) )
21 19 20 ax-mp 
 |-  ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) ) = ( +g ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } )
22 21 eqcomi 
 |-  ( +g ` { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } ) = ( u e. { 0 , 1 } , v e. { 0 , 1 } |-> if ( ( u = 0 /\ v = 0 ) , 1 , 0 ) )
23 5 18 22 mgm2nsgrplem1 
 |-  ( ( 0 e. _V /\ 1 e. _V ) -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e. Mgm )
24 4 23 mp1i 
 |-  ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e. Mgm )
25 neleq1 
 |-  ( m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } -> ( m e/ Smgrp <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) )
26 25 adantl 
 |-  ( ( ( # ` { 0 , 1 } ) = 2 /\ m = { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } ) -> ( m e/ Smgrp <-> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp ) )
27 5 18 22 mgm2nsgrplem4 
 |-  ( ( # ` { 0 , 1 } ) = 2 -> { <. ( Base ` ndx ) , { 0 , 1 } >. , <. ( +g ` ndx ) , ( x e. { 0 , 1 } , y e. { 0 , 1 } |-> if ( ( x = 0 /\ y = 0 ) , 1 , 0 ) ) >. } e/ Smgrp )
28 24 26 27 rspcedvd 
 |-  ( ( # ` { 0 , 1 } ) = 2 -> E. m e. Mgm m e/ Smgrp )
29 1 28 ax-mp 
 |-  E. m e. Mgm m e/ Smgrp