[proofplan] We first prove that distance preservation forces $f$ to be injective: two points with the same image have distance zero in $X$, hence are equal by the definiteness axiom of a metric. Since surjectivity is assumed, this gives bijectivity and therefore a well-defined inverse map $f^{-1}:Y\to X$. We then compute distances between inverse images by writing each point of $Y$ as the image of its inverse preimage. Finally, surjectivity of $f^{-1}$ follows by applying the inverse to points of the form $f(x)$. [/proofplan] [step:Prove that distance preservation makes $f$ injective] Let $x,x'\in X$ satisfy $f(x)=f(x')$. Since $f$ preserves distances, \begin{align*} d_X(x,x')=d_Y(f(x),f(x')). \end{align*} Because $f(x)=f(x')$, the metric axiom on $(Y,d_Y)$ gives \begin{align*} d_Y(f(x),f(x'))=d_Y(f(x),f(x))=0. \end{align*} Thus $d_X(x,x')=0$. By the definiteness axiom of the metric $d_X$, this implies $x=x'$. Therefore $f$ is injective. [guided] We must show that different points of $X$ cannot be sent to the same point of $Y$. Take arbitrary points $x,x'\in X$ and assume that their images agree: \begin{align*} f(x)=f(x'). \end{align*} The hypothesis that $f$ is an isometry in the distance-preserving sense says that every pair of points in $X$ has the same distance as its image pair in $Y$. Applying that hypothesis to the pair $(x,x')$, we get \begin{align*} d_X(x,x')=d_Y(f(x),f(x')). \end{align*} Since $f(x)=f(x')$, the right-hand side is the distance in $Y$ from a point to itself: \begin{align*} d_Y(f(x),f(x'))=d_Y(f(x),f(x))=0. \end{align*} Therefore \begin{align*} d_X(x,x')=0. \end{align*} The definiteness axiom for the metric $d_X$ states that $d_X(a,b)=0$ holds exactly when $a=b$. Applying this axiom with $a=x$ and $b=x'$, we obtain $x=x'$. Hence $f$ is injective. [/guided] [/step] [step:Use surjectivity and injectivity to define the inverse map] By hypothesis, $f:X\to Y$ is surjective. The preceding step shows that $f$ is injective. Hence $f$ is bijective, and its inverse is a well-defined map \begin{align*} f^{-1}:Y\to X. \end{align*} For every $y\in Y$, the element $f^{-1}(y)\in X$ is the unique point satisfying \begin{align*} f(f^{-1}(y))=y. \end{align*} For every $x\in X$, bijectivity also gives \begin{align*} f^{-1}(f(x))=x. \end{align*} [/step] [step:Compute distances after applying the inverse] Let $y,y'\in Y$. Define $x:=f^{-1}(y)\in X$ and $x':=f^{-1}(y')\in X$. By the defining property of the inverse map, \begin{align*} f(x)=y \end{align*} and \begin{align*} f(x')=y'. \end{align*} Using the distance-preserving property of $f$ on the pair $(x,x')$, we obtain \begin{align*} d_X(f^{-1}(y),f^{-1}(y'))=d_X(x,x')=d_Y(f(x),f(x'))=d_Y(y,y'). \end{align*} Since $y,y'\in Y$ were arbitrary, $f^{-1}$ preserves distances on all of $Y$. [/step] [step:Show that the inverse map is surjective] Let $x\in X$. Define $y:=f(x)\in Y$. Since $f^{-1}$ is the inverse of $f$, \begin{align*} f^{-1}(y)=f^{-1}(f(x))=x. \end{align*} Thus every $x\in X$ lies in the image of $f^{-1}:Y\to X$, so $f^{-1}$ is surjective. Combining this with the distance preservation proved above, $f^{-1}$ is a surjective isometry. [/step]