This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) =/= (/) )