Motivation: With the following I want to understand the relationship between the set-theoretical natural numbers 0,1,2,... and the set of natural numbers $\omega$ better.
Let 0 := $\emptyset$, 1 := {$\emptyset$}, 2 := {$\emptyset$, {$\emptyset$}}... be the usual set-theoretical natural numbers and let $\omega$ be the set of natural numbers.
For a fixed n (for $n \geq 1$), let $\varphi(x)$ be a first-order formula defining the class of sets in n. Correct me if I am wrong, but one should now be able to show that
$$\textbf{ZFC} \vdash ((x = \textbf{0} \lor ... \lor x = \textbf{n-1}) \leftrightarrow \varphi(x)).$$
Now let $\varphi(x)$ be a first-order formula defining the class of sets in $\omega$. For bigger and bigger $n$ one should still be able to show (using longer and longer proofs) that
$$\textbf{ZFC} \vdash ((x = \textbf{0} \lor ... \lor x = \textbf{n-1}) \rightarrow \varphi(x)).$$
The analogous result
$$\textbf{ZFC} \vdash (x = \textbf{n} \rightarrow \varphi(x))$$
being obtainable (by metamathematical induction) for any n seems to be a sensible way of "proving" that
(1) The set-theoretical natural numbers are contained in $\omega$.
It seems however, that not being able to form the infinite disjunction $(x = \textbf{0} \lor x = \textbf{1} \lor ...)$ restricts us to this "collection of proofs" making up the desired statement (1). This leads me to
Question 1: Is there a sensible first order expression meaning that every set-theoretical natural number is contained in $\omega$?
The other direction appears to be even worse. It seems that one cannot even give a "collection" $(\varphi_n)$ of first-order expressions indexed by naive natural numbers, s.t.
$$\textbf{ZFC} \vdash \varphi_n$$
is true for all $n$ (e.g. proven by metamathematical induction) and one can view this collection of proofs as a "proof" of
(2) Every set in $\omega$ is a set-theoretical natural number.
This leads me to
Question 2: Is there a sensible collection of first order expressions indexed by naive natural numbers meaning that every set in $\omega$ is a set-theoretical natural number?
If the answer is yes, then I ask for more in
Question 3: Is there a sensible first order expression meaning that every set in $\omega$ is a set-theoretical natural number?
Remark: If one just wants to talk about models of ZFC inside the universe, then one should be able to find appropriate formulas for all 3 questions using encodings of expressions, a provability predicate, and so on (tell me if I misunderstood this). Assuming the answer to my questions is always no: Is this then another case of "property cannot be checked in the universe (i.e. model of ZFC we are in) but can be checked for the models of ZFC inside the universe"?
Lastly, thank you for reading all of this.