Union of Union of Relation is Union of Domain with Image

Theorem

Let $V$ be a basic universe.

Let $\RR \subseteq V \times V$ be a relation.

Let $\Dom \RR$ denote the domain of $\RR$.

Then:

$\map \bigcup {\bigcup \RR} = \Dom \RR \cup \Img \RR$

where:

$\bigcup \RR$ denotes the union of $\RR$

$\Dom \RR$ denotes the domain of $\RR$

$\Img \RR$ denotes the image of $\RR$.

Proof

\(\ds \bigcup \RR\)

\(=\)

\(\ds \set {z: \exists \tuple {x, y} \in \RR: z \in \tuple {x, y} }\)

Definition of Union of Class

\(\ds \)

\(=\)

\(\ds \set {z: \exists \set {\set x, \set {x, y} } \in \RR: z \in \tuple {x, y} }\)

Definition of Kuratowski Formalization of Ordered Pair

\(\ds \)

\(=\)

\(\ds \set {\set x, \set {x, y}: x \in \Dom \RR, \tuple {x, y} \in \RR}\)

\(\ds \leadsto \ \ \)

\(\ds \map \bigcup {\bigcup \RR}\)

\(=\)

\(\ds \set {z: \exists X \in \bigcup \RR: z \in X}\)

Definition of Union of Class

\(\ds \)

\(=\)

\(\ds \set {x, y: x \in \Dom \RR, \tuple {x, y} \in \RR}\)

Definition of $\bigcup \RR$

\(\ds \)

\(=\)

\(\ds \set {x, y: x \in \Dom \RR, y \in \Img \RR}\)

Definition of Image of Relation

\(\ds \)

\(=\)

\(\ds \set {x: x \in \Dom \RR} \cup \set {y: y \in \Img \RR}\)

Definition of Class Union

\(\ds \)

\(=\)

\(\ds \Dom \RR \cup \Img \RR\)

$\blacksquare$