Let $N$ be a set for which $$\forall a\left(a\in N\iff a=\{\}\lor\exists b\left(b\in N\land a=\left\{b\right\}\right)\right)$$ Prove that $$\forall P\left(\left\{\right\}\in P\land \forall a\left(a\in N\implies\left(a\in P\implies\{a\}\in P\right)\right)\implies\forall a\left(a\in N\implies a\in P\right)\right)$$
I'm having troubles with this problem. The first thing I tried to do is to expand the definition of set $N$. It seems that there is exactly one set $N$ for which the first statement is true. The second statement should be true for all $P$ and $a$ (we need to prove it).
My first attempt was to replace $a\in N$ in the second statement with $a=\{\}\lor\exists \left(b\in N\land a=\left\{b\right\}\right)$. The part $\{\}\in P\implies\{\}\in N$ is true, according to the definition of $N$. Now, I'm not sure how to deal with $\forall a\left(a\in N\implies\left(a\in P\implies\{a\}\in P\right)\right)$. Becuase there is an implication after this statement, the first idea which came to my mind is to try contradiction approach. Suppose that $\forall a\left(a\in N\implies\left(a\in P\implies\{a\}\in P\right)\right)$ is not true. So, I need to prove that then exists some $a$ from $N$ which is not in $P$. But, how to do that? I ran out of ideas.
One thing I noticed is that both in the definition of $N$ and the second statement, which we need to prove, appear $\{b\}$ (and in the second $\{a\}$). I suppose the trick is to somehow apply this part of the definition of set $N$ (or a set $N$, if there may be multiple sets $N$) such that these two parts cancel out using some logical implications.
I'm looking for an axiom-level proof. I mean, applying logical and ZFC axioms to this statement until we obtain an equivalence where on the left side is the statement we need to prove and on the right side is something which is true by definition.
Simply, what would be the easiest way to prove this? Thank you in advance if you decide to help :)
The key idea you're missing is to use the axiom of regularity in order to make a stronger assumption about $a$. Specifically, suppose there does exist $a\in N$ such that $a\not\in P$. Let $S=\{a:a\in N\wedge a\not\in P\}$ (this set exists by Separation from $N$). By assumption, $S$ is nonempty, so by the axiom of regularity there exists some $a\in S$ such that for all $b\in S$, $b\not\in a$. Now try applying your line of thinking to this particular special $a$.
(Incidentally, I would very strongly advise against trying to think about things like this in purely formal "axiom"-level terms. First come up with an informal argument based on your intuitive understanding of how sets and logic work and what the axioms mean, and then go back and try to make it fully formal once you have the informal argument.)