Q:

Proving two claims about sets and functions

Let X,Y be sets, and let $f:X\rightarrow Y$ be a function. Prove:

$f(f^{-1}(B))\subset B$ for every $B\subset Y$. Intuitively I understand why's that, but how do I prove it with formality?
For every $B\subset Y$, $f(f^{-1}(B))=B$ if and only if $f$ is surjective. Same as #1. Thanks in advance! 

A:

With $f : X \rightarrow Y$, $x \in X$, $y \in Y$, $A \subset X$, and $B \subset Y$ assumed throughout, and using the definitions $$
\begin{align}
(0) & y \in f(A) \;\equiv\; \langle \exists x : x \in A : f(x) = y \rangle \\
(1) & x \in f^{-1}(B) \;\equiv\; f(x) \in B \\
\end{align}
$$ the simplest thing I see is to calculate which elements are in $f(f^{-1}(B))$, since that is the most complex expression in the question: for every $y$ and $B$, we have $$
\begin{align}
& y \in f(f^{-1}(B)) \\
\equiv & \;\;\;\;\;\text{"expand using definition (0)"} \\
& \langle \exists x : x \in f^{-1}(B) : f(x) = y \rangle \\
\equiv & \;\;\;\;\;\text{"expand using definition (1)"} \\
& \langle \exists x : f(x) \in B : f(x) = y \rangle \\
\equiv & \;\;\;\;\;\text{"logic: substitute $y$ for $f(x)$"} \\
& \langle \exists x : y \in B : f(x) = y \rangle \\
\equiv & \;\;\;\;\;\text{"logic: simplify, allowed because expression $y \in B$ does not contain $x$"} \\
& y \in B \;\land\; \langle \exists x :: f(x) = y \rangle \\
\equiv & \;\;\;\;\;\text{"make $x \in X$ explicit -- to prepare for use of definition (0)"} \\
& y \in B \;\land\; \langle \exists x : x \in X: f(x) = y \rangle \\
\equiv & \;\;\;\;\;\text{"introduce definition (0)"} \\
& y \in B \;\land\; y \in f(X) \\
\equiv & \;\;\;\;\;\text{"definition of $\cap$"} \\
& y \in B \cap f(X) \\
\end{align}
$$  (For clarity I've left in a few trivial steps that one would normally skip.)  So by set extensionality we've calculated that $$
(*) \;\;\;\;\; f(f^{-1}(B)) \;=\; B \cap f(X)
$$  From this key insight, both parts of the question follow directly.  For the first part use $B \cap f(X) \subset B$ from set theory.  For the second part, surjectivity automatically falls out of the following calculation: $$
\begin{align}
& \langle \forall B :: f(f^{-1}(B)) = B \rangle \\
\equiv & \;\;\;\;\;\text{"using (*)"} \\
& \langle \forall B :: B \cap f(X) = B \rangle \\
\equiv & \;\;\;\;\;\text{"make range explicit; set theory"} \\
& \langle \forall B : B \subset Y : B \subset f(X) \rangle \\
\equiv & \;\;\;\;\;\text{"set theory"} \\
& Y \subset f(X) \\
\equiv & \;\;\;\;\;\text{"set extensionality -- so that we can use our definitions again"} \\
& \langle \forall y : y \in Y : y \in f(X) \rangle \\
\equiv & \;\;\;\;\;\text{"introduce definition (0)"} \\
& \langle \forall y : y \in Y : \langle \exists x : x \in X: f(x) = y \rangle \rangle \\
\equiv & \;\;\;\;\;\text{"definition of surjectivity"} \\
& f \textrm { is surjective} \\
\end{align}
$$

