ThmDex – An index of mathematical definitions, results, and conjectures.
Result R292 on D77: Set union
Subresult of R4736: Disjunction is smallest upper bound
Union is smallest upper bound
Formulation 0
Let $X$ be a D11: Set.
Let $E_j$ be a D11: Set for each $j \in J$ such that
(i) $\bigcup_{j \in J} E_j$ is the D77: Set union of $E = \{ E_j \}_{j \in J}$
Then
(1) \begin{equation} \forall \, i \in J : E_i \subseteq \bigcup_{j \in J} E_j \end{equation}
(2) \begin{equation} \forall \, j \in J : E_j \subseteq X \quad \implies \quad \bigcup_{j \in J} E_j \subseteq X \end{equation}
Proofs
Proof 0
Let $X$ be a D11: Set.
Let $E_j$ be a D11: Set for each $j \in J$ such that
(i) $\bigcup_{j \in J} E_j$ is the D77: Set union of $E = \{ E_j \}_{j \in J}$
The first claim is clear since $E_i$ forms part of the union $\bigcup_{j \in J} E_j$ for each $i \in J$.

Let $E_j$ then be contained in $X$ for each $j \in J$. Let $x \in \bigcup_{j \in J} E_j$. Then there is an index $i \in J$ such that $x$ belongs to $E_i$. Since $E_i \subseteq X$, transitivity of subset relation implies that $x \in X$. Since $x \in \bigcup_{j \in J} E_j$ was arbitrary, this concludes the proof. $\square$