Theorem submid

Description: Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Hypothesis	submss.b	|- B = ( Base ` M )
Assertion	submid	|- ( M e. Mnd -> B e. ( SubMnd ` M ) )

Proof

Step	Hyp	Ref	Expression
1		submss.b	|- B = ( Base ` M )
2		ssidd	|- ( M e. Mnd -> B C_ B )
3		eqid	|- ( 0g ` M ) = ( 0g ` M )
4	1 3	mndidcl	|- ( M e. Mnd -> ( 0g ` M ) e. B )
5	1	ressid	|- ( M e. Mnd -> ( M |`s B ) = M )
6		id	|- ( M e. Mnd -> M e. Mnd )
7	5 6	eqeltrd	|- ( M e. Mnd -> ( M |`s B ) e. Mnd )
8		eqid	|- ( M |`s B ) = ( M |`s B )
9	1 3 8	issubm2	|- ( M e. Mnd -> ( B e. ( SubMnd ` M ) <-> ( B C_ B /\ ( 0g ` M ) e. B /\ ( M |`s B ) e. Mnd ) ) )
10	2 4 7 9	mpbir3and	|- ( M e. Mnd -> B e. ( SubMnd ` M ) )