Mapping Induced on Power Set is Mapping

Theorem

Let $S$ and $T$ be sets.

Let $\mathcal R \subseteq S \times T$ be a relation on $S \times T$.

Let $\mathcal R^\to: \mathcal P \left({S}\right) \to \mathcal P \left({T}\right)$ be the mapping induced by $\mathcal R$:

$\forall X \in \mathcal P \left({S}\right): \mathcal R^\to \left({X}\right) = \left\{ {t \in T: \exists s \in X: \left({s, t}\right) \in \mathcal R}\right\}$

Then $\mathcal R^\to$ is indeed a mapping.

Proof

Take the general relation $\mathcal R \subseteq S \times T$.

Let $X \subseteq S$, that is $X \in \mathcal P \left({S}\right)$.

Suppose $X = \varnothing$.

Then from Image of Empty Set is Empty Set:

$\mathcal R^\to \left({X}\right) = \varnothing \subseteq T$

Suppose $X = S$.

Then from Image is Subset of Codomain: Corollary 1:

$\mathcal R^\to \left({X}\right) = \operatorname{Im} \left({\mathcal R}\right) \subseteq T$

Finally, suppose $\varnothing \subset X \subset S$.

From Image is Subset of Codomain, again:

$\mathcal R^\to \left({X}\right) \subseteq T$

Now, from the definition of the power set, we have that:

$Y \subseteq T \iff Y \in \mathcal P \left({T}\right)$

We defined $R^\to \subseteq \mathcal P \left({S}\right) \times \mathcal P \left({T}\right)$ such that:

$R^\to: \mathcal P \left({S}\right) \to \mathcal P \left({T}\right): R^\to \left({X}\right) = \left\{ {t \in T: \exists s \in X: \left({s, t}\right) \in \mathcal R}\right\}$

By definition, there is only one $\mathcal R^\to \left({X}\right)$ for any given $X$, and so $R^\to$ is functional.

We have shown that:

$\forall X \subseteq S: \mathcal R^\to \left({X}\right) \in \mathcal P \left({T}\right)$

So:

$\forall X \in \mathcal P \left({S}\right): \exists_1 Y \in \mathcal P \left({T}\right): \mathcal R^\to \left({X}\right) = Y$

So:

$R^\to$ is defined for all $X \in \mathcal P \left({S}\right)$

and therefore $R^\to$ is a mapping.

$\blacksquare$