Ambient constructible power sets when the reals are not well-orderable (source code)

= Ambient constructible power sets when the reals are not well-orderable
{title2=$a\in L\Longrightarrow(\mathcal P^V(a)\in L\iff a\text{ is finite})$}

If the ambient <power set> of $\omega$ is not well-orderable and $a\in L$, then the full ambient <power set> of $a$ belongs to $L$ exactly when $a$ is finite. <Finite set> operations give the forward construction for finite $a$. If $a$ is infinite, its constructible well-order gives an <injection> $\omega\to a$. The induced <injection> of <power sets> would make the ambient <power set> of $\omega$ well-orderable if $\mathcal P(a)$ belonged to $L$.