Metamath Proof Explorer


Theorem mgm2nsgrp

Description: A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020)

Ref Expression
Hypotheses mgm2nsgrp.s S=AB
mgm2nsgrp.b BaseM=S
mgm2nsgrp.o +M=xS,ySifx=Ay=ABA
Assertion mgm2nsgrp Could not format assertion : No typesetting found for |- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s S=AB
2 mgm2nsgrp.b BaseM=S
3 mgm2nsgrp.o +M=xS,ySifx=Ay=ABA
4 1 hashprdifel S=2ASBSAB
5 1 2 3 mgm2nsgrplem1 ASBSMMgm
6 5 3adant3 ASBSABMMgm
7 4 6 syl S=2MMgm
8 1 2 3 mgm2nsgrplem4 Could not format ( ( # ` S ) = 2 -> M e/ Smgrp ) : No typesetting found for |- ( ( # ` S ) = 2 -> M e/ Smgrp ) with typecode |-
9 7 8 jca Could not format ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) ) : No typesetting found for |- ( ( # ` S ) = 2 -> ( M e. Mgm /\ M e/ Smgrp ) ) with typecode |-