# Metamath Proof Explorer

## Theorem clmgmOLD

Description: Obsolete version of mgmcl as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis clmgmOLD.1 ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}$
Assertion clmgmOLD ${⊢}\left({G}\in \mathrm{Magma}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$

### Proof

Step Hyp Ref Expression
1 clmgmOLD.1 ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}$
2 1 ismgmOLD ${⊢}{G}\in \mathrm{Magma}\to \left({G}\in \mathrm{Magma}↔{G}:{X}×{X}⟶{X}\right)$
3 fovrn ${⊢}\left({G}:{X}×{X}⟶{X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$
4 3 3exp ${⊢}{G}:{X}×{X}⟶{X}\to \left({A}\in {X}\to \left({B}\in {X}\to {A}{G}{B}\in {X}\right)\right)$
5 2 4 syl6bi ${⊢}{G}\in \mathrm{Magma}\to \left({G}\in \mathrm{Magma}\to \left({A}\in {X}\to \left({B}\in {X}\to {A}{G}{B}\in {X}\right)\right)\right)$
6 5 pm2.43i ${⊢}{G}\in \mathrm{Magma}\to \left({A}\in {X}\to \left({B}\in {X}\to {A}{G}{B}\in {X}\right)\right)$
7 6 3imp ${⊢}\left({G}\in \mathrm{Magma}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$