Metamath Proof Explorer

Definition df-grpo

Description: Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of Herstein p. 54. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Assertion df-grpo ⊢ GrpOp = g | ∃ t g : t × t ⟶ t ∧ ∀ x ∈ t ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z ∧ ∃ u ∈ t ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgr class GrpOp
1 vg setvar g
2 vt setvar t
3 1 cv setvar g
4 2 cv setvar t
5 4 4 cxp class t × t
6 5 4 3 wf wff g : t × t ⟶ t
7 vx setvar x
8 vy setvar y
9 vz setvar z
10 7 cv setvar x
11 8 cv setvar y
12 10 11 3 co class x g y
13 9 cv setvar z
14 12 13 3 co class x g y g z
15 11 13 3 co class y g z
16 10 15 3 co class x g y g z
17 14 16 wceq wff x g y g z = x g y g z
18 17 9 4 wral wff ∀ z ∈ t x g y g z = x g y g z
19 18 8 4 wral wff ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z
20 19 7 4 wral wff ∀ x ∈ t ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z
21 vu setvar u
22 21 cv setvar u
23 22 10 3 co class u g x
24 23 10 wceq wff u g x = x
25 11 10 3 co class y g x
26 25 22 wceq wff y g x = u
27 26 8 4 wrex wff ∃ y ∈ t y g x = u
28 24 27 wa wff u g x = x ∧ ∃ y ∈ t y g x = u
29 28 7 4 wral wff ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u
30 29 21 4 wrex wff ∃ u ∈ t ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u
31 6 20 30 w3a wff g : t × t ⟶ t ∧ ∀ x ∈ t ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z ∧ ∃ u ∈ t ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u
32 31 2 wex wff ∃ t g : t × t ⟶ t ∧ ∀ x ∈ t ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z ∧ ∃ u ∈ t ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u
33 32 1 cab class g | ∃ t g : t × t ⟶ t ∧ ∀ x ∈ t ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z ∧ ∃ u ∈ t ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u
34 0 33 wceq wff GrpOp = g | ∃ t g : t × t ⟶ t ∧ ∀ x ∈ t ∀ y ∈ t ∀ z ∈ t x g y g z = x g y g z ∧ ∃ u ∈ t ∀ x ∈ t u g x = x ∧ ∃ y ∈ t y g x = u