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 \in Mnd \to B \in SubMnd (M)$

Step	Hyp	Ref	Expression
1		submss.b	$⊢ B = {Base}_{M}$
2		ssidd	$⊢ M \in Mnd \to B \subseteq B$
3		eqid	$⊢ 0_{M} = 0_{M}$
4	1 3	mndidcl	$⊢ M \in Mnd \to 0_{M} \in B$
5	1	ressid	$⊢ M \in Mnd \to M ↾_{𝑠} B = M$
6		id	$⊢ M \in Mnd \to M \in Mnd$
7	5 6	eqeltrd	$⊢ M \in Mnd \to M ↾_{𝑠} B \in Mnd$
8		eqid	$⊢ M ↾_{𝑠} B = M ↾_{𝑠} B$
9	1 3 8	issubm2	$⊢ M \in Mnd \to (B \in SubMnd (M) \leftrightarrow (B \subseteq B \land 0_{M} \in B \land M ↾_{𝑠} B \in Mnd))$
10	2 4 7 9	mpbir3and	$⊢ M \in Mnd \to B \in SubMnd (M)$

Metamath Proof Explorer