slwn0

Description: Every finite group contains a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

		Ref	Expression
	Hypothesis	slwn0.1	$⊢ X = {Base}_{G}$
	Assertion	slwn0	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to P pSyl G \neq \emptyset$

Step	Hyp	Ref	Expression
1		slwn0.1	$⊢ X = {Base}_{G}$
2		eqid	$⊢ 0_{G} = 0_{G}$
3	2	0subg	$⊢ G \in Grp \to \{0_{G}\} \in SubGrp (G)$
4	3	3ad2ant1	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to \{0_{G}\} \in SubGrp (G)$
5		simp2	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to X \in Fin$
6	2	pgp0	$⊢ (G \in Grp \land P \in ℙ) \to P pGrp (G ↾_{𝑠} \{0_{G}\})$
7	6	3adant2	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to P pGrp (G ↾_{𝑠} \{0_{G}\})$
8		eqid	$⊢ G ↾_{𝑠} \{0_{G}\} = G ↾_{𝑠} \{0_{G}\}$
9		eqid	$⊢ (x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land \{0_{G}\} \subseteq y)\} ⟼ \|x\|) = (x \in \{y \in SubGrp (G) \| (P pGrp (G ↾_{𝑠} y) \land \{0_{G}\} \subseteq y)\} ⟼ \|x\|)$
10	1 8 9	pgpssslw	$⊢ (\{0_{G}\} \in SubGrp (G) \land X \in Fin \land P pGrp (G ↾_{𝑠} \{0_{G}\})) \to \exists z \in (P pSyl G) \{0_{G}\} \subseteq z$
11	4 5 7 10	syl3anc	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to \exists z \in (P pSyl G) \{0_{G}\} \subseteq z$
12		rexn0	$⊢ \exists z \in (P pSyl G) \{0_{G}\} \subseteq z \to P pSyl G \neq \emptyset$
13	11 12	syl	$⊢ (G \in Grp \land X \in Fin \land P \in ℙ) \to P pSyl G \neq \emptyset$

Metamath Proof Explorer