Description: Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | submgmrcl | ⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ Mgm ) |
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 | sselid | ⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ Mgm ) |