Set Intersection is Idempotent/Indexed Family

Theorem

Let $\family {F_i}_{i \mathop \in I}$ be a non-empty indexed family of sets.

Suppose that all the sets in the $\family {F_i}_{i \mathop \in I}$ are the same.

That is, suppose that for some set $S$:

$\forall i \in I: F_i = S$

Then:

$\ds \bigcap_{i \mathop \in I} F_i = S$

where $\ds \bigcap_{i \mathop \in I} F_i$ is the intersection of $\family {F_i}_{i \mathop \in I}$.

First we show that:

$\ds \bigcap_{i \mathop \in I} F_i \subseteq S$

Let $x \in \ds \bigcap_{i \mathop \in I} F_i$.

Since $I$ is non-empty, it has an element $k$.

By the definition of intersection, $x \in F_k$.

By the premise, $F_k = S$, so $x \in S$.

Since this holds for all $x \in \ds \bigcap_{i \mathop \in I} F_i$:

$\ds \bigcap_{i \mathop \in I} F_i \subseteq S$

Next we show that:

$\ds S \subseteq \bigcap_{i \mathop \in I} F_i$

Let $x \in S$.

Then for all $i \in I$, $F_i = S$, so $x \in F_i$.

Thus by the definition of intersection:

$x \in \ds \bigcap_{i \mathop \in I} F_i$

Since this holds for all $x \in S$:

$S \subseteq \ds \bigcap_{i \mathop \in I} F_i$

By definition of set equality:

$\ds \bigcap_{i \mathop \in I} F_i = S$

$\blacksquare$