Theorem: Real Line Continuity by Inverse of Mapping

Let $f$ be a real function.
Let the domain of $f$ be open.
Let $f^{-1}$ be the inverse of $f$.
Then $f$ is continuous {{iff}}:
:for every open real set $O$ that overlaps with the image of $f$, the preimage $f^{-1} \sqbrk O$ is open.

Proof:
=== Necessary Condition ===
Let $\Dom f$ be the domain of $f$.
Let $\Img f$ be the image of $f$.
Let $f^{-1} \sqbrk O$ be the preimage of $O$ under $f$.
Thus by definition:
: $\Img f$ is the set of points $q$ in the codomain of $f$ satisfying $q = \map f p$ for a point $p$ in $\Dom f$.
:$f^{-1} \sqbrk O$ is the set of points $p$ in $\Dom f$ such that $\map f p \in O$.
Let $f$ be continuous.
Let $O$ be an open real set that overlaps with $\Img f$.
We need to show that $f^{-1} \sqbrk O$ is open.
$(1): \quad$ It is shown that $f^{-1} \sqbrk O$ is non-empty.
A point $q_1$ exists in $O \cap \Img f$ as $O$ and $\Img f$ overlap.
In particular, $q_1 \in \Img f$.
Therefore, by definition of $\Img f$, a point $p_1$ in $\Dom f$ exists satisfying $\map f {p_1} = q_1$.
Also, $q_1 \in O$, which gives:
{{begin-eqn}}
{{eqn | l = q_1
      | o = \in
      | r = O
}}
{{eqn | ll= \leadsto
      | l = \map f {p_1} 
      | o = \in
      | r = O
      | c = as $\map f {p_1} = q_1$
}}
{{eqn | ll= \leadsto
      | l = p_1 
      | o = \in
      | r = f^{-1} \sqbrk O
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{end-eqn}}
Accordingly, $f^{-1} \sqbrk O$ is non-empty.
$(2): \quad$ It is shown that the function $f$ maps $\openint {x - \delta} {x + \delta}$ into $O$.
Let $x$ be a point in $f^{-1} \sqbrk O$.
This means that $x \in \Dom f$ and $\map f x \in O$.
We know that $f$ is continuous.
Accordingly, $f$ is continuous at $x$ as $x \in \Dom f$.
Let an $\epsilon > 0$ be given.
That $f$ is continuous at $x$, means that:
:a $\delta > 0$ exists such that $\map f y \in \openint {\map f x - \epsilon} {\map f x + \epsilon}$ whenever $y \in \openint {x - \delta} {x + \delta} \cap \Dom f$.
We know that $\map f x \in O$.
Also, $O$ is open.
This allows us to choose $\epsilon \in \R_{>0}$ small enough such that:
:$\openint {\map f x - \epsilon} {\map f x + \epsilon} \subseteq O$
We know that $x \in \Dom f$.
Also, $\Dom f$ is open.
This allows us to choose $\delta \in \R_{>0}$ small enough such that:
:$\openint {x - \delta} {x + \delta} \subseteq \Dom f$
Having chosen $\epsilon$ and $\delta$ in this way, we have, where $f \sqbrk {\openint {x - \delta} {x + \delta} }$ is the image of $\openint {x - \delta} {x + \delta}$ by $f$:
:$f \sqbrk {\openint {x - \delta} {x + \delta} } \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$ as $\map f y \in \openint {\map f x - \epsilon} {\map f x + \epsilon}$ whenever $y \in \openint {x - \delta} {x + \delta}$
which implies:
:$f \sqbrk {\openint {x - \delta} {x + \delta} } \subseteq O$ as $\openint {\map f x - \epsilon} {\map f x + \epsilon} \subseteq O$.
$(3): \quad$ It is shown that the interval $\openint {x - \delta} {x + \delta}$ is a subset of $f^{-1} \sqbrk O$.
Keep in mind that by Subset of Domain is Subset of Preimage of Image:
:$\openint {x - \delta} {x + \delta} \subseteq f^{-1} \sqbrk {f \sqbrk {\openint {x - \delta} {x + \delta} } } $
Continuing by elaborating on $f \sqbrk {\openint {x - \delta} {x + \delta} } \subseteq O$:
{{begin-eqn}}
{{eqn | l = f \sqbrk {\openint {x - \delta} {x + \delta} }
      | o = \subseteq
      | r = O
}}
{{eqn | ll= \leadsto
      | l = f^{-1} \sqbrk {f \sqbrk {\openint {x - \delta} {x + \delta} } }
      | o = \subseteq
      | r = f^{-1} \sqbrk O
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = \openint {x - \delta} {x + \delta}
      | o = \subseteq
      | r = f^{-1} \sqbrk O
      | c = as $\openint {x - \delta} {x + \delta} \subseteq f^{-1} \sqbrk {f \sqbrk {\openint {x - \delta} {x + \delta} } }$
}}
{{end-eqn}}
Because:
:$f \sqbrk {\openint {x - \delta} {x + \delta} } \subseteq O$
it follows that:
:$\openint {x - \delta} {x + \delta} \subseteq f^{-1} \sqbrk O$
Since $x$ is an arbitrary point in $f^{-1} \sqbrk O$, it follows by definition of open set that $f^{-1} \sqbrk O$ is open.
{{qed|lemma}}