Vtyjkyuk

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 $mathbbF$ and $mathbbG$ are nonempty families of sets and every element of $mathbbF$ is a subset of every element of $mathbbG$. Then $cup mathbbF subseteq cap mathbbG$.

Here's my proof:

Suppose $mathbbF$ and $mathbbG$ are nonempty families of sets, and every element of $mathbbF$ is a subset of every element of $mathbbG$. Now suppose $x in cup mathbbF$. Then there is some set $A$ such that $A in mathbbF$ and $x in A$. Since every element of $mathbbF$ is a subset of every element of $mathbbG$, it follows that $A subseteq cap mathbbG$. Since $x in A$, then $x subseteq cap mathbbG$. But $x$ was an arbitrary element in $cup mathbbF$, so $cup mathbbF subseteq cap mathbbG$.

Comments:

I feel uneasy about the statement “since every element of $mathbbF$ is a subset of every element of $mathbbG$, it follows that $A subseteq cap mathbbG$.” 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:=,xmid forall ycolon (yin Bbb Gto xin y), $$
i.e.,
$$tag1 xinbigcap Bbb Giff forall ycolon (yin Bbb Gto xin y)$$
in analogy to
$$tag2xinbigcup Bbb Fiff exists ycolon (yinBbb Fland xin y). $$
We are given that
$$tag3 forall xcolon(xin Bbb Fto forall ycolon (yinBbb Gto xsubseteq y)),$$
i.e.,
$$tag4 forall xcolon(xin Bbb Fto forall ycolon (yinBbb Gto forall zcolon (zin xto zin y))).$$
Now let $xinbigcup Bbb F$. By $(2)$ there exists $y$ such that $xin y$ and $yin Bbb F$. Then $(4)$ tells us that $forall y'colon (y'inBbb Gto forall zcolon (zin yto zin y'))$. In particular,
$forall y'colon (y'inBbb Gto (xin yto xin y'))$ and, as we do have $xin y$, $$forall y'colon (y'inBbb Gto xin y').$$
According to $(1)$, this means $xin bigcap Bbb G$, as desired.