What does a proof that $\mathcal{N}$ is a model of $PA$ look like? What does a proof that $\mathcal{N} \models PA$ (where $\mathcal{N}$ is the structure $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq)$, $\models$ is the satisfaction relation, and $PA$ is first-order Peano arithmetic) look like? By which I mean, what machinery is used in whatever meta-theory is being used for this proof? If Tarski's undefinability theorem says that a theory (with sufficient arithmetical power) can never define the truth of its own formulas and we need a meta-theory to handle that task, how does the meta-theory handle that task?
I have seen it said that systems much weaker than $PA$ can be used as the meta-theory for these results, e.g. primitive recursive arithmetic. How does $PRA$ prove that $\mathcal{N}$ is a model of $PA$, when $PA$ is much stronger than $PRA$? What aspect of $PA$ allows it to prove $V$ is a model of $ZFC$? I can only assume it's done through Gödel coding, what exactly is being encoded?
I understand that an interpretation is a tuple $<D,F>$ where $D$ is a domain of individuals ands predicates/functions and $F$ is a function that maps each member of $D$ to the syntactic objects of whatever theory is being talked about (which means that the interpretation is a meta-object, correct?). How, then, does $PRA$ prove "$<$($\mathbb{N}$ $, 0, 1, S, +, \times, \leq), F>$ correctly satisfies PA"? Or to get more to the point of my confusion, how does PRA assure that "when $F$ interprets the sentences of PA with $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq)$, there is never a sentence that is interpreted falsely" when $F$ is chosen correctly? Wouldn't $PRA$ need to prove either a statement about an infinite object, which it cannot do, or an infinite amount of things for this to be the case? Is this getting into Hilbert's idea of a finitary proof and an example of the impossibility of what he wanted?
Intuitively, I believe that $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq)$ does satisfy $PA$ under a proper assignment, but that is only because I have seen it said many times that PA captures the correct notions of arithmetical addition and multiplication and  because of my (innate and naively platonistic) belief that $\mathbb{N}$ exists and arithmetic is well defined. By which I mean, I do not believe it because I have seen the mechanics of a formal proof that $\mathcal{N} \models PA$, and that is what I would ultimately like to see. To paraphrase, my justification for why I believe $($$\mathbb{N}$ $, 0, 1, S, +, \times, \leq) \models PA$ is because of inductive (real induction, not mathematical) reasons and not deductive reasons, and I would hopefully like to see a deductive proof.
This question is motivated by my confusion about what exactly is allowed to happen and does happen in a meta-theory, and I used a lot of individual questions to try and outline my specific confusion. That being said, I really don't want this question to be closed for asking multiple questions, especially because it isn't actually. So I'll reiterate that the real question that I'm asking is the same as the question in the title: 

What does a proof (in, for example, $PRA$) that $\mathcal{N}$ is a model of $PA$ look like?

 A: To prove that any model $M$ is a model of PA, in the usual sense of "model of PA", you have to work in a metatheory that has the ability to form the satisfaction relation $\models$ for $M$.  Otherwise, the metatheory can't express "is a model". 
Compare this outline of how ZFC set theory proves that $\mathbb{N} \models \text{PA}$. First, we can use ZFC to form the satisfaction relation $\models$ for $\mathbb{N}$. Second, we look at how $\mathbb{N}$ is defined in ZFC to see that the satisfaction relation thinks that all the basic axioms are true. Finally, we again use the way that $\mathbb{N}$ is defined in ZFC to show that it satisfies each of the induction axioms of PA.  This fact that ZFC proves $\mathbb{N} \models PA$ also leads quickly to the theorem that ZFC proves PA is consistent. 
Weak theories like PRA do not have enough strength to even talk about satisfaction relations, much less construct them.  So, in PRA, we cannot directly express a relation such as $\mathbb{N} \models \phi$.  Moreover, we know that PRA does not prove that PA is consistent, so we know there will be some real limits on how much we can prove about PA in PRA. 
PRA is mostly useful as a metatheory when we are working syntactically, looking at proofs instead of models. In that situation, although PRA doesn't prove the consistency of many theories, it can prove the relative consistency of many pairs of theories, e.g $\text{PRA}\vdash \text{Con}(\text{ZFC})\to\text{Con}(\text{PA})$.  PRA is also strong enough to prove formalized versions of Gödel's incompleteness theorem and Tarski's undefinability theorem - both of which, in the end, are about provability. But PRA can only do so much, because it is an extremely limited theory.  
Similarly, PA cannot express what it would mean for the set theoretic universe to model ZFC. PA has no way to define the satisfaction relation 
$\models$ for $V$. Even ZFC itself can't do that.  But, more generally, PA is not able to talk about sets or models in the way that we talk about them in introductory logic. 
For metatheoretic results involving models, the easiest metatheory to work in is ZFC set theory. Occasionally we need to look at stronger systems, but only when we look at the metatheory of set theory itself. Occasionally we work in weaker, intermediate systems, but these are mostly of technical interest. 
