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