Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma,

my_thm : ¬ (∀ {M : Set} (P Q : M → M → Set) →
(∀ x → ∃ M , λ y → P x y ∨ Q x y) →
(∀ x → ∃ M , P x) ∨ (∀ x → ∃ M , Q x))
my_thm = ?

while Agda gives following mistake:

Set₁ != Set
when checking that the expression
{M : Set} (P Q : M → M → Set) →
(∀ x → ∃ M , λ y → P x y ∨ Q x y) →
(∀ x → ∃ M , P x) ∨ (∀ x → ∃ M , Q x)
has type Set

honestly, in my untrained eyes, this type looks entirely routine to me, and it shouldn't introduce universe inconsistency.

all extra quantifier and connectivities are defined as following,

data _∨_ : Set → Set → Set where
inl : {A B : Set} → A → A ∨ B
inr : {A B : Set} → B → A ∨ B
infixl 20 _∨_

¬_ : Set → Set
¬ P = P → False
infix 40 ¬_

data ∃_,_ : (A : Set) → (A → Set) → Set where
ex : {A : Set}{P : A → Set} → (x : A) → (ev : P x) → ∃ A , P
infix 10 ∃_,_

which part introduces Set1 in this code?

ok, it turns out it's caused by negation: ¬_ : Set → Set. However, I still not understand. why this innocent looking function does not do what I want? what's the correct way of implementing it?