Detailed syntax breakdown of Definition df-submnd
Step | Hyp | Ref
| Expression |
1 | | csubmnd 18217 |
. 2
class
SubMnd |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | cmnd 18173 |
. . 3
class
Mnd |
4 | 2 | cv 1542 |
. . . . . . 7
class 𝑠 |
5 | | c0g 16944 |
. . . . . . 7
class
0g |
6 | 4, 5 | cfv 6380 |
. . . . . 6
class
(0g‘𝑠) |
7 | | vt |
. . . . . . 7
setvar 𝑡 |
8 | 7 | cv 1542 |
. . . . . 6
class 𝑡 |
9 | 6, 8 | wcel 2110 |
. . . . 5
wff
(0g‘𝑠) ∈ 𝑡 |
10 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
11 | 10 | cv 1542 |
. . . . . . . . 9
class 𝑥 |
12 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
13 | 12 | cv 1542 |
. . . . . . . . 9
class 𝑦 |
14 | | cplusg 16802 |
. . . . . . . . . 10
class
+g |
15 | 4, 14 | cfv 6380 |
. . . . . . . . 9
class
(+g‘𝑠) |
16 | 11, 13, 15 | co 7213 |
. . . . . . . 8
class (𝑥(+g‘𝑠)𝑦) |
17 | 16, 8 | wcel 2110 |
. . . . . . 7
wff (𝑥(+g‘𝑠)𝑦) ∈ 𝑡 |
18 | 17, 12, 8 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡 |
19 | 18, 10, 8 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈
𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡 |
20 | 9, 19 | wa 399 |
. . . 4
wff
((0g‘𝑠) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡) |
21 | | cbs 16760 |
. . . . . 6
class
Base |
22 | 4, 21 | cfv 6380 |
. . . . 5
class
(Base‘𝑠) |
23 | 22 | cpw 4513 |
. . . 4
class 𝒫
(Base‘𝑠) |
24 | 20, 7, 23 | crab 3065 |
. . 3
class {𝑡 ∈ 𝒫
(Base‘𝑠) ∣
((0g‘𝑠)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡)} |
25 | 2, 3, 24 | cmpt 5135 |
. 2
class (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫
(Base‘𝑠) ∣
((0g‘𝑠)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡)}) |
26 | 1, 25 | wceq 1543 |
1
wff SubMnd =
(𝑠 ∈ Mnd ↦
{𝑡 ∈ 𝒫
(Base‘𝑠) ∣
((0g‘𝑠)
∈ 𝑡 ∧
∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡)}) |