Metamath Proof Explorer

Theorem submrcl

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

		Ref	Expression
	Assertion	submrcl	$⊢ S \in SubMnd (M) \to M \in Mnd$

Step	Hyp	Ref	Expression
1		df-submnd	$⊢ SubMnd = (s \in Mnd ⟼ \{t \in 𝒫 {Base}_{s} \| (0_{s} \in t \land \forall x \in t \forall y \in t x +_{s} y \in t)\})$
2	1	mptrcl	$⊢ S \in SubMnd (M) \to M \in Mnd$