The preimage theorem for submanifolds under submersions

Fix $p\in F^{-1}(S)$ and put $y:=F(p)$. By [L1], there is a neighbourhood $V$ of $y$ and a local defining submersion $\mathrm{\Phi }:V\to {\mathbb{R}}^c$ for $S$ at $y$. Shrink to an open neighbourhood $U$ of $p$ with $F(U)\subseteq V$, and set $H:=\mathrm{\Phi }\circ F:U\to {\mathbb{R}}^c$. By [L4], $H$ is smooth, and $H^{-1}(0)=U\cap F^{-1}(S)$. For every $x\in U$, [L5] gives $d{H}_x=d{\mathrm{\Phi }}_{F(x)}\circ d{F}_x$; both factors are surjective because $F$ and $\mathrm{\Phi }$ are submersions, so $d{H}_x$ is surjective. Thus $0$ is a regular value of $H$.

By [L2], $U\cap F^{-1}(S)$ is an embedded codimension-$c$ submanifold near $p$. Since $p$ was arbitrary, $F^{-1}(S)$ is embedded of codimension $c$.

Applying [L3] to the regular level set of $H$ gives $T_p(F^{-1}(S))=\ker d{H}_p$. By [L5], $\ker d{H}_p=\ker (d{\mathrm{\Phi }}_y\circ d{F}_p)=(d{F}_p{)}^{-1}(\ker d{\mathrm{\Phi }}_y)$. Applying [L3] again to the regular level set ${\mathrm{\Phi }}^{-1}(0)=V\cap S$ at $y$ gives $\ker d{\mathrm{\Phi }}_y=T_{y}S$, so $T_p(F^{-1}(S))=(d{F}_p{)}^{-1}(T_{y}S)$.

Steps 2.1 and 2.2 prove the theorem.