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 ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → P pSyl G ≠ ∅

Proof

Step Hyp Ref Expression
1 slwn0.1 ⊢ X = Base G
2 eqid ⊢ 0 G = 0 G
3 2 0subg ⊢ G ∈ Grp → 0 G ∈ SubGrp ⁡ G
4 3 3ad2ant1 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → 0 G ∈ SubGrp ⁡ G
5 simp2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → X ∈ Fin
6 2 pgp0 ⊢ G ∈ Grp ∧ P ∈ ℙ → P pGrp G ↾ 𝑠 0 G
7 6 3adant2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → P pGrp G ↾ 𝑠 0 G
8 eqid ⊢ G ↾ 𝑠 0 G = G ↾ 𝑠 0 G
9 eqid ⊢ x ∈ y ∈ SubGrp ⁡ G | P pGrp G ↾ 𝑠 y ∧ 0 G ⊆ y ⟼ x = x ∈ y ∈ SubGrp ⁡ G | P pGrp G ↾ 𝑠 y ∧ 0 G ⊆ y ⟼ x
10 1 8 9 pgpssslw ⊢ 0 G ∈ SubGrp ⁡ G ∧ X ∈ Fin ∧ P pGrp G ↾ 𝑠 0 G → ∃ z ∈ P pSyl G 0 G ⊆ z
11 4 5 7 10 syl3anc ⊢ G ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → ∃ z ∈ P pSyl G 0 G ⊆ z
12 rexn0 ⊢ ∃ z ∈ P pSyl G 0 G ⊆ z → P pSyl G ≠ ∅
13 11 12 syl ⊢ G ∈ Grp ∧ X ∈ Fin ∧ P ∈ ℙ → P pSyl G ≠ ∅