Union of Set of Singletons

Theorem

Let $S$ be a set.

Let $T = \set {\set x: x \in S}$ be the set of all singletons of elements of $S$.

Then:

$\ds \bigcup T = S$

where $\ds \bigcup T$ denotes the union of $T$.

Proof

Union of $T$ Subset $S$

Let $\ds x \in \bigcup T$.

By definition of union:

$\exists A \in T: x \in A$

By definition of $T$:

$\exists y \in S: A = \set y$

Then by definition of singleton:

$x = y$

Thus $x \in S$.

$\Box$

$S$ Subset Union of $T$

Let $x \in S$.

By definition of $T$:

$\set x \in T$

By Set is Subset of Union/Set of Sets:

$\ds \set x \subseteq \bigcup T$

By definition of singleton:

$x \in \set x$

Thus by definition of subset:

$\ds x \in \bigcup T$

$\Box$

Thus by definition of set equality:

$\ds \bigcup T = S$

$\blacksquare$

Sources

• Mizar article RELSET_2:15