About proving that the Continuum Hypothesis is independent of ZFC In Mathematical Logic, we were introduced to the concept of forcing using countable transitive models - ctm - of $\mathsf{ZFC}$. Using two different notions of forcing we were able to build (from the existence of a "basic" ctm) two different ctm's, where one of them verifies the continuum hypothesis ($\mathsf{CH}$), and the other verifies its negation.
My question is the following. Does this prove that $\mathsf{CH}$ is independent of $\mathsf{ZFC}$? It seems to me that the only thing this proves is: "If there is a ctm of $\mathsf{ZFC}$ then $\mathsf{CH}$ is independent of $\mathsf{ZFC}$". And, well, we cannot prove in $\mathsf{ZFC}$ that there is a ctm of $\mathsf{ZFC}$, since that would imply that $\mathsf{ZFC}$ proves its own consistency!
What am I missing here? Is it enough to assure the existence of a ctm in some "universe" different from $\mathsf{ZFC}$? Does this even make sense?
Thank you in advance.

As Asaf points out, we can still get the relative consistency results we want without "leaving" ZFC. But I think it is worth noting that there are natural extensions of ZFC in which the existence of ctm's of ZFC are provable, and thus in which we can carry out forcing arguments as is. 
One natural extension arises from adding to ZFC a satisfaction predicate $Sat(x, y)$ with the usual Tarkian clauses for the connectives and quantifiers. For instance, we would add:
(&) $Sat(\phi\wedge\psi, a) \leftrightarrow Sat(\phi, a) \wedge Sat(\psi, a)$
where $a$ is an assignment function.  
Once we have $Sat(x, y)$ in our language, it is natural to extend the replacement schema to formulas involving it. In the resulting theory we can prove that there are closed and unbounded $\alpha$ such that $V_\alpha$ is an elementary substructure of $V$. Each such $V_\alpha$ models ZFC, and it is then straightforward to get our ctm's using a Skolem hull argument on any one of them followed by the Mostowski collapse lemma.
