This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem submbas

Description: The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015)

		Ref	Expression
	Hypothesis	submmnd.h	$⊢ H = M ↾_{𝑠} S$
	Assertion	submbas	$⊢ S \in SubMnd (M) \to S = {Base}_{H}$

Step	Hyp	Ref	Expression
1		submmnd.h	$⊢ H = M ↾_{𝑠} S$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3	2	submss	$⊢ S \in SubMnd (M) \to S \subseteq {Base}_{M}$
4	1 2	ressbas2	$⊢ S \subseteq {Base}_{M} \to S = {Base}_{H}$
5	3 4	syl	$⊢ S \in SubMnd (M) \to S = {Base}_{H}$