Metamath Proof Explorer

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	\|- Mnd C. Smgrp

Proof


 |-  ( x e. Mnd -> x e. Smgrp )
 |-  Mnd C_ Smgrp
 |-  E. x e. Smgrp x e/ Mnd
 |-  ( ( Mnd C_ Smgrp /\ E. x e. Smgrp x e/ Mnd ) -> Mnd C. Smgrp )
 |-  Mnd C. Smgrp

Step	Hyp	Ref	Expression
1		mndsgrp	\|- ( x e. Mnd -> x e. Smgrp )
2	1	ssriv	\|- Mnd C_ Smgrp
3		sgrpnmndex	\|- E. x e. Smgrp x e/ Mnd
4		ssexnelpss	\|- ( ( Mnd C_ Smgrp /\ E. x e. Smgrp x e/ Mnd ) -> Mnd C. Smgrp )
5	2 3 4	mp2an	\|- Mnd C. Smgrp