# Understanding the proof of the theorem that image of an embedding is a submanifold

I am trying to understand the proof of the following theorem in Differential Topology by Guillemin and Pollack (page 17).

Theorem. An embedding $$f:X\to Y$$ maps $$X$$ diffeomorphically onto a submanifold of $$Y$$.

The "difficult" part of the proof shows by contradiction that the image of any open set $$W$$ of $$X$$ is an open subset of $$f(X)$$; this implies that $$f(X)$$ is a manifold. But I do not understand the "trivial" part of the proof in the book:

• It is now trivial to check that $$f:X\to f(X)$$ is a diffeomorphism, for we now know $$f$$ to be a local diffeomorphism from $$X$$ to $$f(X)$$.
• Since it is bijective, the inverse $$f^{-1}:f(X)\to X$$ is well defined
• But locally $$f^{-1}$$ is already known to be smooth.

How do we "now" know that $$f$$ is a local diffeomorphism from $$X$$ to $$f(X)$$ and why "locally $$f^{-1}$$ is already known to be smooth"?

So we know that $$f:X \rightarrow Y$$ is an embedding between two smooth manifolds $$X$$ and $$Y$$, and that it is at least a local diffeomorphism from $$X$$ to its image $$f(X) \subseteq Y$$. Being an embedding, $$f$$ is injective and furthermore $$f$$ by definition is surjective onto its image $$f(X)$$. So there is nothing getting in the way of $$f:X \rightarrow f(X)$$ actually being a global diffeomorphism.
The last two points highlight that since $$f$$ is bijective onto $$f(X)$$, a set-theoretic inverse $$f^{-1}:f(X) \rightarrow X$$ exists, i.e. we haven't said anything yet about continuity, smoothness, etc. However, since $$f$$ is a local diffeomorphism, locally $$f^{-1}$$ is smooth, so now we can say the set-theoretic inverse $$f^{-1}$$ adopts this smoothness from all the local neighborhoods patched together.
• In the proof leading up to that point, it is shown that $f(X)$ is a smooth manifold, hence locally the image of $f$ is smooth. It is also injective globally (hence locally) and surjective globally by definition of the image $f(X)$ (hence locally). So locally $f$ is smooth and invertible, and applying the same reasoning to $f^{-1}$ shows it's locally a diffeomorphism. – BenCWBrown Feb 26 at 16:03