Gentzen Natural Deduction Quantifier Problem!

Question

I am having a problem with

$$\exists x \ T(x),\quad \forall x \ (T(x) \to P(x)) \quad \text{leads to} \quad \exists y\ (T(y) \land P(y))... \tag 1$$

It is using $$\forall \text{intro,elim} \ \text{and}\ \exists\text{intro,elim}.$$ Also, another question is

$$\forall x \ (P(x)\land Q(x)) \quad \text{leads to}\quad \forall x \ P(x) \land \forall y\ Q(y). \tag 2$$

I can go until some level, but I am not sure if I am correct and did the right steps. For first $Q$, I got until $T(t) \to P(t)$, but I don't know how I can use ∃elim to make the first premise to $T(t)$. For the second $Q$, I got $P(t)$ and $Q(t)$ but I am stuck.. please help :)

Answer 1

For the first one, we have to prove :

$∃x T(x), ∀x (T(x) → P(x)) \vdash ∃y (T(y)∧P(y))$

1) $∃x T(x)$ --- premise

2) $∀x (T(x) → P(x))$ --- premise

3) $T(a)$ --- assumed [a] from 1) for $∃$-elim

4) $T(a) → P(a)$ --- from 2) by $\forall$-elim

5) $P(a)$ --- from 3) and 4)

6) $T(a) \land P(a)$ --- from 3) and 5) bu $\land$-intro

7) $∃y (T(y)∧P(y))$ --- from 6) by $∃$-intro.

Now we may close the $\exists$-elim discharging assumption [a].

---

The second one is very,very simple. We have only to use $\forall$-elim and $\land$-elim, followed by $\forall$-intro and $\land$-intro.