Is the inverse image function injective? It seems that the inverse image function(see my previous question) is injective. Where a proof of that can be found?
 A: Still waiting for an answer, but here is my proof:

*

*It is clear that the set
$part(f) := \{f^{-1}(\{f(x)\}) : x \in dom(f)\}$ is a partition of $dom(f)$.


*It is also clear that there exists a bijection between $im(f)$ and $part(f)$;


*Then exists the induced bijection between $P(im(f))$ and $P(part(f))$;


*From the other side, because $f^{-1}(X \cup Y) = f^{-1}(X) \cup f^{-1}(Y)$ where $X,Y \subset im(f)$
$f^{-1}(B) = \{x \in dom(f) : f(x) \in B\} = U[b \in B, f^{-1}(\{f(b)\}) = U[b \in B, \pi(b)] $.
where $ \pi(b) := f^{-1}(\{f(b)\})$ is an element of $part(f)$.


*If the inverse image function is not injective, then for some
$B_1,B_2 \subset im(f), B_1 \neq B_2$ holds:
$U[b \in B_1, \pi(b)] = U[b \in B_2, \pi(b)]$.


*But this is impossible, because  all $\pi(b)$ are disjoint and in the left and right parts
of the above equation the collections of $\pi(b)$ are different ( because  $B1 \neq B2$   and (3)).
A: *

*In order that the inverse $f^{-1}$ to exist, $f$ must be injective (1-1).
Because, if not, $\exists x_1, x_2: f(x_1) = f(x_2) \land  x_1 \neq x_2
   \Rightarrow \exists y_1, y_2: y_1 = y_2 \land  f^{-1}(y_1) \neq
   f^{-1}(y_2)$, violating the definition of a function.

*Now, $f^{-1} = F[y \in im(f)), \{x \in dom(f): f(x) = y \}]$. We have $y_1 \neq y_2 \Rightarrow f(x_1) \neq f(x_2) \Rightarrow x_1 \neq x_2 \Rightarrow f^{-1}(y_1) \neq f^{-1}(y_2)$ (by injectivity of $f$). Which implies $f^{-1}$ is injective.

