Thanks, your answer was useful (specially to Question 2) and clarify many things to me, but nevertheless I still am in lack of what I wanted to know in Question 1. 

Question1] ed) means that $\pi_0$ is an epimorphism, less evidently, uv) means that it is a monomorphism. Precisely I would like to have a hint of how to prove this. Out of an internal formula you derive an external statement. I had the statements exed) and exuv) and wanted to know how do you prove that they follow from  ed) and un). I can prove by standard category theory that exed) and exuv) are equivalent to $\pi_0$ being an isomorphism, but I am still in darkness about how using ed) and uv) as hypothesis on $\lambda: X \times Y \to \Omega$, I can  produce an arrow $\lambda: X \to Y$ to work with. Of course, I have a relation $R \subset X \times Y$, and all  I need is to prove that $\pi_0$ is an isomorphism. But, how I can prove (or explain) this ?, more convincingly that writing "it just says so".

Question2] A reference to or proof that the bijection 
$\mathcal{E}(X \times Y, f_* \Omega) \cong \mathcal{F}(f^* X \times f^* Y, \Omega)$ is a locale isomorphism ?. 

Concerning my original question2, it is still necessary to argue how using that being the bijection a locale isomorphism it follows that arrows which satisfy ed) and uv) correspond.