Image of Domain of Relation is Image Set

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $S$ and $T$ be sets.

Let $\RR \subseteq S \times T$ be a relation.


The image of the domain of $\RR$ is the image set of $\RR$:

$\RR \sqbrk {\Dom \RR} = \Img \RR$

where $\Img \RR$ is the image of $\RR$.


Proof

Let $y \in \RR \sqbrk {\Dom \RR}$.

\(\ds y\) \(\in\) \(\ds \RR \sqbrk {\Dom \RR}\)
\(\ds \leadsto \ \ \) \(\ds \exists x \in \Dom \RR: \, \) \(\ds \tuple {x, y}\) \(\in\) \(\ds \RR\) Definition of Image of Subset under Relation
\(\ds \leadsto \ \ \) \(\ds y\) \(\in\) \(\ds \Img \RR\) Definition of Image of Relation
\(\ds \leadsto \ \ \) \(\ds \RR \sqbrk {\Dom \RR}\) \(\subseteq\) \(\ds \Img \RR\) Definition of Subset


Let $y \in \Img \RR$.

\(\ds y\) \(\in\) \(\ds \Img \RR\)
\(\ds \leadsto \ \ \) \(\ds \exists x \in S: \, \) \(\ds \tuple {x, y}\) \(\in\) \(\ds \RR\) Definition of Image of Relation
\(\ds \leadsto \ \ \) \(\ds y\) \(\in\) \(\ds \RR \sqbrk {\Dom \RR}\) Definition of Domain of Relation
\(\ds \leadsto \ \ \) \(\ds \Img \RR\) \(\subseteq\) \(\ds \RR \sqbrk {\Dom \RR}\) Definition of Subset


The result follows by definition of set equality.

$\blacksquare$