ZFC allows models of second order PA and proves that those models are all isomorphic. Within each model of ZFC there is no such thing as a nonstandard model of second order PA. One can only think it is nonstandard by looking from outside the model, no? What theorem of second order PA is ZFC unable to prove?
This is similar to how there are countable models of ZFC but those models think of themselves as uncountable. They are countable externally and not internally.
