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.

-
The writing could be tightened up just a bit, but it’s correct and reasonably clear. – Brian M. Scott Feb 2 '13 at 23:19
@WilloW In the first inclusion you took $y\in Y$ first and you supposed it was in LHS set of the equality. Despite not being incorrect, there's no need for that. You can simply take $y$ in the LHS set from the get go. – Git Gud Feb 2 '13 at 23:24
Thanks for the comments! Really appreciate it. – WilloW Feb 3 '13 at 17:19

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.

-