Metamath Proof Explorer

Theorem slwpss

Description: A proper superset of a Sylow subgroup is not a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis slwispgp.1 ⊢ S = G ↾ 𝑠 K
Assertion slwpss ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → ¬ P pGrp S

Proof

Step Hyp Ref Expression
1 slwispgp.1 ⊢ S = G ↾ 𝑠 K
2 simp3 ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → H ⊂ K
3 2 pssned ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → H ≠ K
4 2 pssssd ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → H ⊆ K
5 4 biantrurd ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → P pGrp S ↔ H ⊆ K ∧ P pGrp S
6 1 slwispgp ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G → H ⊆ K ∧ P pGrp S ↔ H = K
7 6 3adant3 ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → H ⊆ K ∧ P pGrp S ↔ H = K
8 5 7 bitrd ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → P pGrp S ↔ H = K
9 8 necon3bbid ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → ¬ P pGrp S ↔ H ≠ K
10 3 9 mpbird ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G ∧ H ⊂ K → ¬ P pGrp S