Well, technically not every model of ZFC has a ZFC-modelling element. There is a model of “ZFC+¬Con(ZFC)”, and no element of this monster can be a model of ZFC. Not even with nonstandard element-relation.
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.
Well, technically not every model of ZFC has a ZFC-modelling element. There is a model of “ZFC+¬Con(ZFC)”, and no element of this monster can be a model of ZFC. Not even with nonstandard element-relation.
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)