For more explanation about how to prove Con(ZFC)→Con(ZFC+¬CH) finitistically, I'd recommend Chapter VII, §9 of Kunen's book Set Theory: An Introduction to Independence Proofs. Here is one relevant paragraph:
We show that, given any finite list, $\phi_1, \ldots, \phi_n$, of axioms of, say, ZFC+¬CH, we can prove in ZFC that there is a countable transitive model for $\phi_1, \ldots, \phi_n$. The procedure involves finding (in the metatheory) another finite list $\psi_1, \ldots, \psi_m$ of axioms of ZFC, and proving in ZFC that given a countable transitive model $M$ for $\psi_1, \ldots, \psi_m$, there is a generic extension, $M[G]$, satisfying $\phi_1, \ldots, \phi_n$. The inelegant part of this argument is that the procedure for finding $\psi_1, \ldots, \psi_m$, although straightforward, completely effective, and finitistically valid, is also very tedious. We must list in $\psi_1, \ldots, \psi_m$ not only the axioms of ZFC "obviously" used in checking that $\phi_1, \ldots, \phi_n$ hold in $M[G]$ (e.g., if $\phi_1$ is the Power Set Axiom, then $\phi_1$ should be listed among $\psi_1, \ldots, \psi_m$), but also all the axioms needed to verify that various concepts are absolute for $M$ ("finite", "p.o.", etc.), as well as the axioms needed to show that certain mathematical results, such as the Δ-system lemma, hold in $M$.