===== Hereditarily finite set =====
==== Set ====
| @#FFBB00: definiendum | @#FFBB00: $V_\omega$ in it |
| @#55EE55: postulate   | @#55EE55: $\emptyset\in V_\omega$ |
| @#FFFDDD: for all     | @#FFFDDD: $x\in V_\omega$ |
| @#55EE55: postulate   | @#55EE55: ${\mathcal P}(x)\in V_\omega $ |
| @#55EE55: postulate   | @#55EE55: $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: [[http://en.wikipedia.org/wiki/Hereditarily_finite_set|Hereditarily finite set]]

-----
=== Requirements ===
[[Power set]], [[Empty set]]
=== Element of ===
[[Grothendieck universe]]
=== Related ===
[[Set universe]]