Fitch proof exercise: showing $(\lnot \forall x \; P(x)) \leftrightarrow (\exists x \lnot P(x))$ I have got a Problem with the following fitch proof excercise:

$\quad\;\; |$
$\triangleright \quad | \quad ?. \quad (\lnot \forall x  \; P(x)) \leftrightarrow (\exists x \lnot P(x))$

This is how far I got: (Notice: I started from the bottom to the top!)

My problem is, that I can't find a way how to contradict $P(c)$. My first idea was, to proof $\forall x \; P(x)$ in the subproof in order to get a contradiction.
As you can see, this is only the first part of the proof. I know that I will have to use a Biconditional introduction in the end. I only need help for the first subproof.
Would be great if anyone could give me some hints.
 A: It looks to me like you are trying to show that $\lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $\forall x ( \lnot P(x))$. But that's too strong -- you only want to show that $\exists x (\lnot P(x))$. (Convince yourself that $\forall x ( \lnot P(x))$ is not necessarily implied by $\lnot (\forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)
So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $\exists x (\lnot P(x))$; but you only know that $\lnot \forall x. P(x)$, and there's no way to get a $c$ directly from that statement.
In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $\exists x (\lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving
$$
\lnot \lnot (\exists x ( \lnot P(x))),
$$
by assuming $\lnot \exists x ( \lnot P(x)))$ and getting a contradiction.
The proof structure will look like this:

1. $\lnot ( \forall x ( P(x)))$

  
*$\lnot \exists x ( \lnot P(x))$
  
*...[fill in here]...
  
*$\bot$
5. $\lnot \lnot \exists x (\lnot P(x))$
6. $\exists x (\lnot P(x))$ (double negation elimination from 5)

But you have to fill in the details for step 3. ... above.
To do this, show as another lemma there that $\forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.
$^1$  To prove $\forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $\lnot P(a)$ and derive a contradiction, thus showing $\lnot \lnot P(a)$, then double negation to $P(a)$.
A: Hint
You have to start assuming $\lnot Pc$ and $\lnot \exists x \lnot Px$ and find a first contradiction.
Then use Double Negation to derive $Pc$ and from it $\forall x Px$ and a new contradiction.
Then, conclude by Double Negation again.
A: Your proof idea is not going to work. Think about it: All you are given is that not everything has property $P$.  However, does that mean that some specific object $c$ does not have property $P$?  No. So, you won't be able to prove $\neg P(c)$
This is often the case when the conclusion is some existential: you have to prove that some object has (or lacks) some property, but you won;t be able to point to any specific object and say that that is one of those.
Instead, a potential fruitful approach to prove any existential is to try a proof by contradiction. Below is a completed Fitch Proof using exactly that strategy:

