Internal Power Set in L

In the ambient universe use Separation on $\mathcal{P}(a)$ to form $Y=\{b\subseteq a:b\in L\}$. The predicate of belonging to L is uniformly definable. Ambient Replacement collects $R=\{{\rho }_L(b):b\in Y\}$; put $\beta =\sup (R\cup \{{\rho }_L(a)\})+1$. Then $a\in L_{\beta }$ and $Y\subseteq L_{\beta }$. This bounds all constructible subsets simultaneously without using Power Set or Replacement in L.

The set $L_{\beta }$ is itself an element of L. Apply F1 inside L to this set with the predicate $b\subseteq a$. For $a,b\in L$, this predicate is absolute directly: every member of $b$ lies in L by transitivity, and membership in $a$ is actual membership. The separated set is therefore $\{b\in L_{\beta }:b\subseteq a\}=Y$ by step 1.1. It belongs to L and contains exactly the internal subsets of a, proving internal Power Set.