Detailed syntax breakdown of Definition df-slw
Step | Hyp | Ref
| Expression |
1 | | cslw 18919 |
. 2
class
pSyl |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | vg |
. . 3
setvar 𝑔 |
4 | | cprime 16228 |
. . 3
class
ℙ |
5 | | cgrp 18365 |
. . 3
class
Grp |
6 | | vh |
. . . . . . . . 9
setvar ℎ |
7 | 6 | cv 1542 |
. . . . . . . 8
class ℎ |
8 | | vk |
. . . . . . . . 9
setvar 𝑘 |
9 | 8 | cv 1542 |
. . . . . . . 8
class 𝑘 |
10 | 7, 9 | wss 3866 |
. . . . . . 7
wff ℎ ⊆ 𝑘 |
11 | 2 | cv 1542 |
. . . . . . . 8
class 𝑝 |
12 | 3 | cv 1542 |
. . . . . . . . 9
class 𝑔 |
13 | | cress 16784 |
. . . . . . . . 9
class
↾s |
14 | 12, 9, 13 | co 7213 |
. . . . . . . 8
class (𝑔 ↾s 𝑘) |
15 | | cpgp 18918 |
. . . . . . . 8
class
pGrp |
16 | 11, 14, 15 | wbr 5053 |
. . . . . . 7
wff 𝑝 pGrp (𝑔 ↾s 𝑘) |
17 | 10, 16 | wa 399 |
. . . . . 6
wff (ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) |
18 | 6, 8 | weq 1971 |
. . . . . 6
wff ℎ = 𝑘 |
19 | 17, 18 | wb 209 |
. . . . 5
wff ((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘) |
20 | | csubg 18537 |
. . . . . 6
class
SubGrp |
21 | 12, 20 | cfv 6380 |
. . . . 5
class
(SubGrp‘𝑔) |
22 | 19, 8, 21 | wral 3061 |
. . . 4
wff
∀𝑘 ∈
(SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘) |
23 | 22, 6, 21 | crab 3065 |
. . 3
class {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)} |
24 | 2, 3, 4, 5, 23 | cmpo 7215 |
. 2
class (𝑝 ∈ ℙ, 𝑔 ∈ Grp ↦ {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)}) |
25 | 1, 24 | wceq 1543 |
1
wff pSyl =
(𝑝 ∈ ℙ, 𝑔 ∈ Grp ↦ {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)}) |