Metamath Proof Explorer

Theorem submgmmgm

Description: Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis submgmmgm.h 
|- H = ( M |`s S )
Assertion submgmmgm 
|- ( S e. ( SubMgm ` M ) -> H e. Mgm )

Proof

Step Hyp Ref Expression
1 submgmmgm.h 
 |-  H = ( M |`s S )
2 submgmrcl 
 |-  ( S e. ( SubMgm ` M ) -> M e. Mgm )
3 eqid 
 |-  ( Base ` M ) = ( Base ` M )
4 3 1 issubmgm2 
 |-  ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ ( Base ` M ) /\ H e. Mgm ) ) )
5 2 4 syl 
 |-  ( S e. ( SubMgm ` M ) -> ( S e. ( SubMgm ` M ) <-> ( S C_ ( Base ` M ) /\ H e. Mgm ) ) )
6 5 ibi 
 |-  ( S e. ( SubMgm ` M ) -> ( S C_ ( Base ` M ) /\ H e. Mgm ) )
7 6 simprd 
 |-  ( S e. ( SubMgm ` M ) -> H e. Mgm )