Hereditarily countable constructible sets appear below omega-one (source code)

= Hereditarily countable constructible sets appear below omega-one
{title2=$H_{\omega_1}^L=L_{\omega_1}^L$}

Inside the <constructible universe>, every <hereditarily countable set> appears in a countable level of the <constructible hierarchy>. Take a countable <elementary substructure> of a sufficiently large $L_\eta$ containing its <transitive closure> pointwise. The <condensation lemma for the constructible universe> identifies the collapse with $L_\beta$ for countable $\beta$, and the collapse fixes the original set. Conversely, a countable-indexed level is countable inside the <constructible universe>.