Theorem submgmrcl

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

	Ref	Expression
Assertion	submgmrcl	⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		df-submgm	⊢ SubMgm = ( 𝑠 ∈ Mgm ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 } )
2	1	dmmptss	⊢ dom SubMgm ⊆ Mgm
3		elfvdm	⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ dom SubMgm )
4	2 3	sseldi	⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ Mgm )