Preimage of Relation is Subset of Domain

Theorem

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

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

$\Preimg \RR \subseteq S$

Proof

The preimage of $\RR$ is defined as:

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

Hence:

\(\ds s\)

\(\in\)

\(\ds \Preimg \RR\)

\(\ds \leadsto \ \ \)

\(\ds s\)

\(\in\)

\(\ds \Dom \RR\)

Definition of Preimage of Relation

\(\ds \leadsto \ \ \)

\(\ds \Preimg \RR\)

\(\subseteq\)

\(\ds \Dom \RR\)

Subset of Set with Propositional Function

$\blacksquare$