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 𝐾 )
Assertion	slwpss	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ¬ 𝑃 pGrp 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		slwispgp.1	⊢ 𝑆 = ( 𝐺 ↾s 𝐾 )
2		simp3	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ⊊ 𝐾 )
3	2	pssned	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ≠ 𝐾 )
4	2	pssssd	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ⊆ 𝐾 )
5	4	biantrurd	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( 𝑃 pGrp 𝑆 ↔ ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ) )
6	1	slwispgp	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) )
7	6	3adant3	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) )
8	5 7	bitrd	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( 𝑃 pGrp 𝑆 ↔ 𝐻 = 𝐾 ) )
9	8	necon3bbid	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( ¬ 𝑃 pGrp 𝑆 ↔ 𝐻 ≠ 𝐾 ) )
10	3 9	mpbird	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ¬ 𝑃 pGrp 𝑆 )