MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mgm Structured version   Visualization version   GIF version

Definition df-mgm 17007
Description: A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-mgm Mgm = {𝑔[(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
Distinct variable group:   𝑔,𝑏,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-mgm
StepHypRef Expression
1 cmgm 17005 . 2 class Mgm
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1473 . . . . . . . . 9 class 𝑥
4 vy . . . . . . . . . 10 setvar 𝑦
54cv 1473 . . . . . . . . 9 class 𝑦
6 vo . . . . . . . . . 10 setvar 𝑜
76cv 1473 . . . . . . . . 9 class 𝑜
83, 5, 7co 6523 . . . . . . . 8 class (𝑥𝑜𝑦)
9 vb . . . . . . . . 9 setvar 𝑏
109cv 1473 . . . . . . . 8 class 𝑏
118, 10wcel 1975 . . . . . . 7 wff (𝑥𝑜𝑦) ∈ 𝑏
1211, 4, 10wral 2891 . . . . . 6 wff 𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏
1312, 2, 10wral 2891 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏
14 vg . . . . . . 7 setvar 𝑔
1514cv 1473 . . . . . 6 class 𝑔
16 cplusg 15710 . . . . . 6 class +g
1715, 16cfv 5786 . . . . 5 class (+g𝑔)
1813, 6, 17wsbc 3397 . . . 4 wff [(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏
19 cbs 15637 . . . . 5 class Base
2015, 19cfv 5786 . . . 4 class (Base‘𝑔)
2118, 9, 20wsbc 3397 . . 3 wff [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏
2221, 14cab 2591 . 2 class {𝑔[(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
231, 22wceq 1474 1 wff Mgm = {𝑔[(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
Colors of variables: wff setvar class
This definition is referenced by:  ismgm  17008
  Copyright terms: Public domain W3C validator