A local isometry from a complete connected manifold has geodesically complete target image

For $q\in O$, choose $p\in M$ with $F(p)=q$. By [F1], some neighbourhood of $p$ maps diffeomorphically onto an open neighbourhood $V$ of $q$ in $N$, and $V\subseteq F(M)=O$. Thus every point of $O$ is interior and $O$ is open. The choice of $p$ instantiates one existential statement for one fixed $q$.

If $O=\mathrm{\varnothing }$, it has no initial tangent vectors and is geodesically complete vacuously by [F2]; the stronger assertion is vacuous as well. Suppose $q\in O$ and fix $w\in T_{q}N$. Choose one $p\in M$ with $F(p)=q$. Since $O$ is open, $T_{q}O=T_{q}N$, and [F1] gives the unique vector $v=(d{F}_p{)}^{-1}w\in T_{p}M\mathrm{.}$

The point $p$ shows that $M$ is nonempty, so [F2] applies to the assumed metric completeness of $M$. By [F3], the maximal source geodesic $\eta :\mathbb{R}\to M$ with initial data $(p,v)$ is therefore defined for every real time.

Regard $F$ first as a map $M\to O$ with the restricted target metric. It is still a local Riemannian isometry by [F1], so [F4] makes $\sigma =F\circ \eta :\mathbb{R}\to O$ a geodesic. It has $\sigma (0)=q$ and ${\sigma }^{\mathrm{\prime }}(0)=d{F}_p(v)=w$. By [F3], the maximal geodesic in $O$ with data $(q,w)$ contains this global geodesic and hence has domain $\mathbb{R}$. Since $(q,w)$ was arbitrary, $O$ is geodesically complete.

Regard the same $\sigma$ as an $N$-valued geodesic. It has the same initial data $(q,w)$, so uniqueness in [F3] identifies it with the maximal $N$-geodesic on that geodesic's domain. Because $\sigma$ itself is defined on all of $\mathbb{R}$, maximality makes the $N$-geodesic global; its value at every time is $F(\eta (t))\in O$. This proves the stronger assertion.

The empty case was settled in step 2.1. In dimension zero, every tangent vector is zero and the relevant geodesics are constant; dimension one is unchanged. The zero vector and both positive and negative infinite-time directions are included because $\eta$ has domain all of $\mathbb{R}$. The statement is one-way and does not infer a covering map. Assumption [A1] is used through [F2] and [F3]; choosing one preimage after fixing $(q,w)$ and applying one inverse linear map require no family-wide choice.