# Direct Image of Intersection with Inverse Image

## Theorem

Let $S$ and $T$ be sets.

Let $f: S \to T$ be a mapping.

Let:

$f^\to: \powerset S \to \powerset T$ denote the direct image mapping of $f$
$f^\gets: \powerset T \to \powerset S$ denote the inverse image mapping of $f$

where $\powerset S$ denotes the power set of $S$.

Then:

$\forall A \in \powerset S, B \in \powerset T: \map {f^\to} {A \cap \map {f^\gets} B} = \map {f^\to} A \cap B$

## Proof

Let $A \in \powerset S, B \in \powerset T$ be arbitrary.

Then:

 $\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}$ $\subseteq$ $\displaystyle \map {f^\to} A \cap \map {f^\to} {\map {f^\gets} B}$ Image of Intersection under Mapping $\displaystyle$ $\subseteq$ $\displaystyle \map {f^\to} A \cap B$ Subset of Codomain is Superset of Image of Preimage

Let $x \in \map {f^\to} A \cap B$.

 $\displaystyle x$ $\in$ $\displaystyle \map {f^\to} A$ Definition of Set Intersection $\text {(1)}: \quad$ $\displaystyle \leadsto \ \$ $\displaystyle x$ $=$ $\displaystyle \map f a$ for some $a \in A$ and: $\displaystyle x$ $\in$ $\displaystyle B$ Definition of Set Intersection $\displaystyle \leadsto \ \$ $\displaystyle \map f a$ $\in$ $\displaystyle B$ from $(1)$ above $\displaystyle \leadsto \ \$ $\displaystyle a$ $\in$ $\displaystyle \map {f^\gets} B$ Definition of Inverse Image Mapping $\displaystyle \leadsto \ \$ $\displaystyle a$ $\in$ $\displaystyle A \cap \map {f^\gets} B$ Definition of Set Intersection $\displaystyle \leadsto \ \$ $\displaystyle \map f a$ $\in$ $\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}$ Definition of Direct Image Mapping $\displaystyle \leadsto \ \$ $\displaystyle x$ $\in$ $\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}$ as $x = \map f a$ $\displaystyle \leadsto \ \$ $\displaystyle \map {f^\to} A \cap B$ $\subseteq$ $\displaystyle \map {f^\to} {A \cap \map {f^\gets} B}$ Definition of Subset

Thus we have:

$\map {f^\to} {A \cap \map {f^\gets} B} \subseteq \map {f^\to} A \cap B$

and:

$\map {f^\to} A \cap B \subseteq \map {f^\to} {A \cap \map {f^\gets} B}$

and so:

$\forall A \in \powerset S, B \in \powerset T: \map {f^\to} {A \cap \map {f^\gets} B} = \map {f^\to} A \cap B$

by definition of set equality.

$\blacksquare$