Set theory proof on injections, sequences of sets I'm trying to practice my proof-writing skills. At the moment I trying to prove the following proposition:
For every one-to-one function $\: f:X \to Y \:$, and sequence of sets $\: B_n \subseteq X \:$, 
$$\: f \left[\bigcap_{n=0}^\infty B_n \right] = \bigcap_{n=0}^\infty f \left[B_n\right].$$
I was hoping to get some feedback on the proof. I suppose both in terms of content and form. Thanks!
Proof.
First, for some arbitrary $y \in Y$, suppose that $y \in f\left[ \bigcap_{n=0}^\infty B_n\right]$. 
Then, by definition, $\exists x \in \bigcap_{n=0}^\infty B_n$ such that $f(x) = y$. 
And, because we have an intersection, it follows that $\exists x : \forall n\, (x \in B_n)$.
In that case, $y \in f\left[B_n\right]$ for each $n$. 
And therefore, $y \in \bigcap_{n=0}^\infty f\left[B_n\right]$. 
So we've shown that $y \in f\left[ \bigcap_{n=0}^\infty B_n\right] \implies y \in \bigcap_{n=0}^\infty f\left[B_n\right]$.  
Now, assuming that $f$ is one-to-one, suppose that we have $y \in f\left[B_n\right]$ for each $n$. 
So for all $n$, there is an $x \in X$ such that $f(x) = y$. 
But if $f$ is an injection then, by definition, there is only one such $x$. 
It follows that for each $n$, this unique $x$ is in $B_n$, that is $x \in \bigcap_{n=0}^\infty B_n$.  
And $x \in \bigcap_{n=0}^\infty B_n \implies y \in f\left[ \bigcap_{n=0}^\infty B_n\right] $.
So we've shown that $y \in \bigcap_{n=0}^\infty f\left[B_n\right] \implies y \in f\left[ \bigcap_{n=0}^\infty B_n\right] $. 
So the implication goes in both directions, which is what we needed to show. 
End proof.
Thanks in advance for your comments. I really appreciate it. 
 A: The proof looks correct, however, you should consider the case where either side is the empty set.
A more concise proof (of a slight generalization: the index set need not be countable). Let $\Lambda$ be an index set and let $B_\alpha$ be a sequence of sets in $X$ where $\alpha \in \Lambda$. Let $f : X \to Y$ be an injective function.
Suppose that neither side is the empty set.
\begin{align*}
y \in f \bigg(\bigcap_{\alpha \in \Lambda} B_\alpha \bigg) &\implies \exists x \in \bigcap_{\alpha \in \Lambda} B_\alpha : y = f(x) \\
&\implies \exists x \in B_\alpha , \forall \alpha \in \Lambda : y = f(x) \\
&\implies y \in f(B_\alpha), \forall \alpha \in \Lambda \\
&\implies y \in \bigcap_{\alpha \in \Lambda} f(B_\alpha)
\end{align*}
and
\begin{align*}
y \in \bigcap_{\alpha \in \Lambda} f(B_\alpha) & \implies \forall \alpha \in \Lambda, y \in f(B_\alpha)\\
&\implies \forall \alpha \in \Lambda, \exists x_\alpha \in B_\alpha : y = f(x_\alpha) \\
&\implies x \in B_\alpha, \forall \alpha \in \Lambda \text{ where } x_\alpha = x,  \forall \alpha \in \Lambda \text{ by injectivity} \\
&\implies x \in \bigcap_{\alpha \in \Lambda} B_\alpha : y = f(x) \\
&\implies y \in f\bigg( \bigcap_{\alpha \in \Lambda} B_\alpha \bigg)
\end{align*}
Now, if either side is empty, and we assume by way of contradiction that the other side is nonempty, we arrive at the fact (using our reasoning above) that the side we started with was empty, a contradiction.
