Metamath Proof Explorer

Theorem submrcl

Description: Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Assertion submrcl 
|- ( S e. ( SubMnd ` M ) -> M e. Mnd )

Proof

Step Hyp Ref Expression
1 df-submnd 
 |-  SubMnd = ( s e. Mnd |-> { t e. ~P ( Base ` s ) | ( ( 0g ` s ) e. t /\ A. x e. t A. y e. t ( x ( +g ` s ) y ) e. t ) } )
2 1 mptrcl 
 |-  ( S e. ( SubMnd ` M ) -> M e. Mnd )