Theorem mndsssgrp

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

	Ref	Expression
Assertion	mndsssgrp	$$⊢\mathrm{Mnd}\subset \mathrm{Smgrp}$$

Proof

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