Sylow I: every finite group has a Sylow $p$-subgroup

Argue by strong induction [L6] on $\mathrm{\mid }G\mathrm{\mid }$, the induction statement being that every finite group of order $n$ has a subgroup of order $p^a$ whenever $n=p^{a}m$ with $p\nmid m$. Let $\mathrm{\Omega }$ be the set of subsets of $G$ of size $p^a$ and let $G$ act on $\mathrm{\Omega }$ by left translation, $g\cdot A:=gA$; this is an action, and $\mathrm{\mid }gA\mathrm{\mid }=\mathrm{\mid }A\mathrm{\mid }$ because left translation is a bijection of $G$. Counting subsets gives $\mathrm{\mid }\mathrm{\Omega }\mathrm{\mid }=\left(\genfrac{}{}{0px}{}{p^{a}m}{p^a}\right)$, so [L2] yields $v_p(\mathrm{\mid }\mathrm{\Omega }\mathrm{\mid })=0$, that is $p\nmid \mathrm{\mid }\mathrm{\Omega }\mathrm{\mid }$.

By [L7] the orbits partition $\mathrm{\Omega }$, so $\mathrm{\mid }\mathrm{\Omega }\mathrm{\mid }$ is the sum of the orbit sizes. Were $p$ to divide every orbit size it would divide $\mathrm{\mid }\mathrm{\Omega }\mathrm{\mid }$, so some orbit $\mathcal{O}$ has $p\nmid \mathrm{\mid }\mathcal{O}\mathrm{\mid }$. Choose $A\in \mathcal{O}$ and put $H=G_A=\{g\in G:gA=A\}$. The bijection of [L3] between $G\mathrm{/}H$ and $\mathcal{O}$ gives $\mathrm{\mid }\mathcal{O}\mathrm{\mid }=[G:H]$, so [L4] gives $p^{a}m=\mathrm{\mid }G\mathrm{\mid }=\mathrm{\mid }H\mathrm{\mid }\mathrm{\mid }\mathcal{O}\mathrm{\mid }$; since $p\nmid \mathrm{\mid }\mathcal{O}\mathrm{\mid }$, the full power $p^a$ divides $\mathrm{\mid }H\mathrm{\mid }$.

Suppose $H=G$. Then $gA=A$ for every $g\in G$, so for any $x\in A$ the set $A$ contains $Gx=G$, whence $A=G$ and $p^a=\mathrm{\mid }A\mathrm{\mid }=\mathrm{\mid }G\mathrm{\mid }=p^{a}m$. Thus $m=1$ and $G$ itself is a subgroup of order $p^a$.

Suppose instead $H\mathrm{\ne }G$, so $\mathrm{\mid }H\mathrm{\mid }<\mathrm{\mid }G\mathrm{\mid }$. By [L5], $\mathrm{\mid }H\mathrm{\mid }$ divides $p^{a}m$; writing $\mathrm{\mid }H\mathrm{\mid }=p^b{m}^{\mathrm{\prime }}$ with $p\nmid m^{\mathrm{\prime }}$, step 2.1 gives $b\ge a$, while $p^b\mid p^{a}m$ with $p\nmid m$ gives $b\le a$. Hence $\mathrm{\mid }H\mathrm{\mid }=p^a{m}^{\mathrm{\prime }}$ with $p\nmid m^{\mathrm{\prime }}$, and the induction hypothesis applied to $H$ supplies a subgroup of $H$ of order $p^a$, which is a subgroup of $G$.

Steps 3.1 and 3.2 are exhaustive, so $G$ has a subgroup $P$ of order $p^a$, and $\mathrm{\mid }P\mathrm{\mid }$ is the largest power of $p$ dividing $\mathrm{\mid }G\mathrm{\mid }$, so $P$ is a Sylow $p$-subgroup by [L1]. At $a=0$ the argument returns the trivial subgroup, of order $p^0=1$; for the trivial group $\mathrm{\mid }G\mathrm{\mid }=1$ this is $G$ itself, and $m=1$ is the case settled in step 3.1.