$PA$ and $ZFC-Infinity$ are mutually interpretable, meaning that a model of one is a model of the other and every axiom and theorem can be translated to the other system.
One of the $ZFC - Infinity$ axioms is the axiom of pairing, which states that for any two sets $a$ and $b$, the set $\{a,b\}$ exists.
My question is: how does the axiom of pairing translate to $PA$? My understanding is that one of the reasons $\omega$ is not a model of $ZFC$ is because it doesn't satisfy the axiom of pairing (e.g. $\{23,53\}$ is not a subset of $\omega$). Of course it is also not a model of $ZFC$ because it doesn't satisfy the axiom of infinity. But what I don't understand is how removing the axiom of infinity makes $\omega$ satisfy the axiom of pairing. My understanding is that if the two theories are mututally interpretable, that means that there is some theorem of $PA$ that is equivalent, given the translation, to the axiom of pairing. What does this theorem say and what does $\{23,53\}$ look like in $PA$, is it just a Gödel encoding made up of natural numbers?
One interpretation of the language of set theory into the language of arithmetic, due to Ackermann, is to view each natural number $m$ as a code for a set $S_m$, as follows: $S_n \in S_m$ if and only if the $n$th binary digit of $m$ is $1$. It can be shown that if we then translate the ZFC axioms to use this interpretation, the translated axioms of $\text{ZFC}^-$ are all provable in PA. This is how we show that PA interprets $\text{ZFC}^-$.
How do we prove pairing in this interpretaton? Easily enough: we only have to show that for all $n_1$ and $n_2$ there is an $m$ so that only the $n_1$st and $n_2$nd binary digits of $m$ are $1$. And, because PA proves that $2^{n_1}+2^{n_2}$ exists for all $n_1$ and $n_2$, this is no problem.