Preimage of Relation is Subset of Domain

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}$ $\displaystyle \leadsto \ \$ $\displaystyle s$ $\in$ $\displaystyle \Dom {\mathcal R}$ Definition of Preimage of Relation $\displaystyle \leadsto \ \$ $\displaystyle \Preimg {\mathcal R}$ $\subseteq$ $\displaystyle \Dom {\mathcal R}$ Subset of Set with Propositional Function

$\blacksquare$