Can someone help me? How one does metaproofs? Let's say I want to prove that if I have a countable language alphabet then I have a countable set of strings over that alphabet too! Is the main idea that I use the same logic rules like when I do formal proofs plus some system of axioms but let's say I decide to use the same ZFC again.

Then I just encode entities like natural numbers in zfc or ordered pairs in zfc so for example I encode string and alphabet into zfc and then I prove my main theorem about those encoded sets and from that I conclude that I proved what I wanted?