# Direct Image Mapping of Injection is Injection

This page has been identified as a candidate for refactoring.This should be part of an if and only if proof, the other part being Mapping is Injection if its Direct Image Mapping is InjectionUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Theorem

Let $f: S \to T$ be an injection.

Then the direct image mapping of $f$:

- $f^\to: \powerset S \to \powerset T$

is an injection.

## Proof

Suppose $f^\to: \powerset S \to \powerset T$ is not an injection.

Then:

- $\exists Y \in \powerset T: \exists X_1, X_2 \in \powerset S: X_1 \ne X_2 \land \map {f^\to} {X_1} = \map {f^\to} {X_2} = Y$

There are two cases to consider:

- $(1): \quad$ Either $X_1$ or $X_2$ is the empty set
- $(2): \quad$ Neither $X_1$ nor $X_2$ is the empty set.

### Either subset is the empty set

Without loss of generality assume that $X_1 = \O$.

Then, from Image of Empty Set is Empty Set:

- $Y = \map {f^\to} {X_1} = \O$

But that means:

- $\map {f^\to} {X_2} = \O$

Now $X_1 \ne X_2$, so $X_2 \ne \O$.

Thus:

- $\exists x_2 \in X_2: \neg \exists y \in T: \map f {x_2} = y$

which means that $f$ is not even a mapping, let alone an injection.

The same argument applies if $X_2$ is empty.

$\Box$

### Neither subset is the empty set

Now, assume that neither $X_1$ nor $X_2$ is the empty set.

As $X_1 \ne X_2$, there must be at least one element in either one which is not in the other.

Without loss of generality assume that $\exists x_1 \in X_1: x_1 \notin X_2$.

Now suppose $\map f {x_1} = y \in Y$.

However, as $\map {f^\to} {X_2} = Y$, there must be some $x_2 \in X_2$ such that $\map f {x_2} = y \in Y$.

So:

- $\exists x_1 \ne x_2 \in S: \map f {x_1} = \map f {x_2}$

which means, by definition, that $f$ is not injective.

Thus, if $f^\to: \powerset S \to \powerset T$ is not an injection then neither is $f: S \to T$.

Thus, by the Rule of Transposition, the result follows.

$\blacksquare$