It can be shown in $ZFC$ that $V_{\omega}$ is a model of $ZFC$ minus Infinity, so $$ZFC\vdash CON(\ulcorner ZFC-\mathrm{Inf}\urcorner)$$ (where $V_{0}=0$, $V_{\alpha +1}=P(V_{\alpha})$, $V_{\alpha}=\cup_{\beta\lt\alpha} V_{\beta}$ if $\alpha$ is a limit).
One can prove that $ZF\vdash(ZF+AC)^{\mathbf{L}}$ for the constructible class $\mathbf{L}$. So we have, in a finitistic way, $Con(ZF)\rightarrow Con(ZFC)$. From this, one can also deduce $$ZF\vdash CON(\ulcorner ZF\urcorner)\rightarrow CON(\ulcorner ZFC \urcorner)$$ and so $ZFC\not\vdash CON(\ulcorner ZF \urcorner)$ by the Goedel's second incompleteness.
At this point, I wonder why some fragments of $ZFC$, e.g., $ZFC- \mathrm{I}\mathrm{n}\mathrm{f}$ and $ZFC- \mathrm{P}$, can be shown its consistency in $ZFC$, but some, for example $ZFC-AC$, should not be. I mean, why can we not to construct a set model of $ZF$ in $ZFC$, where we can construct a set model of $ZFC-\mathrm{Inf}$ or of $ZFC-\mathrm{P}$?
Best Answer
You seem to have answered the question yourself in the second paragraph. If we could prove there were a set model of ZF in ZFC, then the constructible universe of that model would be a set model of ZFC, and we would have proved Con(ZFC) in ZFC, which is impossible by GIT, unless ZFC is inconsistent.
The fact that the constructible universe is a model of ZFC (and GCH, $\lozenge,$ $\lnot$SH etc) is good news in the sense that it shows AC, et. al. will not cause an inconsistency that wasn't already there in ZF. But from the perspective of hoping we might be able to prove Con(ZF) by adding choice, it's bad news.