Definition df-grpo 30512

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.)

Assertion

Ref	Expression
df-grpo	⊢ GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))}

Distinct variable group:   𝑡,𝑔,𝑢,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-grpo

Step	Hyp	Ref	Expression
1		cgr 30508	. 2 class GrpOp
2		vt	. . . . . . . 8 setvar 𝑡
3	2	cv 1539	. . . . . . 7 class 𝑡
4	3, 3	cxp 5683	. . . . . 6 class (𝑡 × 𝑡)
5		vg	. . . . . . 7 setvar 𝑔
6	5	cv 1539	. . . . . 6 class 𝑔
7	4, 3, 6	wf 6557	. . . . 5 wff 𝑔:(𝑡 × 𝑡)⟶𝑡
8		vx	. . . . . . . . . . . 12 setvar 𝑥
9	8	cv 1539	. . . . . . . . . . 11 class 𝑥
10		vy	. . . . . . . . . . . 12 setvar 𝑦
11	10	cv 1539	. . . . . . . . . . 11 class 𝑦
12	9, 11, 6	co 7431	. . . . . . . . . 10 class (𝑥𝑔𝑦)
13		vz	. . . . . . . . . . 11 setvar 𝑧
14	13	cv 1539	. . . . . . . . . 10 class 𝑧
15	12, 14, 6	co 7431	. . . . . . . . 9 class ((𝑥𝑔𝑦)𝑔𝑧)
16	11, 14, 6	co 7431	. . . . . . . . . 10 class (𝑦𝑔𝑧)
17	9, 16, 6	co 7431	. . . . . . . . 9 class (𝑥𝑔(𝑦𝑔𝑧))
18	15, 17	wceq 1540	. . . . . . . 8 wff ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
19	18, 13, 3	wral 3061	. . . . . . 7 wff ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
20	19, 10, 3	wral 3061	. . . . . 6 wff ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
21	20, 8, 3	wral 3061	. . . . 5 wff ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
22		vu	. . . . . . . . . . 11 setvar 𝑢
23	22	cv 1539	. . . . . . . . . 10 class 𝑢
24	23, 9, 6	co 7431	. . . . . . . . 9 class (𝑢𝑔𝑥)
25	24, 9	wceq 1540	. . . . . . . 8 wff (𝑢𝑔𝑥) = 𝑥
26	11, 9, 6	co 7431	. . . . . . . . . 10 class (𝑦𝑔𝑥)
27	26, 23	wceq 1540	. . . . . . . . 9 wff (𝑦𝑔𝑥) = 𝑢
28	27, 10, 3	wrex 3070	. . . . . . . 8 wff ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢
29	25, 28	wa 395	. . . . . . 7 wff ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)
30	29, 8, 3	wral 3061	. . . . . 6 wff ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)
31	30, 22, 3	wrex 3070	. . . . 5 wff ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)
32	7, 21, 31	w3a 1087	. . . 4 wff (𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))
33	32, 2	wex 1779	. . 3 wff ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))
34	33, 5	cab 2714	. 2 class {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))}
35	1, 34	wceq 1540	1 wff GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))}

This definition is referenced by:  isgrpo  30516