Intersection is Idempotent

Theorem

$S \cap S = S$

Indexed Family

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}$.

Proof

 $\ds x$ $\in$ $\ds S \cap S$ $\ds \leadstoandfrom \ \$ $\ds x \in S$ $\land$ $\ds x \in S$ Definition of Set Intersection $\ds \leadstoandfrom \ \$ $\ds x$ $\in$ $\ds S$ Rule of Idempotence: Conjunction

$\blacksquare$