Theorem: Restriction of Inverse is Inverse of Restriction

Let $S_1$ and $S_2$ be sets.
Let $f: S_1 \to S_2$ be a bijection.
Let $S \subseteq S_1$ be a subset of $S_1$.
Let $f \sqbrk S$ be the image of $S$ under $f$.
Let $f^{-1}$ be the inverse of $f$.
Let $f {\restriction_{S \mathop \times f \sqbrk S}}$ be the restriction of $f$ to $S \times f \sqbrk S$.
Let $f^{-1} {\restriction_{f \sqbrk S \mathop \times S}}$ be the restriction of $f^{-1}$ to $f \sqbrk S \times S$.
Then:
:$f {\restriction_{S \mathop \times f \sqbrk S} }$ is a bijection
and:
:$\paren {f {\restriction_{S \mathop \times f \sqbrk S} } }^{-1} = f^{-1} {\restriction_{f \sqbrk S \mathop \times S}}$

Proof:
Let $y \in f \sqbrk S$.
By the definition of image:
:$\exists z \in S : \map f z = y$
Since $f$ is a bijection, $f^{-1}$ is a mapping.
Let $x = \map {f^{-1} } y$.
{{AimForCont}} $x \notin S$.
Suppose that $x = z$.
Then $x \in S$.
Thus $x \ne z$.
By the definition of inverse mapping:
:$\map f x = y$
By Equality is Transitive:
:$\map f x = \map f z$
Thus, $f$ is not an injection.
Thus, $f$ is not a bijection.
This contradicts the assumption.
Therefore, $x \in S$.
By the definition of restriction of mapping:
:$\map {f {\restriction_{S \mathop \times f \sqbrk S} } } x = \map f x$
By Equality is Transitive:
:$\map {f {\restriction_{S \mathop \times f \sqbrk S} } } x = y$
{{AimForCont}} there exists a $w \in S$ such that $w \ne x$ and $\map {f {\restriction_{S \mathop \times f \sqbrk S} } } w = y$.
By the definition of restriction of mapping:
:$\map {f {\restriction_{S \mathop \times f \sqbrk S} } } w = \map f w$
By Equality is Transitive:
:$\map f w = y$
By Equality is Transitive:
:$\map f w = \map f\ x$
Thus, $f$ is not an injection.
Thus, $f$ is not a bijection.
This contradicts the assumption.
Therefore, there exists a unique $x \in S$ such that:
:$\map {f {\restriction_{S \mathop \times f \sqbrk S} } } x = y$
Since $y \in f \sqbrk S$ was arbitrary, $f {\restriction_{S \mathop \times f \sqbrk S} }$ is a bijection.
Thus, ${\left(f {\restriction_{S \mathop \times f \sqbrk S} }\right)}^{-1}$ is a mapping.
Let $x' = {\left(f {\restriction_{S \mathop \times f \sqbrk s} }\right)}^{-1}\left({y}\right)$.
By the definition of inverse mapping:
:$\map {f {\restriction_{S \mathop \times f \sqbrk S} } } {x'} = y$
By the definition of restriction of mapping, we have $\map f {x'} = y$.
Suppose that $x' \ne x$.
By Equality is Transitive:
:$\map f {x'}= \map f x$
Thus, $f$ is not an injection.
Thus, $f$ is not a bijection.
This contradicts the assumption.
Therefore, $x' = x$.
By Equality is Transitive:
:$\map {f^{-1} } y = \map {\paren {f {\restriction_{S \mathop \times f \sqbrk S} } }^{-1} } y$
By the definition of restriction of mapping:
:$\map {f^{-1} {\restriction_{f \sqbrk S \mathop \times S} } } y = \map {f^{-1} } y$
By Equality is Transitive:
:$\map {\paren {f {\restriction_{S \mathop \times f \sqbrk S} } }^{-1} } y = \map {f^{-1} {\restriction_{f \sqbrk S \mathop \times S} } } y$
Since $y \in f \sqbrk S$ was arbitrary:
:$\paren {f {\restriction_{S \mathop \times f \sqbrk S} } }^{-1} = f^{-1} {\restriction_{f \sqbrk S \mathop \times S} }$
{{qed}}
Category:Restrictions
Category:Inverse Mappings
6cg436ym52t97hgklzb9rnlxqpnyokv