Preimage of Relation is Subset of Domain

From ProofWiki
Jump to: navigation, search

Theorem

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


Then the preimage of $\mathcal R$ is a subset of its domain:

$\Preimg {\mathcal R} \subseteq S$


Proof

The preimage of $\mathcal R$ is defined as:

$\Preimg {\mathcal R} = \set {s \in \Dom {\mathcal R}: \exists t \in \Rng {\mathcal R}: \tuple {s, t} \in \mathcal R}$


Hence:

\(\displaystyle s\) \(\in\) \(\displaystyle \Preimg {\mathcal R}\) $\quad$ $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle s\) \(\in\) \(\displaystyle \Dom {\mathcal R}\) $\quad$ Definition of Preimage of Relation $\quad$
\(\displaystyle \leadsto \ \ \) \(\displaystyle \Preimg {\mathcal R}\) \(\subseteq\) \(\displaystyle \Dom {\mathcal R}\) $\quad$ Subset of Set with Propositional Function $\quad$

$\blacksquare$