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