Metamath Proof Explorer


Theorem submss

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

Ref Expression
Hypothesis submss.b 𝐵 = ( Base ‘ 𝑀 )
Assertion submss ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆𝐵 )

Proof

Step Hyp Ref Expression
1 submss.b 𝐵 = ( Base ‘ 𝑀 )
2 submrcl ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )
3 eqid ( 0g𝑀 ) = ( 0g𝑀 )
4 eqid ( 𝑀s 𝑆 ) = ( 𝑀s 𝑆 )
5 1 3 4 issubm2 ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆𝐵 ∧ ( 0g𝑀 ) ∈ 𝑆 ∧ ( 𝑀s 𝑆 ) ∈ Mnd ) ) )
6 2 5 syl ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆𝐵 ∧ ( 0g𝑀 ) ∈ 𝑆 ∧ ( 𝑀s 𝑆 ) ∈ Mnd ) ) )
7 6 ibi ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑆𝐵 ∧ ( 0g𝑀 ) ∈ 𝑆 ∧ ( 𝑀s 𝑆 ) ∈ Mnd ) )
8 7 simp1d ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆𝐵 )