Theorem submrcl

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

	Ref	Expression
Assertion	submrcl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		df-submnd	⊢ SubMnd = ( 𝑠 ∈ Mnd ↦ { 𝑡 ∈ 𝒫 ( Base ‘ 𝑠 ) ∣ ( ( 0g ‘ 𝑠 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ∈ 𝑡 ) } )
2	1	mptrcl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )