# Metamath Proof Explorer

## Definition df-mgm

Description: Amagma 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)

Ref Expression
Assertion df-mgm
`|- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgm
` |-  Mgm`
1 vg
` |-  g`
2 cbs
` |-  Base`
3 1 cv
` |-  g`
4 3 2 cfv
` |-  ( Base ` g )`
5 vb
` |-  b`
6 cplusg
` |-  +g`
7 3 6 cfv
` |-  ( +g ` g )`
8 vo
` |-  o`
9 vx
` |-  x`
10 5 cv
` |-  b`
11 vy
` |-  y`
12 9 cv
` |-  x`
13 8 cv
` |-  o`
14 11 cv
` |-  y`
15 12 14 13 co
` |-  ( x o y )`
16 15 10 wcel
` |-  ( x o y ) e. b`
17 16 11 10 wral
` |-  A. y e. b ( x o y ) e. b`
18 17 9 10 wral
` |-  A. x e. b A. y e. b ( x o y ) e. b`
19 18 8 7 wsbc
` |-  [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b`
20 19 5 4 wsbc
` |-  [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b`
21 20 1 cab
` |-  { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }`
22 0 21 wceq
` |-  Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }`