Theorem sgrpssmgm

Description: The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Assertion	sgrpssmgm	$$⊢\mathrm{Smgrp}\subset \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		sgrpmgm	$$⊢x\in \mathrm{Smgrp}\to x\in \mathrm{Mgm}$$
2	1	ssriv	$$⊢\mathrm{Smgrp}\subseteq \mathrm{Mgm}$$
3		mgmnsgrpex	$$⊢\exists x\in \mathrm{Mgm}x\notin \mathrm{Smgrp}$$
4		ssexnelpss	$$⊢\left(\mathrm{Smgrp}\subseteq \mathrm{Mgm}\wedge \exists x\in \mathrm{Mgm}x\notin \mathrm{Smgrp}\right)\to \mathrm{Smgrp}\subset \mathrm{Mgm}$$
5	2 3 4	mp2an	$$⊢\mathrm{Smgrp}\subset \mathrm{Mgm}$$