Show that $\bigcup_i f(A_i) = f(\bigcup_i A_i)$

Let $y\in\cup_i f(A_i)$. Then $y\in f(A_j)$ for some $j$. Then $y=f(t)$ for some $t\in A_j$. But $t\in \cup_i A_i$ so that $y\in f\left(\cup_i A_i\right)$.

Let $y\in f\left(\cup_i A_i\right)$. Then $y=f(s)$ for some $s\in\cup_i A_i$. But $s\in A_l$ for some $l$ so that $y\in f(A_l)$. Hence $y\in\cup_i f(A_i)$.

This is easily proved by ‘element-chasing’: assume that $x$ is an element of the lefthand side and chase through the definition of union to show that $x$ is an element of the righthand side, then do the opposite. I’ll do one direction and let you try the other.

Suppose that $x\in\bigcup_{i\in I}f[A_i]$. By the definition of union this means that there is at least one $i_0\in I$ such that $x\in f[A_i]$. Since $x\in f[A_{i_0}]$, there is some $y\in A_{i_0}$ such that $x=f(y)$. That’s about as much as we can get directly from the hypothesis, so let’s see where we’re trying to go: we want to show that $x\in f\left[\bigcup_{i\in I}A_i\right]$.

Okay, we know that $x=f(y)$; is $y\in\bigcup_{i\in I}A_i$? If it is, then certainly $x=f(y)\in f\left[\bigcup_{i\in I}A_i\right]$, and we’re home free. And the answer is yes: $y\in A_{i_0}\subseteq\bigcup_{i\in I}A_i$, so $y\in\bigcup_{i\in I}A_i$, and therefore $x\in f\left[\bigcup_{i\in I}A_i\right]$. Since $x$ was an arbitrary element of $\bigcup_{i\in I}f[A_i]$, we’ve shown that $$\bigcup_{i\in I}f[A_i]\subseteq f\left[\bigcup_{i\in I}A_i\right]\;.$$

Now you try the same approach to prove that $$f\left[\bigcup_{i\in I}A_i\right]\subseteq\bigcup_{i\in I}f[A_i]\;;$$ once you’ve done that, you can conclude that $$\bigcup_{i\in I}f[A_i]=f\left[\bigcup_{i\in I}A_i\right]\;.$$

Expanding the definitions and using predicate logic leads to a very simple and direct proof: with $\;i\;$ implicitly ranging over some index set, we calculate for all $\;y\;$,

\begin{align} & y \in \langle \cup i :: f\left[ A_i \right] \rangle \rangle \\ \equiv & \qquad \text{"definition of $\;\cup\;$ quantification"} \\ & \langle \exists i :: y \in f\left[ A_i \right] \rangle \rangle \\ \equiv & \qquad \text{"definition of $\;\cdot\left[\cdot\right]\;$"} \\ & \langle \exists i :: \langle \exists x : f(x) = y : x \in A_i \rangle \rangle \\ (*) \quad \equiv & \qquad \text{"logic: exchange $\;\exists\;$ quantifications -- really the only thing to do"} \\ & \langle \exists x : f(x) = y : \langle \exists i :: x \in A_i \rangle \rangle \\ \equiv & \qquad \text{"definition of $\;\cup\;$ quantification"} \\ & \langle \exists x : f(x) = y : x \in \langle \cup i :: A_i \rangle \rangle \\ \equiv & \qquad \text{"definition of $\;\cdot\left[\cdot\right]\;$"} \\ & y \in f\left[ \langle \cup i :: A_i \rangle \right] \\ \end{align} which (by set extensionality) proves $\;\langle \cup i :: f\left[ A_i \right] \rangle \rangle = f\left[ \langle \cup i :: A_i \rangle \right]\;$ as required.

Note how the key step is $(*)$.

Note also how we did not have to have separate $\;\Rightarrow\;$ and $\;\Leftarrow\;$ proofs: we proved both directions at the same time.

Finally, note that a similar proof would not work for $\;\cap\;$ instead of $\;\cup\;$: most we could prove there would be $\;\langle \cap i :: f\left[ A_i \right] \rangle \rangle \supseteq f\left[ \langle \cap i :: A_i \rangle \right]\;$, using $\;\exists\forall \Rightarrow \forall\exists\;$.