Linked impressive authority says the model has a ZFC-model-encoding element, plus enough nonstandard quoted ZFC axioms in-model that in-model ZFC doesn’t think it’s a ZFC-model-encoding element. I.e., the formula for “semantically entails ZFC” is false within the model, but from outside, using our own standard list of axioms, we think the element is a model of ZFC.
Linked impressive authority says the model has a ZFC-model-encoding element, plus enough nonstandard quoted ZFC axioms in-model that in-model ZFC doesn’t think it’s a ZFC-model-encoding element. I.e., the formula for “semantically entails ZFC” is false within the model, but from outside, using our own standard list of axioms, we think the element is a model of ZFC.
Ah, sorry, I didn’t notice that the question is about model of ZFC inside a “universe” modelling ZFC+Con^∞(ZFC)