submss

Description: Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Hypothesis	submss.b	$⊢ B = {Base}_{M}$
	Assertion	submss	$⊢ S \in SubMnd (M) \to S \subseteq B$

Step	Hyp	Ref	Expression
1		submss.b	$⊢ B = {Base}_{M}$
2		submrcl	$⊢ S \in SubMnd (M) \to M \in Mnd$
3		eqid	$⊢ 0_{M} = 0_{M}$
4		eqid	$⊢ M ↾_{𝑠} S = M ↾_{𝑠} S$
5	1 3 4	issubm2	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land 0_{M} \in S \land M ↾_{𝑠} S \in Mnd))$
6	2 5	syl	$⊢ S \in SubMnd (M) \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land 0_{M} \in S \land M ↾_{𝑠} S \in Mnd))$
7	6	ibi	$⊢ S \in SubMnd (M) \to (S \subseteq B \land 0_{M} \in S \land M ↾_{𝑠} S \in Mnd)$
8	7	simp1d	$⊢ S \in SubMnd (M) \to S \subseteq B$

Metamath Proof Explorer