Detailed syntax breakdown of Definition df-sgrp
Step | Hyp | Ref
| Expression |
1 | | csgrp 18016 |
. 2
class
Smgrp |
2 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . . . . . . 11
class 𝑥 |
4 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
5 | 4 | cv 1541 |
. . . . . . . . . . 11
class 𝑦 |
6 | | vo |
. . . . . . . . . . . 12
setvar 𝑜 |
7 | 6 | cv 1541 |
. . . . . . . . . . 11
class 𝑜 |
8 | 3, 5, 7 | co 7170 |
. . . . . . . . . 10
class (𝑥𝑜𝑦) |
9 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
10 | 9 | cv 1541 |
. . . . . . . . . 10
class 𝑧 |
11 | 8, 10, 7 | co 7170 |
. . . . . . . . 9
class ((𝑥𝑜𝑦)𝑜𝑧) |
12 | 5, 10, 7 | co 7170 |
. . . . . . . . . 10
class (𝑦𝑜𝑧) |
13 | 3, 12, 7 | co 7170 |
. . . . . . . . 9
class (𝑥𝑜(𝑦𝑜𝑧)) |
14 | 11, 13 | wceq 1542 |
. . . . . . . 8
wff ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) |
15 | | vb |
. . . . . . . . 9
setvar 𝑏 |
16 | 15 | cv 1541 |
. . . . . . . 8
class 𝑏 |
17 | 14, 9, 16 | wral 3053 |
. . . . . . 7
wff
∀𝑧 ∈
𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) |
18 | 17, 4, 16 | wral 3053 |
. . . . . 6
wff
∀𝑦 ∈
𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) |
19 | 18, 2, 16 | wral 3053 |
. . . . 5
wff
∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) |
20 | | vg |
. . . . . . 7
setvar 𝑔 |
21 | 20 | cv 1541 |
. . . . . 6
class 𝑔 |
22 | | cplusg 16668 |
. . . . . 6
class
+g |
23 | 21, 22 | cfv 6339 |
. . . . 5
class
(+g‘𝑔) |
24 | 19, 6, 23 | wsbc 3680 |
. . . 4
wff
[(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) |
25 | | cbs 16586 |
. . . . 5
class
Base |
26 | 21, 25 | cfv 6339 |
. . . 4
class
(Base‘𝑔) |
27 | 24, 15, 26 | wsbc 3680 |
. . 3
wff
[(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧)) |
28 | | cmgm 17966 |
. . 3
class
Mgm |
29 | 27, 20, 28 | crab 3057 |
. 2
class {𝑔 ∈ Mgm ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} |
30 | 1, 29 | wceq 1542 |
1
wff Smgrp =
{𝑔 ∈ Mgm ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} |