[proofplan]
Let $F: M \to N$ be a diffeomorphism and compare it in local coordinates near an arbitrary point $p \in M$. In charts, $F$ becomes a smooth map between open subsets of Euclidean spaces whose inverse is also smooth. The chain rule applied to the two coordinate maps shows that their derivatives are inverse linear maps, so the Euclidean source and target dimensions are equal. These Euclidean dimensions are exactly $\dim M$ and $\dim N$.
[/proofplan]
[step:Choose compatible charts around a point and its image]
Let $m := \dim M$ and $n := \dim N$. Since $M$ is nonempty, choose a point $p \in M$. Let $q := F(p) \in N$.
Choose a coordinate chart $(U_0,\varphi)$ on $M$ with $p \in U_0$ and
\begin{align*}
\varphi: U_0 \to \varphi(U_0) \subset \mathbb{R}^m
\end{align*}
a homeomorphism onto an open subset of $\mathbb{R}^m$. Choose a coordinate chart $(V,\psi)$ on $N$ with $q \in V$ and
\begin{align*}
\psi: V \to \psi(V) \subset \mathbb{R}^n
\end{align*}
a homeomorphism onto an open subset of $\mathbb{R}^n$.
Because $F$ is smooth, it is continuous. Hence
\begin{align*}
U := U_0 \cap F^{-1}(V)
\end{align*}
is an open neighbourhood of $p$ in $M$. Replacing $U_0$ by $U$, we may regard $(U,\varphi|_U)$ as a coordinate chart around $p$ satisfying $F(U) \subset V$.
[/step]
[step:Write the diffeomorphism and its inverse in local coordinates]
Define the local coordinate representative of $F$ by
\begin{align*}
f: \varphi(U) \to \psi(V)
\end{align*}
with
\begin{align*}
f := \psi \circ F \circ (\varphi|_U)^{-1}.
\end{align*}
Since $F(U) \subset V$, this map is well-defined. Since $F$ is smooth and $\varphi,\psi$ are smooth charts, the map $f$ is smooth.
Let
\begin{align*}
W := F(U) \subset V.
\end{align*}
Because $F$ is a homeomorphism, $W$ is open in $N$. Define the local coordinate representative of $F^{-1}$ on $W$ by
\begin{align*}
g: \psi(W) \to \varphi(U)
\end{align*}
with
\begin{align*}
g := \varphi|_U \circ F^{-1} \circ (\psi|_W)^{-1}.
\end{align*}
Since $F^{-1}$ is smooth and $\varphi,\psi$ are smooth charts, the map $g$ is smooth.
By construction, $g$ is the inverse of $f$ after restricting the codomain of $f$ to $\psi(W)$. Thus
\begin{align*}
g \circ f = \operatorname{id}_{\varphi(U)}.
\end{align*}
Also,
\begin{align*}
f \circ g = \operatorname{id}_{\psi(W)}.
\end{align*}
[guided]
The purpose of passing to charts is to convert a statement about manifolds into a statement about Euclidean spaces. We have chosen $(U,\varphi)$ around $p$ and $(V,\psi)$ around $q = F(p)$ so that $F(U) \subset V$. This ensures that the expression $\psi \circ F \circ (\varphi|_U)^{-1}$ is defined on all of $\varphi(U)$.
Define
\begin{align*}
f: \varphi(U) \to \psi(V)
\end{align*}
by
\begin{align*}
f := \psi \circ F \circ (\varphi|_U)^{-1}.
\end{align*}
The domain $\varphi(U)$ is an open subset of $\mathbb{R}^m$, and the target $\psi(V)$ is an open subset of $\mathbb{R}^n$. The map $f$ is smooth because it is a composition of smooth maps in the sense of the definition of a smooth map between manifolds.
Now we also need the inverse map in coordinates. Let
\begin{align*}
W := F(U).
\end{align*}
Since $F$ is a diffeomorphism, it is in particular a homeomorphism, so $W$ is open in $N$. Define
\begin{align*}
g: \psi(W) \to \varphi(U)
\end{align*}
by
\begin{align*}
g := \varphi|_U \circ F^{-1} \circ (\psi|_W)^{-1}.
\end{align*}
This map is smooth because $F^{-1}$ is smooth and the chart maps are smooth.
The definitions are arranged so that $f$ and $g$ undo each other. If $a \in \varphi(U)$, then $(\varphi|_U)^{-1}(a) \in U$, so
\begin{align*}
(g \circ f)(a) = a.
\end{align*}
Thus
\begin{align*}
g \circ f = \operatorname{id}_{\varphi(U)}.
\end{align*}
Similarly, if $b \in \psi(W)$, then $(\psi|_W)^{-1}(b) \in W = F(U)$, so applying $F^{-1}$ returns a point of $U$, and therefore
\begin{align*}
(f \circ g)(b) = b.
\end{align*}
Hence
\begin{align*}
f \circ g = \operatorname{id}_{\psi(W)}.
\end{align*}
[/guided]
[/step]
[step:Differentiate the inverse identities to obtain inverse linear maps]
Let
\begin{align*}
a := \varphi(p) \in \varphi(U).
\end{align*}
Then
\begin{align*}
f(a) = \psi(F(p)) = \psi(q).
\end{align*}
Set
\begin{align*}
b := f(a) \in \psi(W).
\end{align*}
By the chain rule applied to $g \circ f = \operatorname{id}_{\varphi(U)}$ at $a$, we obtain
\begin{align*}
Dg_b \circ Df_a = D(\operatorname{id}_{\varphi(U)})_a.
\end{align*}
The derivative of the identity map on the [open set](/page/Open%20Set) $\varphi(U) \subset \mathbb{R}^m$ is the identity [linear map](/page/Linear%20Map) on $\mathbb{R}^m$, so
\begin{align*}
Dg_b \circ Df_a = \operatorname{id}_{\mathbb{R}^m}.
\end{align*}
By the chain rule applied to $f \circ g = \operatorname{id}_{\psi(W)}$ at $b$, we obtain
\begin{align*}
Df_a \circ Dg_b = D(\operatorname{id}_{\psi(W)})_b.
\end{align*}
The derivative of the identity map on the open set $\psi(W) \subset \mathbb{R}^n$ is the identity linear map on $\mathbb{R}^n$, so
\begin{align*}
Df_a \circ Dg_b = \operatorname{id}_{\mathbb{R}^n}.
\end{align*}
Thus
\begin{align*}
Df_a: \mathbb{R}^m \to \mathbb{R}^n
\end{align*}
is a linear isomorphism with inverse
\begin{align*}
Dg_b: \mathbb{R}^n \to \mathbb{R}^m.
\end{align*}
[/step]
[step:Compare the Euclidean dimensions and conclude]
Since $Df_a: \mathbb{R}^m \to \mathbb{R}^n$ is a linear isomorphism, the vector spaces $\mathbb{R}^m$ and $\mathbb{R}^n$ have the same finite dimension. Therefore
\begin{align*}
m = n.
\end{align*}
By the definitions of $m$ and $n$, this says
\begin{align*}
\dim M = \dim N.
\end{align*}
This proves that dimension is preserved by diffeomorphism.
[/step]
