Using reduction to prove that a given language is not recursively enumerable Let  the language $L$  be as follow  ; 

$$L=\{\langle M_1 \rangle \langle M_2 \rangle \mid L(M_1)  \cap L(M_2)=\emptyset \}$$

$\langle M_1 \rangle$ and $\langle M_2 \rangle$ are the encoding of the Turing machine $M_1$ and $  M_2$.

Using Reduction, I have to prove that $L$ is not  recursively enumerable.

In order to prove that I have to find a non-recursively enumerable  language $S$ so that: 
$$S \leq L$$
One of the non recursively enumerable that I had in my lesson, were  those : 
$${H_{\varepsilon}^\complement}=\{\langle M \rangle \mid \text{M does not halt on empty input} \}$$
 and ;
$${H_{all}}=\{ \langle M \rangle \mid \text{M halts on each input} \}$$

$$ \text{Let then } S = {H_{all}}$$

I  have to prove in this case  that  ; 
$${H_{all}} \leq L $$

let then  ; 
$$ f : {H_{all}} \rightarrow L  \\ 
 \langle M \rangle \mapsto \langle M \rangle \langle M^\complement \rangle$$

In this case $M^\complement $ simulate M in each input , when $M$ accepts/rejects, $M^\complement $ rejects/accepts.

$\texttt{case 1}$

$\langle M \rangle \in {H_{all}} \Rightarrow  \text{M halts on each input and accepts/rejects} \Rightarrow  M^\complement\text{ hatls on each input and rejects/accepts} \Rightarrow  L(M) \cap L(M^\complement)= \emptyset  $

$\Rightarrow \langle M \rangle \langle M^\complement \rangle \in L $

$\texttt{case 2}$

$\langle M \rangle \not\in {H_{all}} \Rightarrow  \text{M does not halt  on all inputs} \Rightarrow  M^\complement\text{  halts  on some inputs} \Rightarrow  L(M) \cap L(M^\complement) \neq\emptyset  $

$\Rightarrow \langle M \rangle \langle M^\complement \rangle \not\in L $

somehow  i think , the contruction of the function of is not  right, does anyone maybe have an other idea or an other S to choose ?
Assume that $L$ is recursively enumerable. We can reduce the Halting problem to $L$ as following. Given $\langle M, w \rangle$, create a TM $M'$ which halts only on the input $w$, and infinitely loops if the input is different from $w$. Clearly $L(M') = \{w\}$ and $L(M) \cap L(M') = \emptyset \iff \langle M,M' \rangle \in L \iff \langle M, w \rangle \notin HALT$. This shows that $\overline{HALT}$ is recursively enumerable. Since $HALT$ is also r.e. it follows that $HALT$ is decidable which is impossible. Thus $L$ is not recursively enumerable.

$HALT = \{\langle M, w \rangle \mid M \text{ is a TM and } M \text{ halts on input } w \}$.