This question is about ZFC set theory. Here I'll define a few things (sets) and then I have a question related to these sets I couldn't prove. Here are the definitions:
Let say that $0$ is symbol for $\{\}$ (empty set), then $1$ is symbol for $\{0\}$, then $2$ is symbol for $\{1\}$, etc. Now you can write every non-negative integer as a set.
Here is the first definition. Let $\mathbb{N}_0$ be the set for which
$$\forall a\left(a\in\mathbb{N}_0\Leftrightarrow a=0\lor\exists b\in\mathbb{N}_0\left(a=\{b\}\right)\right)$$
It may not be obvious, but it can be written as $\mathbb{N}_0=\{0,1,2,\dots\}$. However, the above definition is more formal. Now, lets define relation between non-negative integers:
$$\forall a,b\in\mathbb{N}_0\left(a>b\Leftrightarrow a=\{b\}\lor\exists c\in\mathbb{N}_0\left(a>c\land c>b\right)\right)$$
So, basically, it says that for all non-negative integers $a$ and $b$ we have that $a>b$ iff $a$ is successor of $b$ or there exists some $c$ which is between $a$ and $b$ (and less than $a$).
These was definitions. Now, lets try to prove some statements using these definitions (and of course ZFC axioms). The first statement I came up with is
Prove that $\exists x\in\mathbb{N}_0(x>0)$.
Here is my solution (I'm posting this just to show an example what kind of detailed proof I'm looking for the final question):
Lets expand the definition of non-negative integers relation symbol $>$ $$\exists x\in\mathbb{N}_0\left(x=\{0\}\lor\exists a\in\mathbb{N}_0(x>a\land a>0)\right)$$ Now, notice that at least one of the stamenets $x=\{0\}$ and $\exists a\in\mathbb{N}_0(x>a\land a>0)$ must be true iff the main statement is true. So, lets consider the first statement $x=\{0\}$. Because $\{0\}=1$, the statement we want to prove is true for $x=1$. However, we need to show that $1\in\mathbb{N}_0$. So, using the definition: $$1\in\mathbb{N}_0\Leftrightarrow1=0\lor\exists a\in\mathbb{N}_0\left(1=\{a\}\right)$$ The $1=0$ is obviously false. Now, we need to show that there is some $a$ for which $1=\{a\}$. Because $1$ is non-empty set, then there must be some set $a$ for which $1=\{a\}$ (in this case $a=0$). The proof is completed.
This was not too hard. However, I came up with the following statement (which I couldn't prove yet):
Prove that $\nexists x\in\mathbb{N}_0(0>x)$.
How to prove it? I tried to apply similar technique like in the previous proof, but I ended up in a recursive chain. I also tried to apply contradiction approach. I supposed that the statement is false, but I again ended up in a recursive chain. Any ideas?
Sorry for bad english. Thank you in advance.
P.S. Please notice that this question is not like standard questions, so maybe not everyone will find it helpful. This is more about recreational math or art of proofs. It is related to core math, ZFC axioms and if you don't find this question helpful, then just move on. Thanks.
Note $2=\{0,1\}$, not $2=\{1\}$.
If you assume there is indeed an $x$ such that $x<0$, well the definition of $<$ is "element of". For example, $1<2$ because $1$ is an element of $\{0,1\}$. Also, 0<2 because 0 is an element of {0,1}.
Note $2<2$ is false because of the axiom of foundation.
Back to x<0 now. Note: $0$ is the empty set and $x<0$ iff $x$ is an element of $0$. The latter proposition is false for all $x$. Contradiction implying it is not the case that $x<0$.