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

Metamath Proof Explorer

Theorem submid

Description: Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Hypothesis submss.b 
|- B = ( Base ` M )
Assertion submid 
|- ( M e. Mnd -> B e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 submss.b 
 |-  B = ( Base ` M )
2 ssidd 
 |-  ( M e. Mnd -> B C_ B )
3 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
4 1 3 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. B )
5 1 ressid 
 |-  ( M e. Mnd -> ( M |`s B ) = M )
6 id 
 |-  ( M e. Mnd -> M e. Mnd )
7 5 6 eqeltrd 
 |-  ( M e. Mnd -> ( M |`s B ) e. Mnd )
8 eqid 
 |-  ( M |`s B ) = ( M |`s B )
9 1 3 8 issubm2 
 |-  ( M e. Mnd -> ( B e. ( SubMnd ` M ) <-> ( B C_ B /\ ( 0g ` M ) e. B /\ ( M |`s B ) e. Mnd ) ) )
10 2 4 7 9 mpbir3and 
 |-  ( M e. Mnd -> B e. ( SubMnd ` M ) )