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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cgr | |
|
1 | vg | |
|
2 | vt | |
|
3 | 1 | cv | |
4 | 2 | cv | |
5 | 4 4 | cxp | |
6 | 5 4 3 | wf | |
7 | vx | |
|
8 | vy | |
|
9 | vz | |
|
10 | 7 | cv | |
11 | 8 | cv | |
12 | 10 11 3 | co | |
13 | 9 | cv | |
14 | 12 13 3 | co | |
15 | 11 13 3 | co | |
16 | 10 15 3 | co | |
17 | 14 16 | wceq | |
18 | 17 9 4 | wral | |
19 | 18 8 4 | wral | |
20 | 19 7 4 | wral | |
21 | vu | |
|
22 | 21 | cv | |
23 | 22 10 3 | co | |
24 | 23 10 | wceq | |
25 | 11 10 3 | co | |
26 | 25 22 | wceq | |
27 | 26 8 4 | wrex | |
28 | 24 27 | wa | |
29 | 28 7 4 | wral | |
30 | 29 21 4 | wrex | |
31 | 6 20 30 | w3a | |
32 | 31 2 | wex | |
33 | 32 1 | cab | |
34 | 0 33 | wceq | |