Theorem submgmrcl

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

	Ref	Expression
Assertion	submgmrcl	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		df-submgm	$$⊢\mathrm{SubMgm}=\left(s\in \mathrm{Mgm}⟼\left\{t\in 𝒫{\mathrm{Base}}_s|\forall x\in t\forall y\in tx{+}_{s}y\in t\right\}\right)$$
2	1	dmmptss	$$⊢\mathrm{dom}\mathrm{SubMgm}\subseteq \mathrm{Mgm}$$
3		elfvdm	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to M\in \mathrm{dom}\mathrm{SubMgm}$$
4	2 3	sseldi	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to M\in \mathrm{Mgm}$$