Working in $\mathcal L(=,\in)_{\omega_1, \omega}$, having axioms of:
$\textbf{Extensionality: } \forall z (z \in x \leftrightarrow z \in y) \to x=y$
$\textbf{Empty: } \exists x \forall y \, (y \not \in x)$
$\textbf{ Define: } x=\varnothing \iff \forall y \, (y \not \in x)$
$\textbf{Finite construction: } \bigwedge_{n \in \omega} \forall v_0..\forall v_n \exists x: x=\{v_0,..,v_n \} $
$\textbf{Define: } \operatorname {fin}(x)= x=\varnothing \bigvee_{n \in \omega} \exists v_0 .. \exists v_n: x=\{v_0,..,v_n\}$
Is the following a theorem of this theory?
$\forall x: \neg[ \bigwedge_{n \in \omega} \exists v_0 .. \exists v_n: \bigwedge_{i \in n} (v_{i+1} \in v_i) \land v_0=x] \implies \operatorname {fin} (x) $
In English: every truly finitely ranked set is a truly finite set.