MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-slw Structured version   Unicode version

Definition df-slw 16034
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.)
Assertion
Ref Expression
df-slw  |- pSyl  =  ( p  e.  Prime ,  g  e.  Grp  |->  { h  e.  (SubGrp `  g )  |  A. k  e.  (SubGrp `  g ) ( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <-> 
h  =  k ) } )
Distinct variable group:    g, h, k, p

Detailed syntax breakdown of Definition df-slw
StepHypRef Expression
1 cslw 16030 . 2  class pSyl
2 vp . . 3  setvar  p
3 vg . . 3  setvar  g
4 cprime 13762 . . 3  class  Prime
5 cgrp 15409 . . 3  class  Grp
6 vh . . . . . . . . 9  setvar  h
76cv 1368 . . . . . . . 8  class  h
8 vk . . . . . . . . 9  setvar  k
98cv 1368 . . . . . . . 8  class  k
107, 9wss 3327 . . . . . . 7  wff  h  C_  k
112cv 1368 . . . . . . . 8  class  p
123cv 1368 . . . . . . . . 9  class  g
13 cress 14174 . . . . . . . . 9  classs
1412, 9, 13co 6090 . . . . . . . 8  class  ( gs  k )
15 cpgp 16029 . . . . . . . 8  class pGrp
1611, 14, 15wbr 4291 . . . . . . 7  wff  p pGrp  (
gs  k )
1710, 16wa 369 . . . . . 6  wff  ( h 
C_  k  /\  p pGrp  ( gs  k ) )
186, 8weq 1695 . . . . . 6  wff  h  =  k
1917, 18wb 184 . . . . 5  wff  ( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <-> 
h  =  k )
20 csubg 15674 . . . . . 6  class SubGrp
2112, 20cfv 5417 . . . . 5  class  (SubGrp `  g )
2219, 8, 21wral 2714 . . . 4  wff  A. k  e.  (SubGrp `  g )
( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <->  h  =  k )
2322, 6, 21crab 2718 . . 3  class  { h  e.  (SubGrp `  g )  |  A. k  e.  (SubGrp `  g ) ( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <-> 
h  =  k ) }
242, 3, 4, 5, 23cmpt2 6092 . 2  class  ( p  e.  Prime ,  g  e. 
Grp  |->  { h  e.  (SubGrp `  g )  |  A. k  e.  (SubGrp `  g ) ( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <-> 
h  =  k ) } )
251, 24wceq 1369 1  wff pSyl  =  ( p  e.  Prime ,  g  e.  Grp  |->  { h  e.  (SubGrp `  g )  |  A. k  e.  (SubGrp `  g ) ( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <-> 
h  =  k ) } )
Colors of variables: wff setvar class
This definition is referenced by:  isslw  16106
  Copyright terms: Public domain W3C validator