Metamath Proof Explorer

Theorem subm0cl

Description: Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis subm0cl.z 
|- .0. = ( 0g ` M )
Assertion subm0cl 
|- ( S e. ( SubMnd ` M ) -> .0. e. S )

Proof

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