Metamath Proof Explorer

Theorem submgmrcl

Description: Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020)

Ref Expression
Assertion submgmrcl 
|- ( S e. ( SubMgm ` M ) -> M e. Mgm )

Proof

Step Hyp Ref Expression
1 df-submgm 
 |-  SubMgm = ( s e. Mgm |-> { t e. ~P ( Base ` s ) | A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t } )
2 1 dmmptss 
 |-  dom SubMgm C_ Mgm
3 elfvdm 
 |-  ( S e. ( SubMgm ` M ) -> M e. dom SubMgm )
4 2 3 sselid 
 |-  ( S e. ( SubMgm ` M ) -> M e. Mgm )