Detailed syntax breakdown of Definition df-cmn
Step | Hyp | Ref
| Expression |
1 | | ccmn 19024 |
. 2
class
CMnd |
2 | | va |
. . . . . . . 8
setvar 𝑎 |
3 | 2 | cv 1541 |
. . . . . . 7
class 𝑎 |
4 | | vb |
. . . . . . . 8
setvar 𝑏 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑏 |
6 | | vg |
. . . . . . . . 9
setvar 𝑔 |
7 | 6 | cv 1541 |
. . . . . . . 8
class 𝑔 |
8 | | cplusg 16668 |
. . . . . . . 8
class
+g |
9 | 7, 8 | cfv 6339 |
. . . . . . 7
class
(+g‘𝑔) |
10 | 3, 5, 9 | co 7170 |
. . . . . 6
class (𝑎(+g‘𝑔)𝑏) |
11 | 5, 3, 9 | co 7170 |
. . . . . 6
class (𝑏(+g‘𝑔)𝑎) |
12 | 10, 11 | wceq 1542 |
. . . . 5
wff (𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎) |
13 | | cbs 16586 |
. . . . . 6
class
Base |
14 | 7, 13 | cfv 6339 |
. . . . 5
class
(Base‘𝑔) |
15 | 12, 4, 14 | wral 3053 |
. . . 4
wff
∀𝑏 ∈
(Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎) |
16 | 15, 2, 14 | wral 3053 |
. . 3
wff
∀𝑎 ∈
(Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎) |
17 | | cmnd 18027 |
. . 3
class
Mnd |
18 | 16, 6, 17 | crab 3057 |
. 2
class {𝑔 ∈ Mnd ∣
∀𝑎 ∈
(Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)} |
19 | 1, 18 | wceq 1542 |
1
wff CMnd =
{𝑔 ∈ Mnd ∣
∀𝑎 ∈
(Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)} |