Absoluteness of $ \text{Con}(\mathsf{ZFC}) $ for Transitive Models of $ \mathsf{ZFC} $.

Solution 1:

Yes, $\text{Con}(\mathsf{ZFC})$ is an arithmetic statement ($\Pi^0_1$ in particular, because it says a computer program that looks for an inconsistency will never halt) so it is absolute to transitive models, and your proof is correct.

By the way, there are a couple of ways you can strengthen it. First, arithmetic statements are absolute to $\omega$-models (models with the standard integers, which may nevertheless have nonstandard ordinals) so $\text{Con}(\mathsf{ZFC})$ does not prove the existence of an $\omega$-model of $\mathsf{ZFC}$. Second, the existence of an $\omega$-model of $\mathsf{ZFC}$ does not prove the existence of a transitive model of $\mathsf{ZFC}$, because the existence of an $\omega$-model of $\mathsf{ZFC}$ is a $\Sigma^1_1$ statement, and $\Sigma^1_1$ statements are absolte to transitive models.