Why is the image of a subanalytic set through a proper analytic map subanalytic? Recall the following definitions, where $M$ and $N$ are real analytic manifolds:
A subset $A\subseteq M$ is called semianalytic  if for every $m\in M$ there is an open $U_m\subseteq M$ such that $U_m\cap A$ is a finite union of sets of the form $\{x\in U_m\mid f(x)=0\}$ or $\{x\in U_m\mid g(x)>0\}$, for real analytic functions $f,g\colon U_m\to \Bbb R$.
A subset $A\subseteq M$ is called subanalytic if for every $m\in M$ there is an open $U_m\subseteq M$ such that $U_m\cap A=\pi_M(S)$ where $L$ is a real analytic manifold, $S\subseteq M\times L$ is a relatively compact semianalytic set and $\pi_M\colon M\times L\to M$ is the projection on the first component.
Various authors state that clearly the image of a subanalytic set $A\subseteq M$ through a proper analytic function $f\colon M\to N$ is again subanalytic, but I'm not seeing how to prove this fact. I think I should use the fact that $\mathrm{graph}(f)\subseteq M\times N$ is analytic to locally write $f(A)$ as a projection of semianalytic sets, but this might already be wrong.
Why does the fact above hold?
 A: Your intuition is correct. First, we make a reduction: let $n\in N$ with a relatively-compact semianalytic neighborhood $V_n\subset N$ (for instance, embed $N\subset\Bbb R^P$ and take the intersection of some $\varepsilon$-ball about $n$ with $N$). Then $f^{-1}(V_n):= U\subset M$ is also relatively compact as $f$ is proper, so it can be covered by finitely many $U_m$ as in the definition of a subanalytic set on $M$. Letting $S_m$ and $L_m$ be the corresponding sets for each $U_m$, we declare $L$ to be $\bigsqcup_m L_m$ and $S=\bigsqcup S_m$ so that $A\cap U$ is the projection of the relatively compact semianalytic set $S\subset L \times M$ on to $M$. (If you're someone who cares about manifolds being connected, embed these disjoint unions analytically in some big-enough $\Bbb R^n$.)
Now I claim that the set $(S\times V_n)\cap (L\times \Gamma_f)\subset L\times M\times N$ (where $\Gamma_f\subset M\times N$ is the graph) is semianalytic: it's cut out by the equations $n=f(m)$ and the equations and inequations defining $S\subset L$ and $V_n\subset N$. Being the intersection of a relatively compact set and a closed set, it's also relatively compact. Finally, the intersection of $V_n$ with the projection of $(S\times V_n)\cap (L\times \Gamma_f)$ on to $N$ gives exactly $f(A)\cap V_n$, and by definition we see that $f(A)$ is subanalytic.
