Prove that $B\cup(\bigcap \mathcal F)=\bigcap_{A\in \mathcal F}(B\cup A)$. Not a duplicate of
$\cap_{A \in \mathcal{F}}(B \cup A) \subseteq B \cup (\cap \mathcal{F})$
This is exercise $3.5.16.b$ from the book How to Prove it by Velleman $($$2^{nd}$ edition$)$:
Suppose $\mathcal F$ is a nonempty family of sets and $B$ is a set. Prove that $B\cup(\bigcap \mathcal F)=\bigcap_{A\in \mathcal F}(B\cup A)$.
Here is my proof:
$(\rightarrow)$ Let $x$ be an arbitrary element of $B\cup(\bigcap\mathcal F)$. Let $A$ be an arbitrary element of $\mathcal F$. Now we consider two different cases.
Case $1.$ Suppose $x\in B$ and so $x\in B\cup A$.
Case $2.$ Suppose $x\in\bigcap\mathcal F$. From $x\in\bigcap\mathcal F$ and $A\in \mathcal F$, $x\in A$ and so $x\in B\cup A$.
Since the above cases are exhaustive, $x\in B\cup A$. Thus if $A\in\mathcal F$ then $x\in B\cup A$. Since $A$ is arbitrary, $\forall A(A\in\mathcal F\rightarrow x\in B\cup A)$ and so $x\in\bigcap_{A\in\mathcal F}(B\cup A)$. Therefore if $x\in B\cup(\bigcap\mathcal F)$ then $x\in\bigcap_{A\in\mathcal F}(B\cup A)$. Since $x$ is arbitrary, $\forall x\Bigr(x\in B\cup(\bigcap\mathcal F)\rightarrow x\in\bigcap_{A\in\mathcal F}(B\cup A)\Bigr)$ and so $B\cup(\bigcap \mathcal F)\subseteq\bigcap_{A\in \mathcal F}(B\cup A)$.
$(\leftarrow)$ Let $x$ be an arbitrary element of $\bigcap_{A\in\mathcal F}(B\cup A)$. We consider two different cases.
Case $1.$ Suppose $x\in\bigcap\mathcal F$. Therefore $x\in B\cup(\bigcap\mathcal F)$.
Case $2.$ Suppose $x\notin \bigcap\mathcal F$. So we can choose some $A_0$ such that $A_0\in\mathcal F$ and $x\notin A_0$. From $x\in\bigcap_{A\in\mathcal F}(B\cup A)$ and $A_0\in\mathcal F$, $x\in B\cup A_0$. From $x\in B\cup A_0$ and $x\notin A_0$, $x\in B$. Therefore $x\in B\cup(\bigcap\mathcal F)$.
Since the above cases are exhaustive, $x\in B\cup(\bigcap\mathcal F)$. Therefore if $x\in\bigcap_{A\in\mathcal F}(B\cup A)$ then $x\in B\cup(\bigcap\mathcal F)$. Since $x$ is arbitrary, $\forall x\Bigr(x\in\bigcap_{A\in\mathcal F}(B\cup A)\rightarrow x\in B\cup(\bigcap\mathcal F)\Bigr)$ and so $\bigcap_{A\in \mathcal F}(B\cup A)\subseteq B\cup(\bigcap \mathcal F)$.
Ergo $B\cup(\bigcap \mathcal F)=\bigcap_{A\in \mathcal F}(B\cup A)$. $Q.E.D.$
Is my proof valid$?$
Thanks for your attention.
 A: It’s correct, but Case $1$ of the second part is incomplete: given the level of detail that you’re using elsewhere in the proof, you really should justify the unstated assumption that $\bigcap\mathcal{F}\subseteq\bigcap_{A\in\mathcal{F}}(B\cup A)$. I would reorganize the second part altogether (and shorten it!):

Let $x\in\bigcap_{A\in\mathcal{F}}(B\cup A)$ be arbitrary; then $x\in B\cup A$ for each $A\in\mathcal{F}$. If $x\in B$, then certainly $x\in B\cup\bigcap\mathcal{F}$. If $x\notin B$, then $x\in A$ for each $A\in\mathcal{F}$, so $x\in\bigcap\mathcal{F}$, and again $x\in B\cup\bigcap\mathcal{F}$. Thus, $\bigcap_{A\in\mathcal{F}}(B\cup A)\subseteq B\cup\bigcap\mathcal{F}$.

Further explanation as requested: To begin the second part you assume that $x\in\bigcap_{A\in\mathcal{F}}(B\cup A)$, which is fine. You then consider the cases $x\in\bigcap\mathcal{F}$ and $x\notin\bigcap\mathcal{F}$, but it’s not immediately clear why these are relevant. If there is to be a division into cases at this point, one would expect the cases to derive fairly straightforwardly from the assumption that $x\in\bigcap_{A\in\mathcal{F}}(B\cup A)$, just as in the first part your two cases derive naturally from the assumption that $x\in B\cup\bigcap\mathcal{F}$.
That’s why I first drew the immediate conclusion from $x\in\bigcap_{A\in\mathcal{F}}(B\cup A)$ that $x\in B\cup A$ for each $A\in\mathcal{F}$. Now, because we’re dealing with a union, it’s easy to see what the natural cases are: either $x\in B$, or $x\in A$ for each $A\in\mathcal{F}$. And those two cases match up perfectly with the structure of the target set $B\cup\bigcap\mathcal{F}$,
