Theorem of Bukovsky characterizing ground models

Question

It was mentioned in a talk that Bukovsky proved the following are equivalent for inner models $M \subseteq V$:

(1) There is a partial order $\mathbb P \in M$ and a $\mathbb P$-generic filter $G \in V$ over $M$ such that $V = M[G]$.

(2) There is a cardinal $\kappa$ such that for every ordinal $\alpha$ and every function $f : \alpha \to \mathrm{Ord}$ in $V$, there is $F : \alpha \to [\mathrm{Ord}]^{<\kappa}$ in $M$ such that $(\forall \beta < \alpha) f(\beta) \in F(\beta)$.

Is this written up somewhere? If not, can you prove it? (Obviously (2) $\rightarrow$ (1) is the hard part.)

Answer 1

The original paper is ``Characterization of generic extensions of models of set theory''

A proof can be found in the master thesis of Giorgio Audrito, "Characterizations of set generic extensions", which is available at Viale's home page here.

Also the paper ''On the set-generic multivers'' by Friedman-Fuchino-Sakai gives a proof. See Friedman's home page.

I may mention that $\kappa$ can be chosen to be the cardinal for which the forcing notion is $\kappa$-c.c.