Metamath Proof Explorer

Theorem slwsubg

Description: A Sylow P -subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion slwsubg 
|- ( H e. ( P pSyl G ) -> H e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 isslw 
 |-  ( H e. ( P pSyl G ) <-> ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )
2 1 simp2bi 
 |-  ( H e. ( P pSyl G ) -> H e. ( SubGrp ` G ) )