Theorem slwprm

Description: Reverse closure for the first argument of a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015) (Revised by Mario Carneiro, 2-May-2015)

	Ref	Expression
Assertion	slwprm	|- ( H e. ( P pSyl G ) -> P e. Prime )

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	simp1bi	|- ( H e. ( P pSyl G ) -> P e. Prime )