Metamath Proof Explorer


Definition df-slw

Description: Define the set of Sylow p-subgroups of a group g . A Sylow p-subgroup is a p-group that is not a subgroup of any other p-groups in g . (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion df-slw pSyl = ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( 𝑘𝑝 pGrp ( 𝑔s 𝑘 ) ) ↔ = 𝑘 ) } )

Detailed syntax breakdown

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 𝑘 ) ) ↔ = 𝑘 ) } )