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 
|- B = ( Base ` M )
Assertion submss 
|- ( S e. ( SubMnd ` M ) -> S C_ B )

Proof

Step Hyp Ref Expression
1 submss.b 
 |-  B = ( Base ` M )
2 submrcl 
 |-  ( S e. ( SubMnd ` M ) -> M e. Mnd )
3 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
4 eqid 
 |-  ( M |`s S ) = ( M |`s S )
5 1 3 4 issubm2 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ ( 0g ` M ) e. S /\ ( M |`s S ) e. Mnd ) ) )
6 2 5 syl 
 |-  ( S e. ( SubMnd ` M ) -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ ( 0g ` M ) e. S /\ ( M |`s S ) e. Mnd ) ) )
7 6 ibi 
 |-  ( S e. ( SubMnd ` M ) -> ( S C_ B /\ ( 0g ` M ) e. S /\ ( M |`s S ) e. Mnd ) )
8 7 simp1d 
 |-  ( S e. ( SubMnd ` M ) -> S C_ B )