## Hereditarily finite set

### Set

 definiendum $V_\omega$ in it postulate $\emptyset\in V_\omega$ for all $x\in V_\omega$ postulate ${\mathcal P}(x)\in V_\omega$ postulate $x = \emptyset\ \lor\ \exists (y\in V_\omega).\ x = {\mathcal P}(y)$

#### Idea

This is the set of all finite sets constructable when starting with $\emptyset$. It's the smallest infinite Grothendieck universe, as well as a model of ZFC.