Local slice for a free proper action

Let ${\mathrm{\Phi }}_x:G\to M$ be the orbit map. From ${\mathrm{\Phi }}_x\circ L_g=(y\mapsto g\cdot y)\circ {\mathrm{\Phi }}_x$ and the fact that both outside maps are diffeomorphisms, ${\mathrm{\Phi }}_x$ has constant rank. Its fibre over $x$ is the stabilizer $G_x=\{e\}$ by freeness. If $d({\mathrm{\Phi }}_x{)}_e$ had a nonzero kernel, the constant-rank normal form [F2] would make the local fibre through $e$ positive-dimensional, contradicting that it is a singleton. Thus $d({\mathrm{\Phi }}_x{)}_e$ is injective.

By [F3], choose a complement $N$ to $d({\mathrm{\Phi }}_x{)}_e(T_{e}G)$ in $T_{x}M$. In a chart at $x$, the inverse image of the coordinate subspace corresponding to $N$ is, after shrinking, an embedded submanifold $S_0$ through $x$ with $T_x{S}_0=N$. The differential of $A_0:G\times S_0\to M$, $A_0(g,s)=g\cdot s$, at $(e,x)$ is $(X,v)\mapsto d({\mathrm{\Phi }}_x{)}_{e}X+v$, hence is an isomorphism. By [F2], there are an identity neighborhood $V\subseteq G$ and a neighborhood of $x$ in $S_0$, again denoted $S_0$, on which $A_0{\mathrm{\mid }}_{V\times S_0}$ is a diffeomorphism onto an open neighborhood of $x$.

Choose a compact neighborhood $C$ of $x$ and shrink $S_0$ into its interior. Properness makes $P={\mathrm{\Theta }}^{-1}(C\times C)$ compact. Its projection to $G$ is therefore the compact transporter $K=\{g\in G:gC\cap C\mathrm{\ne }\mathrm{\varnothing }\}\mathrm{.}$ The set $K\setminus V$ is compact by [F4].

For every $g\in K\setminus V$, freeness gives $g\cdot x\mathrm{\ne }x$. Choose disjoint neighborhoods of these two points. Continuity of the action then supplies neighborhoods $O_g$ of $g$ and $N_g$ of $x$ such that $g^{\mathrm{\prime }}{N}_g\cap N_g=\mathrm{\varnothing }$ for all $g^{\mathrm{\prime }}\in O_g$. The $O_g$ cover the compact set $K\setminus V$, so finitely many suffice. Intersect their corresponding $N_g$ and shrink $S_0$ to a submanifold neighborhood $S$ of $x$ inside that finite intersection and inside $C$. Then $gS\cap S=\mathrm{\varnothing }$ for $g\in K\setminus V$; it is also empty for $g\mathrm{\notin }K$ because $S\subseteq C$.

If $gS\cap S\mathrm{\ne }\mathrm{\varnothing }$, step 4.1 gives $g\in V$. For $s,t\in S$ with $g\cdot s=t$, the two points $(g,s)$ and $(e,t)$ of $V\times S_0$ have the same image under the injective local map from step 2.1, so $g=e$ and $s=t$. Consequently $A:G\times S\to G\cdot S$ is bijective.

The differential of $A$ is invertible at every $(g,s)$: at $(e,s)$ this follows after the preceding shrinking from the local diffeomorphism in step 2.1, and arbitrary $g$ follows by translation in the source and the action diffeomorphism in the target. Thus $A$ is a bijective local diffeomorphism, hence a diffeomorphism onto its open image. Its image is saturated by definition and contains $x$. The construction uses only a finite subcover in step 4.1 and no choice principle.