Showing that $\cup\Bbb F\subseteq\cap\Bbb G$, assuming every member of $\Bbb F$ is a subset of every member of $\Bbb G$

Question

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.

Answer 1

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.