## 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) $ |

#### Discussion

#### 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.

#### Reference

Wikipedia: Hereditarily finite set