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|tg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgr classGrpOp
1 vg setvarg
2 vt setvart
3 1 cv setvarg
4 2 cv setvart
5 4 4 cxp classt×t
6 5 4 3 wf wffg:t×tt
7 vx setvarx
8 vy setvary
9 vz setvarz
10 7 cv setvarx
11 8 cv setvary
12 10 11 3 co classxgy
13 9 cv setvarz
14 12 13 3 co classxgygz
15 11 13 3 co classygz
16 10 15 3 co classxgygz
17 14 16 wceq wffxgygz=xgygz
18 17 9 4 wral wffztxgygz=xgygz
19 18 8 4 wral wffytztxgygz=xgygz
20 19 7 4 wral wffxtytztxgygz=xgygz
21 vu setvaru
22 21 cv setvaru
23 22 10 3 co classugx
24 23 10 wceq wffugx=x
25 11 10 3 co classygx
26 25 22 wceq wffygx=u
27 26 8 4 wrex wffytygx=u
28 24 27 wa wffugx=xytygx=u
29 28 7 4 wral wffxtugx=xytygx=u
30 29 21 4 wrex wffutxtugx=xytygx=u
31 6 20 30 w3a wffg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=u
32 31 2 wex wfftg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=u
33 32 1 cab classg|tg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=u
34 0 33 wceq wffGrpOp=g|tg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=u