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

Metamath Proof Explorer

Theorem subgsubm

Description: A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion subgsubm 
|- ( S e. ( SubGrp ` G ) -> S e. ( SubMnd ` G ) )

Proof

Step Hyp Ref Expression
1 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
2 eqid 
 |-  ( invg ` G ) = ( invg ` G )
3 2 issubg3 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S e. ( SubMnd ` G ) /\ A. x e. S ( ( invg ` G ) ` x ) e. S ) ) )
4 1 3 syl 
 |-  ( S e. ( SubGrp ` G ) -> ( S e. ( SubGrp ` G ) <-> ( S e. ( SubMnd ` G ) /\ A. x e. S ( ( invg ` G ) ` x ) e. S ) ) )
5 4 ibi 
 |-  ( S e. ( SubGrp ` G ) -> ( S e. ( SubMnd ` G ) /\ A. x e. S ( ( invg ` G ) ` x ) e. S ) )
6 5 simpld 
 |-  ( S e. ( SubGrp ` G ) -> S e. ( SubMnd ` G ) )