ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2080 on D77: Set union
Union is upper bound for intersection
Formulation 0
Let $E_j$ be a D11: Set for each $j \in J$.
Then
(1) $\bigcap_{j \in J} E_j \subseteq \bigcup_{j \in J} E_j$
(2) $\bigcap_{j \in J} E_j = \bigcup_{j \in J} E_j$ if and only if $E_j = E$ for every $j \in J$
Proofs
Proof 0
Let $E_j$ be a D11: Set for each $j \in J$.
Let $x \in \bigcap_{j \in J} E_j$. Then $x \in E_j$ for every $j \in J$. Thus there exists an index $i \in J$ such that $x \in E_i$ and therefore $x \in \bigcup_{j \in J} E_j$.

If $E_j = E$ for every $j \in J$, then both the union $\bigcup_{j \in J} E_j$ and $\bigcap_{j \in J} E_j$ are equal to $E$ and therefore equal. Conversely, suppose that $\bigcap_{j \in J} E_j = \bigcup_{j \in J} E_j$. Suppose to the contrary that there are indices $i, j \in J$ such that $E_i \neq E_j$. Then, by definition, one contains an element which the other does not. Without loss of generality, suppose that $x \in E_i$ such that $x \not\in E_j$. Then $x \in \bigcup_{j \in J} E_j$, but $x \not\in \bigcap_{j \in J} E_j$, which contradicts the assumption that the union and the intersection are equal. Therefore, $E_i = E_j$ for every $i, j \in J$. $\square$