Theorem mndsgrp

Description: A monoid is a semigroup. (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020) (Proof shortened by AV, 6-Feb-2020)

	Ref	Expression
Assertion	mndsgrp	Could not format assertion : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2		eqid	$$⊢{+}_G={+}_G$$
3	1 2	ismnddef	Could not format ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. ( Base ` G ) A. x e. ( Base ` G ) ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) ) : No typesetting found for |- ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. ( Base ` G ) A. x e. ( Base ` G ) ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) ) with typecode |-
4	3	simplbi	Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |-