You got it, absolutely. So yes there are models where as far as the model is concerned there is a set that satisfies the axioms of real numbers, and furthermore

You got it, absolutely. So yes there are models where as far as the model is concerned there is a set that satisfies the axioms of real numbers, and furthermore all elements of that set are actually definable (but not definable from within that model), but that set is not the standard notion of real numbers. It's just that it's impossible to provide a set of axioms that defines the real numbers and only the real numbers (in first order logic), so for any definition of the real numbers you end up with a model that will satisfy that definition but doesn't actually model the "standard notion of real numbers". The reason I brought this up is because when you said that there are models of ZFC where every real is definable, those reals are only definable from outside of the model. From within that model there are still undefinable reals and hence I don't think it matters too much to the point lisper is making. Maybe to put it another way, there is no model of the reals where within that model all reals are definable, and hence lisper's point stands.