As is standard in Kunen, we can talk about $WF$ by working up to it through the "sets of rank $n$" function, $R$, defined in the usual way by iterating collection.
In particular, for limit ordinals $\gamma$ we take
$R(\gamma)= \bigcup_{\alpha < \gamma} R(\alpha)$.
It is then standard to take the hereditarily finite sets $HF = V_\omega$ to be $R(\omega)$.
My question, more specifically, pertains to the axiom of infinity and how $HF$ models $ZF \wedge \neg Infty$. I understand that the gist of the proof is that it only contains finite elements, but its construction involves $\omega$ by the definition of the $R$ function, and $\omega$ being a set necessitates the axiom of infinity. How then does $HF$ model $ZFC \wedge \neg Infty$ if we need an infinite set to exist in order to even talk about it?
Additionally, we would need $V_{\omega}$ to be a proper class, so my language ("contains" finite elements...) is imprecise, but this seems less conceptually difficult in comparison to my previous issue. Nevertheless some clarity on how to deal with this issue more precisely would be good.
(Since logicians seem to get by I assume my issue is either misinformed or unimportant insofar as model theory is concerned. I'd like the explanation regardless.)
The kicker here is that $\omega$ is external to the model, since $\omega\notin R(\omega).$ This means that, as far as the model is concerned, $\omega$ is a proper class--the proper class of all ordinals. Furthermore, since $V_\omega\notin V_\omega,$ then $V_\omega$ is also a proper class, as far as the model is concerned--namely, the proper class of all sets.
What we're doing here is constructing an inner model. Assuming that $\mathsf{ZF}$ holds, then $V_\omega$ exists, and it can be shown that all axioms of $\mathsf{ZF}$ (except the Axiom of Infinity, which fails) still hold if we restrict our sets to those in $V_\omega$.