Just as an exercise in formula manipulation, I tried to find the simplest formula $\phi(x)$ with one free variable $x$ in the language of ZFC that defines the first transfinite ordinal $\omega$ (i.e. $\phi(x) \leftrightarrow x=\omega$). Here is my attempt (operator precedence follows the Wikipedia): $\begin{align}\phi(x):=\exists a (a \in x) \land \forall a \forall b \forall c ((a \in x \lor a = x) \to (c \in b \to (b \in a \to c \in a))) \land \\ \forall a (a \in x \to (\exists b (a \in b \land b \in x) \land (\exists b (b \in a) \to \exists b (b \in a \land \neg \exists c (b \in c \land c \in a)))))\end{align}$ It means that $x$ is non-empty ordinal (transitive set with transitive elements) that is not a successor ordinal, but each its non-empty element is a successor ordinal.
Is this formula correct? Can anybody suggest further simplification?