Theorem submrcl

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

	Ref	Expression
Assertion	submrcl	$$⊢S\in \mathrm{SubMnd}\left(M\right)\to M\in \mathrm{Mnd}$$

Proof

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