Theorem sgrp0

Description: Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Assertion	sgrp0	Could not format assertion : No typesetting found for |- ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgm0	$$⊢\left(M\in V\wedge {\mathrm{Base}}_M=\varnothing \right)\to M\in \mathrm{Mgm}$$
2		rzal	$$⊢{\mathrm{Base}}_M=\varnothing \to \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)$$
3	2	adantl	$$⊢\left(M\in V\wedge {\mathrm{Base}}_M=\varnothing \right)\to \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_M\forall z\in {\mathrm{Base}}_M\left(x{+}_{M}y\right){+}_{M}z=x{+}_M\left(y{+}_{M}z\right)$$
4		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
5		eqid	$$⊢{+}_M={+}_M$$
6	4 5	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. ( Base ` M ) A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. ( Base ` M ) A. y e. ( Base ` M ) A. z e. ( Base ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) with typecode |-
7	1 3 6	sylanbrc	Could not format ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Smgrp ) : No typesetting found for |- ( ( M e. V /\ ( Base ` M ) = (/) ) -> M e. Smgrp ) with typecode |-