I'm a little new when it comes to proof writing and was wondering if someone could help me check if my proof to the following theorem is a valid one:
Theorem: Suppose $\mathbb{F}$ and $\mathbb{G}$ are nonempty families of sets and every element of $\mathbb{F}$ is a subset of every element of $\mathbb{G}$. Then $\cup \mathbb{F} \subseteq \cap \mathbb{G}$.
Here's my proof:
Suppose $\mathbb{F}$ and $\mathbb{G}$ are nonempty families of sets, and every element of $\mathbb{F}$ is a subset of every element of $\mathbb{G}$. Now suppose $x \in \cup \mathbb{F}$. Then there is some set $A$ such that $A \in \mathbb{F}$ and $x \in A$. Since every element of $\mathbb{F}$ is a subset of every element of $\mathbb{G}$, it follows that $A \subseteq \cap \mathbb{G}$. Since $x \in A$, then $x \subseteq \cap \mathbb{G}$. But $x$ was an arbitrary element in $\cup \mathbb{F}$, so $\cup \mathbb{F} \subseteq \cap \mathbb{G}$.
Comments:
I feel uneasy about the statement “since every element of $\mathbb{F}$ is a subset of every element of $\mathbb{G}$, it follows that $A \subseteq \cap \mathbb{G}$.” Is this a valid logical deduction?
Thanks in advance for the help! Sorry if this question seems kind of simple — I just want to make sure my thought process is correct.
The deduction can become valid and can be treated more formally (and that may also mean with less feelings of unease) as soon as we introduce a definition of the $\bigcap$ symbol, which ought to be in class-builder notation $$\bigcap \Bbb G:=\{\,x\mid \forall y\colon (y\in \Bbb G\to x\in y)\,\} $$ i.e., $$\tag1 x\in\bigcap \Bbb G\iff \forall y\colon (y\in \Bbb G\to x\in y)$$ in analogy to $$\tag2x\in\bigcup \Bbb F\iff \exists y\colon (y\in\Bbb F\land x\in y). $$ We are given that $$\tag3 \forall x\colon(x\in \Bbb F\to \forall y\colon (y\in\Bbb G\to x\subseteq y)),$$ i.e., $$\tag4 \forall x\colon(x\in \Bbb F\to \forall y\colon (y\in\Bbb G\to \forall z\colon (z\in x\to z\in y))).$$ Now let $x\in\bigcup \Bbb F$. By $(2)$ there exists $y$ such that $x\in y$ and $y\in \Bbb F$. Then $(4)$ tells us that $\forall y'\colon (y'\in\Bbb G\to \forall z\colon (z\in y\to z\in y'))$. In particular, $\forall y'\colon (y'\in\Bbb G\to (x\in y\to x\in y'))$ and, as we do have $x\in y$, $$\forall y'\colon (y'\in\Bbb G\to x\in y').$$ According to $(1)$, this means $x\in \bigcap \Bbb G$, as desired.