Formally proving the consistency of a formal theory This is based on a related question. I did some further reading to understand the problem. I'm just posting this question to check whether I have correctly understood the solution.
Let's say we are using ZFC as our meta-language (in standard first order logic). We have proven that a theory is consistent iff it has at least one model, and we have defined the satisfaction relation $\models$.
Now we wish to show that some formal theory $\Gamma$ is consistent. To do this, formally speaking, we would need to:

*

*Define the constant, relation and function symbols as sets. Prove each definition describes a unique and existing object (using axioms of ZFC). Define another set $\Gamma$ containing the required axioms of our formal theory.
Also, by doing this, we have extended ZFC with definitions that makes $\mathcal{L}(\Gamma)$ a sub-language of extended-ZFC. This is required for the following.


*Derive the axioms of $\Gamma$ as properties of the defined sets. The proof would be in the language of FOL and would be limited to the axioms of extended-ZFC.


*Construct a tuple $\mathfrak{M} = \langle \ldots \rangle$ listing the constructed sets. This is a $\Gamma$-structure.


*Using the definition of the satisfaction relation, prove that $\mathfrak{M} \models \Gamma$. The proof would again be in the language of FOL and would be limited to the axioms of extended-ZFC.


*Thus, there exists a model of $\Gamma$. Therefore, it is consistent.
Am I right in thinking this is all we need to do, formally speaking? I know in practice we only need to do steps 1 and 2.
One important thing I learned is that, in this situation, we must pick a meta-language that allows us to talk about both $\Gamma$ and its model $\mathfrak{M}$.
Note: I am only looking to check my intuition. There may be better ways of proving consistency, but I am wondering whether my naive understanding could also work, and if not, what the problem is.
Update: I realized that one could regard ZFC as our theory instead, and simply define $\Gamma$-symbols in it. Then steps 1 and 2 are sufficient. But in doing so, ZFC is no longer a meta-theory, and so this solution addresses a different problem.
 A: As Alex Kruckman writes in a comment, it is not necessary to change the language of ZFC. We do not need to prove $\Gamma$ in ZFC, and we do not need to specifically define the model $M$, we only need to prove that it exists.
So, working in ZFC, what we need to do is: 


*

*Write a formula $\phi(N,T)$ of ZFC which expresses "the set $N$ is a model of the theory $T$."

*Prove that there is a set $M$ which is a model of our particular theory $\Gamma$. In other words, prove $(\exists M)\phi(M,\Gamma)$ for the $\phi$ in step 1. Note that we do not need to "define" $M$ or show that it is unique, we only need to prove that it exists. We do not need to extend the language of ZFC. 

*Prove that the model $M$ from step 2 cannot satisfy any contradictory sentence.

*Show that if $\Gamma$ was inconsistent then the model $M$ from step 2 would need to satisfy some contradictory sentence. 
Parts (1), (3), and (4) are standard results, which do not rely on $\Gamma$ in any special way. These are covered in any reasonable logic textbook, and I would just call them "formalizing first-order logic in ZFC". Only step (2) has to be adjusted to the particular theory $\Gamma$. 
