Axioms satisfied by hereditarily countable sets (source code)

= Axioms satisfied by hereditarily countable sets
{title2=$HC\models\mathrm{ZFC}-\mathrm{PowerSet}$}

The <transitive set> of <hereditarily countable sets> satisfies every <ZFC> axiom except the <Axiom of power set>. For internal definable functions on a countable domain, ambient <Axiom schema of replacement> gives a countable range of hereditarily countable sets, which belongs to the structure by <countable-subset closure>. The same closure proves <axiom schema of collection> and retains countable choice-function graphs. All subsets of $\omega$ are elements, but their uncountable full power set is not an element, so Power Set fails.