Natural Deduction Proof with double quantifier (predicate logic) [closed]

Question

Premise: (∃y)(∀x)(Px v Py)

Conclusion: ~(∀y)(~Py)

I'm starting out assuming the negation, i.e., (∀y)(~Py).

But then I'm unsure how to find a contradiction within that subderivation. Here's what I've done so far, i know it's wrong because I can't do ∃E

1. (∃y)(∀x)(Px v Py)       Premise
|  2. (∀y)(~Py)            Assume
|  3. ~Pa                  UI 2
|  4. (∃y)(∀x)(Px v Py)    Reiterate
|  b|  5. (∀x)(Px v Pb)    Assume
|   |  6. Pa v Pb          UE 5
|   |  7. Pb               vE 3,6

Answer 1

1. (∃y)(∀x)(Px v Py)       Premise
|  2. (∀y)(~Py)            Assume
|  3. ~Pa                  UI 2
|  4. (∃y)(∀x)(Px v Py)    Reiterate
|  b|  5. (∀x)(Px v Pb)    Assume
|   |  6. Pa v Pb          UE 5
|   |  7. Pb               vE 3,6

That is a disjunctive syllogism vS rather than disjunction elimination vE. Well, if you are allowed to use that rule, you may.

However, as it stands your main issue lies in not being able to derive a contradiction. It would be best to have somehow derived ~Pb, so...

Do not immediately use UE on an arbitrary variable (a). Instead, be patient and wait until you have the witness for an existential (b).

|_ 1. (∃y)(∀x)(Px v Py)        Premise
|   |_ 2. (∀y)(~Py)            Assume
|   |  3. (∃y)(∀x)(Px v Py)    Reiterate 1
|   |[b]|_ 4. (∀x)(Px v Pb)    Assume
|   |   |  5. (∀y)(~Py)        Reiterate 2
|   |   |  6. ~Pb              UE 5
|   |   |  7. Pb v Pb          UE 4
|   |   |  8. Pb               vS 6,7 
:   :   :