Proving $\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax))) \vdash \forall x (Dx \to Ax)$

Question

I'm trying to prove the following: $$\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax))) \vdash \forall x (Dx \to Ax)$$

The following is my first attempt. However, I'm not sure if I can just drop the existential quantifier when it is nested.

$$\begin{array}{lll} 1 & \begin{array}{l}\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax)) \end{array} \\ 2 & \begin{array}{ll}\forall x ((Dx \to Dx) \land (Dx \to Ax)) \end{array} \\ 3 & \begin{array}{lll}\forall x (Dx \to Ax)\end{array} \\ \end{array}$$

The reasoning seems valid to me. Let's say that each time an organism x is damaged, Dx, it shows avoidance behavior, Ax. We introduce the concept of 'pain' as a factor responsible for triggering the avoidance behavior, Yx. So, each time an x is damaged, there's such a thing as the feeling of pain that triggers the avoidance behavior. Since the domain contains only D and A, that feeling of pain can be identified as either D or A (we don't assume any semantics related to Y) and simply eliminate the existential quantifier. Evidently, Y just plays a role of a mediator.

How to improve the proof?

Answer 1

I don't see how you get from step $1$ to step $2$. This need more developpement. eg you can rewrite $Dx \longrightarrow Yx \equiv \neg Dx \vee Yx$ and $Yx \longrightarrow Ax \equiv \neg Yx \vee Ax$ and use De Morgan's laws from here.

handling the existential quantifier : I suggest to handle $Y$ semantically. Say we have a model $\mathcal{M}$ with universe $M$ that satisfies$$\mathcal{M} \models \forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax)))$$

We need to show that for any $m \in M$, $(\mathcal{M}, x^{\mathcal{M}} = m) \models Dx \longrightarrow Ax$
(ie $\mathcal{M}\models Dm \longrightarrow Am$, we'll write directly $(\mathcal{M}, x^{\mathcal{M}} = m) \models Dm \longrightarrow Am$ to stress out the substitutions).

Let $m \in M$. Since $(\mathcal{M}, x^{\mathcal{M}} = m) \models \exists Y \big( (Dm \to Ym) \wedge (Ym \to Am) \big)$, there exist a set $S \subseteq M$ such that : $$(\mathcal{M}, x^{\mathcal{M}} = m, Y^{\mathcal{M}} = S) \models (Dm \to Sm) \wedge (Sm \to Am)$$ whence $(\mathcal{M}, x^{\mathcal{M}} = m, Y^{\mathcal{M}} = S) \models (Dm \to Am)$ and finally : $$(\mathcal{M}, x^{\mathcal{M}} = m) \models Dm \to Am$$ QED.

Hence, $\mathcal{M} \models \forall x \ (Dx \longrightarrow Ax)$