Step |
Hyp |
Ref |
Expression |
0 |
|
cslw |
⊢ pSyl |
1 |
|
vp |
⊢ 𝑝 |
2 |
|
cprime |
⊢ ℙ |
3 |
|
vg |
⊢ 𝑔 |
4 |
|
cgrp |
⊢ Grp |
5 |
|
vh |
⊢ ℎ |
6 |
|
csubg |
⊢ SubGrp |
7 |
3
|
cv |
⊢ 𝑔 |
8 |
7 6
|
cfv |
⊢ ( SubGrp ‘ 𝑔 ) |
9 |
|
vk |
⊢ 𝑘 |
10 |
5
|
cv |
⊢ ℎ |
11 |
9
|
cv |
⊢ 𝑘 |
12 |
10 11
|
wss |
⊢ ℎ ⊆ 𝑘 |
13 |
1
|
cv |
⊢ 𝑝 |
14 |
|
cpgp |
⊢ pGrp |
15 |
|
cress |
⊢ ↾s |
16 |
7 11 15
|
co |
⊢ ( 𝑔 ↾s 𝑘 ) |
17 |
13 16 14
|
wbr |
⊢ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) |
18 |
12 17
|
wa |
⊢ ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) |
19 |
10 11
|
wceq |
⊢ ℎ = 𝑘 |
20 |
18 19
|
wb |
⊢ ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) |
21 |
20 9 8
|
wral |
⊢ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) |
22 |
21 5 8
|
crab |
⊢ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } |
23 |
1 3 2 4 22
|
cmpo |
⊢ ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } ) |
24 |
0 23
|
wceq |
⊢ pSyl = ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ℎ ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( ℎ ⊆ 𝑘 ∧ 𝑝 pGrp ( 𝑔 ↾s 𝑘 ) ) ↔ ℎ = 𝑘 ) } ) |