I was recently told that the following (due to M. Viale) is a nice theorem:

Suppose there are arbitrarily large supercompacts, and $\mathrm{MM}$ holds in $V$. Let $G$ be generic for a proper forcing and $V[G] \vDash \mathrm{MM}$. Then $L(P(\omega_1))^V$ is elementarily equivalent to $L(P(\omega_1))^{V[G]}$.

My question (borne of ignorance, not skepticism) is:

Why is this theorem nice, and how does it fit into the bigger picture?

Some slightly-more-specific questions that refine my main question are: Do the hypotheses of this theorem often come up in natural settings? What's the upshot of the conclusion? Is it that proper forcing which preserves $\mathrm{MM}$, leaves the theory of a small but not-that-small chunk of the universe unchanged?

I was recently told that the following is a nice theorem:

Suppose there are arbitrarily large supercompacts, and $\mathrm{MM}$ holds in $V$. Let $G$ be generic for a proper forcing and $V[G] \vDash \mathrm{MM}$. Then $L(P(\omega_1))^V$ is elementarily equivalent to $L(P(\omega_1))^{V[G]}$.

My question (borne of ignorance, not skepticism) is:

Why is this theorem nice, and how does it fit into the bigger picture?

Some slightly-more-specific questions that refine my main question are: Do the hypotheses of this theorem often come up in natural settings? What's the upshot of the conclusion? Is it that proper forcing which preserves $\mathrm{MM}$, leaves the theory of a small but not-that-small chunk of the universe unchanged?