Nested transitive models from a worldly cardinal (source code)

= Nested transitive models from a worldly cardinal

A <worldly cardinal> permits a <countable transitive model> $M$ of <ZFC> and a <transitive model> $N$ of <ZFC> with $M\in N$, $|N|=\aleph_1$, and $(\omega_1)^N=\omega_1$. First collapse a countable <elementary substructure> of $V_\kappa$. Then collapse an $\aleph_1$-sized <Skolem hull> containing every countable ordinal and every member of $M$, as well as $M$ itself. The <transitive collapse fixes transitive subsets> lemma preserves $M$ and those ordinals.