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 \}$.

StackExchange Computer Science Q#84448, answer score: 4