Theorem slwn0

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

	Ref	Expression
Hypothesis	slwn0.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion	slwn0	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		slwn0.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
3	2	0subg	⊢ ( 𝐺 ∈ Grp → { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) )
4	3	3ad2ant1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) )
5		simp2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → 𝑋 ∈ Fin )
6	2	pgp0	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) )
7	6	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) )
8		eqid	⊢ ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) = ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } )
9		eqid	⊢ ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ { ( 0g ‘ 𝐺 ) } ⊆ 𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑃 pGrp ( 𝐺 ↾s 𝑦 ) ∧ { ( 0g ‘ 𝐺 ) } ⊆ 𝑦 ) } ↦ ( ♯ ‘ 𝑥 ) )
10	1 8 9	pgpssslw	⊢ ( ( { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp ( 𝐺 ↾s { ( 0g ‘ 𝐺 ) } ) ) → ∃ 𝑧 ∈ ( 𝑃 pSyl 𝐺 ) { ( 0g ‘ 𝐺 ) } ⊆ 𝑧 )
11	4 5 7 10	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ∃ 𝑧 ∈ ( 𝑃 pSyl 𝐺 ) { ( 0g ‘ 𝐺 ) } ⊆ 𝑧 )
12		rexn0	⊢ ( ∃ 𝑧 ∈ ( 𝑃 pSyl 𝐺 ) { ( 0g ‘ 𝐺 ) } ⊆ 𝑧 → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )
13	11 12	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )