Theorem submbas

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

	Ref	Expression
Hypothesis	submmnd.h	⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
Assertion	submbas	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		submmnd.h	⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3	2	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
4	1 2	ressbas2	⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) )
5	3 4	syl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) )