Let $A \subseteq X$ and $f: X \mapsto X$. Prove $f^{-1}(A) = A \iff f(A) \subseteq A \land f^{-1}(A) \subseteq A$ Let $A \subseteq X$ and $f: X \mapsto X$.
Prove $f^{-1}(A) = A \iff f(A) \subseteq A \land f^{-1}(A) \subseteq A$
I have already proved $f(f^{-1}(A)) \subseteq A$:
$e \in f(f^{-1}(A)) = \{f(x) \mid x \in \{y \in X \mid f(y) \in A\}\} \Rightarrow e \in A \Rightarrow f(f^{-1}(A)) \subseteq A$
Is this proof valid ?
I have shown the implication ($\Rightarrow$):
$f^{-1}(A) = \{y \in X \mid f(y) \in A\} = A \Rightarrow f(f^{-1}(A)) = f(A) \Rightarrow f(A) \subseteq A \land f^{-1}(A) \subseteq A$
where the last implication follows from the assumption and the statement I've already proved.
Is this proof valid ?
However could someone help proving the implication ($\Leftarrow$) ?
 A: Hint for $(\Rightarrow)$: For any set $A$ we always have $f(f^{-1}(A))\subseteq A$, so start with $A=f^{-1}(A)$ and take $f$.
Hint for $(\Leftarrow)$: For any set $A$ we always have $A\subseteq f^{-1}(f(A))$, so start with $f(A)\subseteq A$ and take $f^{-1}$.
A: $
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\\ #1 \quad & \quad \text{"#2"} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
$Here is an alternative proof which might help.
First let's simplify the original statement:
$$\calc
f^{-1}[A] = A \;\iff\; f[A] \subseteq A \land f^{-1}[A] \subseteq A
\calcop{\iff}{split $\;=\;$ into two inclusions -- to make both sides more alike}
f^{-1}[A] \subseteq A \land A \subseteq f^{-1}[A] \;\iff\; f[A] \subseteq A \land f^{-1}[A] \subseteq A
\calcop{\iff}{logic: simplify by extracting common conjunct $\;f^{-1}[A] \subseteq A\;$}
\tag{*} f^{-1}[A] \subseteq A \;\implies\; (A \subseteq f^{-1}[A] \;\iff\; f[A] \subseteq A)
\endcalc$$
Now let's see when the equivalence holds, by expanding and simplifying both $\;A \subseteq f^{-1}[A]\;$ and $\;f[A] \subseteq A\;$.  For the left hand side we have
$$\calc
A \subseteq f^{-1}[A]
\calcop{\iff}{definition of $\;\subseteq\;$}
\langle \forall x : x \in A : x \in f^{-1}[A] \rangle
\calcop{\iff}{basic property of $\;\cdot^{-1}[\cdot]\;$}
\tag{**} \langle \forall x : x \in A : f(x) \in A \rangle
\endcalc$$
And for the right hand side we have
$$\calc
f[A] \subseteq A
\calcop{\iff}{definition of $\;\subseteq\;$}
\langle \forall y : y \in f[A] : y \in A \rangle
\calcop{\iff}{definition of $\;\cdot[\cdot]\;$}
\langle \forall y : \langle \exists x : f(x) = y : x \in A \rangle : y \in A \rangle
\calcop{\iff}{logic: merge quantifications -- to simplify}
\langle \forall y,x : f(x) = y \land x \in A : y \in A \rangle
\calcop{\iff}{logic: one-point rule for $\;y\;$}
\tag{**} \langle \forall x : x \in A : f(x) \in A \rangle
\endcalc$$
The lines $\text{(**)}$ are the same, therefore we proved $\;A \subseteq f^{-1}[A] \;\iff\; f[A] \subseteq A\;$, thereby proving that $\text{(*)}$ is true, completing the proof.
