(related to Lemma: Behavior of Functions with Set Operations)
In the following, $A,B$ denote sets, between which a function $f:A\mapsto B$ be defined.
| $y\in f[X\cup Y]$ | $\Leftrightarrow$ | <. $\exists x:(x\in X\cup Y\wedge y=f(x))$ | definition of image. |
|---|---|---|---|
| $\Leftrightarrow$ | <. $\exists x:((x\in X\vee x\in Y)\wedge y=f(x))$ | definition of set union. | |
| $\Leftrightarrow$ | <. $(\exists x:(x\in X \wedge y=f(x)))\vee (\exists x:(x\in Y \wedge y=f(x)))$ | definition of set union. | |
| $\Leftrightarrow$ | <. $\exists y:y\in f[X]\vee y\in f[Y]$ | definition of image. | |
| $\Leftrightarrow$ | <. $\exists y:y\in f[X]\cup f[Y]$ | definition of set union. | |
| Altogether, it follows $f[X\cup Y]=f[X]\cup f[Y]$ for all subsets of $X,Y\subseteq A.$ |
$y\in f[X\cap Y]$| $\Leftrightarrow$|<. $\exists x:(x\in X\cap Y\wedge y=f(x))$| definition of image. | $\Rightarrow$|<. $\exists x_1,x_2:((x_1\in X\wedge x_2\in Y)\wedge y=f(x_1)=f(x_2))$| definition of set intersection and because $f$ is generally not injective, (thus $x_1=x_2$ cannot be assumed). | $\Leftrightarrow$|<. $(\exists x_1:(x_1\in X \wedge y=f(x_1)))\wedge (\exists x_2:(x_2\in Y \wedge y=f(x_2)))$| definition of set intersection. | $\Leftrightarrow$|<. $\exists y:y\in f[X]\wedge y\in f[Y]$| definition of image. | $\Leftrightarrow$|<. $\exists y:y\in f[X]\cap f[Y]$| definition of set intersection. Altogether, it follows $f[X\cap Y]\subseteq f[X]\cap f[Y]$ for all $X,Y\subseteq A.$ Please note the difference in the second argument and in the outcome of the argumentation.
$x\in f^{-1}[X\cup Y]$| $\Leftrightarrow$|<. $\exists x:f(x)\in X\cup Y$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:f(x)\in X \vee f(x)\in Y$| definition of set union. | $\Leftrightarrow$|<. $\exists x:x\in f^{-1}[X]\vee x\in f^{-1}[Y]$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:x\in f^{-1}[X]\cup f^{-1}[Y]$| definition of set union. Altogether, it follows $f^{-1}[X\cup Y]=f^{-1}[X]\cup f^{-1}[Y]$ for all $X,Y\subseteq B.$
$x\in f^{-1}[X\cap Y]$| $\Leftrightarrow$|<. $\exists x:f(x)\in X\cap Y$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:f(x)\in X \wedge f(x)\in Y$| definition of set intersection. | $\Leftrightarrow$|<. $\exists x:x\in f^{-1}[X]\wedge x\in f^{-1}[Y]$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:x\in f^{-1}[X]\cap f^{-1}[Y]$| definition of set intersection. Altogether, it follows $f^{-1}[X\cap Y]=f^{-1}[X]\cap f^{-1}[Y]$ for all $X,Y\subseteq B.$
$y\in f[A]\setminus f[X]$| $\Leftrightarrow$|<. $\exists y:y\in f[A]\wedge y\not\in f[X]$| definition of set difference. | $\Rightarrow$|<. $(\exists x: x\in A\wedge f(x)=y)\wedge (\not\exists x:x\in X\wedge f(x)=y)$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:x\in A\setminus X\wedge f(x)=y$| definition of set difference. | $\Leftrightarrow$|<. $\exists y:y\in f[A\setminus X]$| definition of inverse image. Altogether, it follows $f[A\setminus X]\supseteq f[A]\setminus f[X]$ for all $X \subseteq A.$
$x\in f^{-1}[B\setminus X]$| $\Leftrightarrow$|<. $\exists x:f(x)\in B\setminus X$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:f(x)\in B\wedge f(x)\not \in X$| definition of set difference. | $\Leftrightarrow$|<. $\exists x:x\in A\wedge x\not\in f^{-1}[X]$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:x\in A\setminus f^{-1}[X]$| definition of set difference. Altogether, it follows $f^{-1}[B\setminus X]=A\setminus f^{-1}[X]$ for all $X\subseteq B.$
$x\in X$| $\Rightarrow$|<. $\exists x:f(x)\in f[X]$| definition of image. | $\Leftrightarrow$|<. $\exists x:x\in f^{-1}[X]$| definition of inverse image. Altogether, it follows $f^{-1}[f[X]]\supseteq X$ for all $X\subseteq A.$
$y\in f[f^{-1}[X]]$| $\Rightarrow$|<. $\exists x:x\in f^{-1}[X]\wedge f(x)=y$| definition of image. | $\Leftrightarrow$|<. $\exists x:f(x)\in X\wedge f(x)=y$| definition of inverse image. | $\Leftrightarrow$|<. $\exists x:y\in X\wedge f(x)=y$| definition of function. Altogether, it follows $f[f^{-1}[X]]\subseteq X$ for all $X\subseteq B.$
