Countable-subset closure (source code)

= Countable-subset closure
{title2=$[X]^{\le\aleph_0}\subseteq X$}

A set has countable-subset closure when every countable subset of it is one of its elements, including the empty subset. In <ZFC>, the <hereditarily countable sets> form the least such set. First realize them as the separated subset of $V_{\omega_1}$ with countable <transitive closure>. Countable unions show closure; <well-founded induction> proves leastness because each of these sets is a countable collection of earlier members.