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 = ( p e. Prime , g e. Grp |-> { h e. ( SubGrp ` g ) | A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslw 
 |-  pSyl
1 vp 
 |-  p
2 cprime 
 |-  Prime
3 vg 
 |-  g
4 cgrp 
 |-  Grp
5 vh 
 |-  h
6 csubg 
 |-  SubGrp
7 3 cv 
 |-  g
8 7 6 cfv 
 |-  ( SubGrp ` g )
9 vk 
 |-  k
10 5 cv 
 |-  h
11 9 cv 
 |-  k
12 10 11 wss 
 |-  h C_ k
13 1 cv 
 |-  p
14 cpgp 
 |-  pGrp
15 cress 
 |-  |`s
16 7 11 15 co 
 |-  ( g |`s k )
17 13 16 14 wbr 
 |-  p pGrp ( g |`s k )
18 12 17 wa 
 |-  ( h C_ k /\ p pGrp ( g |`s k ) )
19 10 11 wceq 
 |-  h = k
20 18 19 wb 
 |-  ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k )
21 20 9 8 wral 
 |-  A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k )
22 21 5 8 crab 
 |-  { h e. ( SubGrp ` g ) | A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) }
23 1 3 2 4 22 cmpo 
 |-  ( p e. Prime , g e. Grp |-> { h e. ( SubGrp ` g ) | A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) } )
24 0 23 wceq 
 |-  pSyl = ( p e. Prime , g e. Grp |-> { h e. ( SubGrp ` g ) | A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) } )