I am wondering that if one can show $ZFC \vdash CON(\ulcorner ZFC-P \urcorner)$. There is an argument in Set Theory, An Introduction to Independence Proofs by Kunen (page 145), but I am confused about the proof.

Let $\phi$ be the formula for the coding of $ZFC-P$ in natural numbers, and $X_{ZFC-P}=\{n\in \omega :\phi(n)\}$.

By Godel Completeness Theorem as the formal sentence $\forall X (CON(X) \leftrightarrow \exists \mathfrak{M}(\mathfrak{M} \models X) )$, it is enough to prove that: $ZFC \vdash H(\omega_1) \models X_{ZFC-P} $, or say $ZFC \vdash \forall x \in X_{ZFC-P} (H(\omega_1) \models x)$. By Completeness and Soundness Theorems, it is enough to show that whenever $M$ is model of $ZFC$, $M$ models $\forall x \in X_{ZFC-P} (H(\omega_1) \models x)$. This amounts to showing for all $x \in X_{ZFC-P}$, $H(\omega_1) \models x$ is true in $M$.

However, if $M$ is a nonstandard model which has nonstandard natural numbers, $X_{ZFC-P}$ may be strictly larger than the actual collection of codings of $ZFC-P$. Let $x_0$ be the coding of a nonstandard axiom $\psi$ which has infinite length looking from outside while we have $\phi(x_0)$. In Kunen's book, they showed $H(\omega_1) \models x$ for actual axioms of $ZFC-P$, but not for infinite sentences like $\psi$.

In fact, $CON(\ulcorner ZFC-P \urcorner)$ as a formal sentence also includes possible nonstandard axioms. I am wondering that if there is a way to deal with these nonstandard axioms, or if one can show $ZFC \vdash CON(\ulcorner ZFC-P \urcorner)$.