problem from Kenneth Rosen's Discrete Mathematics and its Applications, Section 1.5 
Express this system specifications using predicates, quantifiers, and
  logical connectives, if necessary.
There are exactly two systems that monitor every remote server.

My solution is : 

∃x∃y∀z(x != y ∧ (∀s M(z,s) → (z = x ∨ z = y))), where M(a, b) means that system a monitors remote server b

So can anyone please check my solution if it's correct and if not what is the correct solution?
 A: The problem:

There are exactly two systems that monitor every remote server.
M(a, b) means that system a monitors remote server b.

Can be rewritten into:
$\color{red}{\text{There is a system x and there is a system z such that the two systems are different}}$ and $\color{blue}{\text{system x monitors all remote servers and system z monitors all remote servers}}$ and $\color{green}{\text{no other system w monitors all remote servers}}$.
$$\color{red}{\exists x,z(x\neq z} \land \color{blue}{\forall y M(x,y) \land \forall y M(z,y)}\land \color{green}{\lnot\exists w(w \neq x \land w \neq z \land \forall y M(w,y))}\color{red}{)}$$
Since $\lnot\exists w(P(w)) \iff \forall w(\lnot P(w))$, we can rewrite this as:
$$\color{red}{\exists x,z(x\neq z} \land \color{blue}{\forall y M(x,y) \land \forall y M(z,y)}\land \color{green}{\forall w(\underbrace{w = x \lor w = z}_{\psi} \lor \lnot\underbrace{\forall y M(w,y)}_{\phi})}\color{red}{)}$$
Finally, using the property:
$\psi \lor \lnot\phi \iff \phi\rightarrow \psi$
we end up with the accepted solution:
$$\color{red}{\exists x,z(x\neq z} \land \color{blue}{\forall y M(x,y) \land \forall y M(z,y)}\land \color{green}{\forall w(\forall y M(w,y) \rightarrow (w = x \lor w = z))}\color{red}{)}$$
A: The valid solution is:

∃x∃y((x ≠ y) ∧ ∀zM(x,z) ∧ ∀zM(y,z) ∧ ∀w(∀zM(w,z) → (w = x) ∨ (w = y)))

And so my solution is too close to the right I just missed to put ∀zM(x,z) ∧ ∀zM(y,z)
