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

Definition df-slw 14847
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 14843 . 2  class pSyl
2 vp . . 3  set  p
3 vg . . 3  set  g
4 cprime 12758 . . 3  class  Prime
5 cgrp 14362 . . 3  class  Grp
6 vh . . . . . . . . 9  set  h
76cv 1622 . . . . . . . 8  class  h
8 vk . . . . . . . . 9  set  k
98cv 1622 . . . . . . . 8  class  k
107, 9wss 3152 . . . . . . 7  wff  h  C_  k
112cv 1622 . . . . . . . 8  class  p
123cv 1622 . . . . . . . . 9  class  g
13 cress 13149 . . . . . . . . 9  classs
1412, 9, 13co 5858 . . . . . . . 8  class  ( gs  k )
15 cpgp 14842 . . . . . . . 8  class pGrp
1611, 14, 15wbr 4023 . . . . . . 7  wff  p pGrp  (
gs  k )
1710, 16wa 358 . . . . . 6  wff  ( h 
C_  k  /\  p pGrp  ( gs  k ) )
186, 8weq 1624 . . . . . 6  wff  h  =  k
1917, 18wb 176 . . . . 5  wff  ( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <-> 
h  =  k )
20 csubg 14615 . . . . . 6  class SubGrp
2112, 20cfv 5255 . . . . 5  class  (SubGrp `  g )
2219, 8, 21wral 2543 . . . 4  wff  A. k  e.  (SubGrp `  g )
( ( h  C_  k  /\  p pGrp  ( gs  k ) )  <->  h  =  k )
2322, 6, 21crab 2547 . . 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 5860 . 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 1623 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 set class
This definition is referenced by:  isslw  14919
  Copyright terms: Public domain W3C validator