Set Union is Self-Distributive/General Result

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\family {\mathbb S_i}_{i \mathop \in I}$ be an $I$-indexed family of sets of sets.

Then:

$\ds \bigcup_{i \mathop \in I} \bigcup \mathbb S_i = \bigcup \bigcup_{i \mathop \in I} \mathbb S_i$


Proof

By the definition of set union, we have:

$\ds \forall i \in I: \forall S \in \mathbb S_i: S \in \bigcup_{j \mathop \in I} \mathbb S_j$

Hence, by Set is Subset of Union: General Result:

$\ds \forall i \in I: \forall S \in \mathbb S_i: S \subseteq \bigcup \bigcup_{j \mathop \in I} \mathbb S_j$

By Union is Smallest Superset: General Result, it follows that:

$\ds \forall i \in I: \bigcup \mathbb S_i \subseteq \bigcup \bigcup_{j \mathop \in I} \mathbb S_j$

Therefore, by Union is Smallest Superset: Family of Sets, we conclude that:

$\ds \bigcup_{i \mathop \in I} \bigcup \mathbb S_i \subseteq \bigcup \bigcup_{j \mathop \in I} \mathbb S_j$


By Set is Subset of Union General Result and then Set is Subset of Union of Family, we have:

$\ds \forall i \in I: \forall S \in \mathbb S_i: S \subseteq \bigcup \mathbb S_i \subseteq \bigcup_{j \mathop \in I} \bigcup \mathbb S_j$

Because $\subseteq$ is transitive, we can apply the definition set union to conclude that:

$\ds \forall S \in \bigcup_{i \mathop \in I} \mathbb S_i: S \subseteq \bigcup_{j \mathop \in I} \bigcup \mathbb S_j$

Hence, by Union is Smallest Superset: General Result:

$\ds \bigcup \bigcup_{i \mathop \in I} \mathbb S_i \subseteq \bigcup_{j \mathop \in I} \bigcup \mathbb S_j$


By definition of set equality, the result follows.

$\blacksquare$