Lemmata about equivalence relations We've defined relations and equivalence relations a few days ago at university. 
I tried to look at them a bit more abstract and came up with two lemmata. I am going to write them down with my proofs and it would be nice to let me know what you think of them. 
Are they useful/useless, are the proofs right/wrong etc...
Lemma 1: Be $Z$ a set and be $\sim$ an equivalence relation on a set $M$.
Be $f$ a function with $f: M \rightarrow Z$ and be $g$ a function with $g: M \rightarrow M$
$f$ and $g$ also fulfill the following:
\begin{align}
&\forall x,y \in M: f(x) = f(y) \implies g(x) = g(y)\\
&\forall x \in M: x \sim g(x)
\end{align}
It follows: $$\forall x,y \in M: f(x) = f(y) \implies x \sim y$$
Proof. Be $x,y \in M$ and be $f(x) = f(y)$. It follows $g(x) = g(y)$ and because $\sim$ is an equivalence relation it holds: $$x \sim g(x) \sim g(y) \sim y \quad \square$$
Lemma 2: Be $Z$ a set and be $\sim$ an equivalence relation on a set $M$.
Be $f$ a (surjective) function with $f: M \rightarrow Z$. Be also $X \subseteq M$ and be $f \mid_X$ bijective. $f$ also fulfills the following: $$\forall x,y \in M: x \sim y \Longleftrightarrow f(x) = f(y)$$
It follows: $$M/_\sim = \{[a]_\sim \mid a \in X\}$$ and $$\forall x,y \in X: x \sim y \implies x=y$$
Proof. $M/_\sim \supseteq \{[a]_\sim \mid a \in X\}$ is trivial. Be $x \in M/_\sim$ and be $x' \in x$. It holds $f(x') \in Z$. $f \mid_X$ is surjective, hence there is a $y \in X$ with: $$f(y) = f(x')$$
Hence $y \sim x'$, which yields $[y]_\sim = [x']_\sim$. Finally: $$M/_\sim \subseteq \{[a]_\sim \mid a \in X\}$$
Be now $x,y \in X$ and be $x \sim y$.
It follows $f(x) = f(y)$ and since $f \mid_X$ is injective, we get: $$x=y \quad \square$$
 A: Intro:
Every function $h:X\rightarrow Z$ induces an equivalence relation
$\sim_{h}$ on set $X$. This by $u\sim_{h}v\iff h\left(u\right)=h\left(v\right)$.
Let $\left[x\right]_{h}$ denote the equivalence class represented
by $x\in X$. Then $\left[x\right]_{h}=h^{-1}\left(\left\{ h\left(x\right)\right\} \right)$.
Conversely if $\sim$ is some equivalence relation on $X$ then $\sim=\sim_{\nu}$
where $\nu:X\rightarrow X/\sim$ is the natural map that send $x$
to the equivalence class that contains $x$.
If $P$ denotes a partition of $X$ then the relation $\sim$ on $X$
defined by $$u\sim v\iff u,v\text{ belong to the same element of }P$$
is an equivalence relation and its equivalence classes are the elements
of $P$.
In that sense there is a strong relation between functions, equivalence
relations and partitions.
It is a very good custom to keep this connection in mind. 

Your lemma1 in this light.
In your first lemma we have $f\left(x\right)=f\left(y\right)\implies g\left(x\right)=g\left(y\right)$.
This is sometimes expressed as: "function $g$ respects function $f$".
It means exactly that $\left[x\right]_{f}\subseteq\left[x\right]_{g}$
for each $x\in X$. In fact the partition induced by function $f$
is finer than the partition induced by function $g$. 
This will be the case if and only if: $$g=h\circ f\text { for some function }h$$ It is easy
to prove that this condition is sufficient. Conversely we can prescribe
such function $h$ by stating that $h\left(z\right):=f\left(x\right)$
when $f\left(x\right)=z$. If no such $x$ can be found then for $h\left(z\right)$
we can take any element in $M$. Exactly the fact that $g$ respects
$f$ guarantees that $h$ is well defined. If $f$ is surjective then
$h$ is unique :for each $z\in Z$ we can find an $x$ with $z=f(x)$ and $h(z)=g(x)$.
Prescribing $\nu:M\rightarrow M/\sim$ by $x\mapsto\left[x\right]_{\sim}$
the statement $\forall x\in M\left[x\sim g\left(x\right)\right]$
is the same as $\nu=\nu\circ g$. Combined with $g=h\circ f$ we find:
$\nu=\nu\circ\left(h\circ f\right)=\left(\nu\circ h\right)\circ f$.
So $\nu$ respects $f$ wich means exactly that $f\left(x\right)=f\left(y\right)\implies x\sim y$.

Your lemma2 in this light.
Let me first say that your lemma is okay again. Defined like this we have $\sim=\sim_{f}$. The injectivity of $f\upharpoonleft X$
ensures that $\left[x\right]_{f}\cap X=\left\{ x\right\} $ for each
$x\in X$ (so that $x\sim y\implies x=y$ for $x,y\in X$ ). The surjectivity of $f\upharpoonleft X$ ensures that collection
$\left\{ \left[x\right]_{f}:x\in X\right\} $ is a partition of $M$
(so that $\left\{ \left[x\right]_{f}:x\in X\right\} =\left\{ \left[x\right]_{f}:x\in M\right\} $
). 
Sidenote:
For every $z\in Z$ there is a unique $x\in X\subseteq M$ with $f\left(x\right)=z$.
This enables us to define a function $s:Z\rightarrow M$ that sends
each $z\in Z$ to this unique $x$. Then $f\circ s=1_{Z}$. Let $r:=s\circ f$.
Then $r$ respects $f$. But also we have $f=1_{Z}\circ f=f\circ s\circ f=f\circ r$
wich means that conversely $f$ respects $r$. This means exactly
that $\sim_{r}=\sim_{f}$. Characteristic for function $r:M\rightarrow M$
is the property $r\circ r=r$. For every partition $P$ on set $X$
you can easily construct such a function. In each $p\in P$ select
some representant $x_{p}\in p$ and prescribe the function by stating
that elements of $p\subset X$ are sent to $x_{p}$.
