This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 / o]˙ ∀ x ∈ b ∀ y ∈ b x o y ∈ b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgm class Mgm
1 vg setvar g
2 cbs class Base
3 1 cv setvar g
4 3 2 cfv class Base g
5 vb setvar b
6 cplusg class + 𝑔
7 3 6 cfv class + g
8 vo setvar o
9 vx setvar x
10 5 cv setvar b
11 vy setvar y
12 9 cv setvar x
13 8 cv setvar o
14 11 cv setvar y
15 12 14 13 co class x o y
16 15 10 wcel wff x o y ∈ b
17 16 11 10 wral wff ∀ y ∈ b x o y ∈ b
18 17 9 10 wral wff ∀ x ∈ b ∀ y ∈ b x o y ∈ b
19 18 8 7 wsbc wff [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b x o y ∈ b
20 19 5 4 wsbc wff [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b x o y ∈ b
21 20 1 cab class g | [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b x o y ∈ b
22 0 21 wceq wff Mgm = g | [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b x o y ∈ b