Theorem slwn0

Description: Every finite group contains a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypothesis	slwn0.1	|- X = ( Base ` G )
Assertion	slwn0	|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( P pSyl G ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		slwn0.1	|- X = ( Base ` G )
2		eqid	|- ( 0g ` G ) = ( 0g ` G )
3	2	0subg	|- ( G e. Grp -> { ( 0g ` G ) } e. ( SubGrp ` G ) )
4	3	3ad2ant1	|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> { ( 0g ` G ) } e. ( SubGrp ` G ) )
5		simp2	|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> X e. Fin )
6	2	pgp0	|- ( ( G e. Grp /\ P e. Prime ) -> P pGrp ( G |`s { ( 0g ` G ) } ) )
7	6	3adant2	|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> P pGrp ( G |`s { ( 0g ` G ) } ) )
8		eqid	|- ( G |`s { ( 0g ` G ) } ) = ( G |`s { ( 0g ` G ) } )
9		eqid	|- ( x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ { ( 0g ` G ) } C_ y ) } |-> ( # ` x ) ) = ( x e. { y e. ( SubGrp ` G ) | ( P pGrp ( G |`s y ) /\ { ( 0g ` G ) } C_ y ) } |-> ( # ` x ) )
10	1 8 9	pgpssslw	|- ( ( { ( 0g ` G ) } e. ( SubGrp ` G ) /\ X e. Fin /\ P pGrp ( G |`s { ( 0g ` G ) } ) ) -> E. z e. ( P pSyl G ) { ( 0g ` G ) } C_ z )
11	4 5 7 10	syl3anc	|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> E. z e. ( P pSyl G ) { ( 0g ` G ) } C_ z )
12		rexn0	|- ( E. z e. ( P pSyl G ) { ( 0g ` G ) } C_ z -> ( P pSyl G ) =/= (/) )
13	11 12	syl	|- ( ( G e. Grp /\ X e. Fin /\ P e. Prime ) -> ( P pSyl G ) =/= (/) )