# Equivalence of Definitions of Inverse Image Mapping of Relation

## Theorem

The following definitions of the concept of Inverse Image Mapping of Relation are equivalent:

### Definition 1

The inverse image mapping of $\mathcal R$ is the mapping $\mathcal R^\gets: \powerset T \to \powerset S$ that sends a subset $Y \subseteq T$ to its preimage $\map {\mathcal R^{-1} } Y$ under $\mathcal R$:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \begin {cases} \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} } & : \Img {\mathcal R} \cap Y \ne \O \\ \O & : \Img {\mathcal R} \cap Y = \O \end {cases}$

### Definition 2

The inverse image mapping of $\mathcal R$ is the direct image mapping of the inverse $\mathcal R^{-1}$ of $\mathcal R$:

$\mathcal R^\gets = \paren {\mathcal R^{-1} }^\to: \powerset T \to \powerset S$

That is:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} }$

## Proof

Consider the mapping defined as:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} }$

Let $\Img {\mathcal R} \cap Y = \O$.

Then:

$\forall t \in T: \neg \exists t \in \Img {\mathcal R} \cap Y$

and so:

$\set {s \in S: \exists t \in Y: \tuple {s, t} \in \mathcal R} = \O$

and so:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \begin {cases} \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} } & : \Img f \cap Y \ne \O \\ \O & : \Img f \cap Y = \O \end {cases}$

$\blacksquare$