Theorem slwprm

Description: Reverse closure for the first argument of a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015) (Revised by Mario Carneiro, 2-May-2015)

	Ref	Expression
Assertion	slwprm	$$⊢H\in \left(P\mathrm{pSyl}G\right)\to P\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		isslw	$$⊢H\in \left(P\mathrm{pSyl}G\right)\leftrightarrow \left(P\in \mathbb{P}\wedge H\in \mathrm{SubGrp}\left(G\right)\wedge \forall k\in \mathrm{SubGrp}\left(G\right)\left(\left(H\subseteq k\wedge P\mathrm{pGrp}\left(G{\upharpoonright }_{𝑠}k\right)\right)\leftrightarrow H=k\right)\right)$$
2	1	simp1bi	$$⊢H\in \left(P\mathrm{pSyl}G\right)\to P\in \mathbb{P}$$