# Restriction of Mapping is its Intersection with Cartesian Product of Subset with Image

## Theorem

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

Let $X \subseteq S$.

Let $f {\restriction_X}$ be the restriction of $f$ to $X$.

Then:

$f {\restriction_X} = f \cap \paren {X \times \Img f}$

where:

$\Img f$ denotes the image of $f$, defined as:
$\Img f = \set {t \in T: \exists s \in S: t = \map f s}$
$X \times \Img f$ denotes the cartesian product of $X$ with $\Img f$.

## Proof

We have:

 $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f {\restriction_X}$ $\displaystyle \leadsto \ \$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f$ Definition of Restriction of Mapping $\, \displaystyle \land \,$ $\displaystyle x$ $\in$ $\displaystyle X$ Definition of $x$ $\, \displaystyle \land \,$ $\displaystyle y$ $\in$ $\displaystyle \Img f$ Definition of Mapping $\displaystyle \leadsto \ \$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f$ Definition of Restriction of Mapping $\, \displaystyle \land \,$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle X \times \Img f$ Definition of Cartesian Product $\displaystyle \leadsto \ \$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f \cap \paren {X \times \Img f}$ Definition of Set Intersection $\displaystyle \leadsto \ \$ $\displaystyle f {\restriction_X}$ $\subseteq$ $\displaystyle f \cap \paren {X \times \Img f}$ Definition of Subset

$\Box$

Then:

 $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f \cap \paren {X \times \Img f}$ $\displaystyle \leadsto \ \$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f$ $\, \displaystyle \land \,$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle X \times \Img f$ Definition of Set Intersection $\displaystyle \leadsto \ \$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f$ $\, \displaystyle \land \,$ $\displaystyle x$ $\in$ $\displaystyle X$ Definition of Cartesian Product $\, \displaystyle \land \,$ $\displaystyle y$ $\in$ $\displaystyle f \sqbrk X$ Definition of Image of Subset under Mapping $\displaystyle \leadsto \ \$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f$ $\, \displaystyle \land \,$ $\displaystyle \tuple {x, y}$ $\in$ $\displaystyle f {\restriction_X}$ Definition of Restriction of Mapping $\displaystyle \leadsto \ \$ $\displaystyle f \cap \paren {X \times \Img f}$ $\subseteq$ $\displaystyle f {\restriction_X}$ Definition of Subset

$\Box$

Thus we have:

 $\displaystyle f {\restriction_X}$ $\subseteq$ $\displaystyle f \cap \paren {X \times \Img f}$ Definition of Subset $\, \displaystyle \land \,$ $\displaystyle f \cap \paren {X \times \Img f}$ $\subseteq$ $\displaystyle f {\restriction_X}$ Definition of Subset $\displaystyle \leadsto \ \$ $\displaystyle f \cap \paren {X \times \Img f}$ $=$ $\displaystyle f {\restriction_X}$ Definition of Set Equality

$\blacksquare$