Let $A_0$ be a finite set, and consider the sets $A_i = A_{i-1} \cup \mathcal{P}(A_{i-1})$ for all $i > 0$, where $\mathcal{P}$ denotes powerset. Does $\bigcup_{j=0}^{\infty} A_j$ exist as a set?
Intuitively, it seems true because each $A_i$ is a finite set, so the class corresponding to the union must be countable. However, I am unsure how to go about proving this from the axioms, since the power set operator is not actually a function, so the definition of $A_i$ does not immediately give a set-theoretic sequence. (It seems reminiscent of the class of hereditarily finite sets $V_\omega$, but I am having trouble finding a proof that $V_\omega$ is a set.)