Metamath Proof Explorer

Theorem mgm2mgm

Description: Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020)

Ref Expression
Assertion mgm2mgm ⊢ M ∈ MgmALT ↔ M ∈ Mgm

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base M = Base M
2 eqid ⊢ + M = + M
3 1 2 ismgmALT ⊢ M ∈ MgmALT → M ∈ MgmALT ↔ + M clLaw Base M
4 fvex ⊢ + M ∈ V
5 fvex ⊢ Base M ∈ V
6 iscllaw ⊢ + M ∈ V ∧ Base M ∈ V → + M clLaw Base M ↔ ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
7 4 5 6 mp2an ⊢ + M clLaw Base M ↔ ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
8 1 2 ismgm ⊢ M ∈ MgmALT → M ∈ Mgm ↔ ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M
9 8 biimprd ⊢ M ∈ MgmALT → ∀ x ∈ Base M ∀ y ∈ Base M x + M y ∈ Base M → M ∈ Mgm
10 7 9 syl5bi ⊢ M ∈ MgmALT → + M clLaw Base M → M ∈ Mgm
11 3 10 sylbid ⊢ M ∈ MgmALT → M ∈ MgmALT → M ∈ Mgm
12 11 pm2.43i ⊢ M ∈ MgmALT → M ∈ Mgm
13 mgmplusgiopALT ⊢ M ∈ Mgm → + M clLaw Base M
14 1 2 ismgmALT ⊢ M ∈ Mgm → M ∈ MgmALT ↔ + M clLaw Base M
15 13 14 mpbird ⊢ M ∈ Mgm → M ∈ MgmALT
16 12 15 impbii ⊢ M ∈ MgmALT ↔ M ∈ Mgm