Theorem slwsubg

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

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

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	simp2bi	$$⊢H\in \left(P\mathrm{pSyl}G\right)\to H\in \mathrm{SubGrp}\left(G\right)$$