lo.logic - Models within a model of set theory

There is an interesting observation surrounding the latter
part of your post, recently discussed in an article of
Brice Halimi (Université Paris Ouest), that many set
theorists find surprising. It is the following:

Theorem. Every model of ZFC contains an element that
is a model of all the ZFC axioms.

To be more precise, if $langle M,{in}^Mrangle$ is a
model of of ZFC, then there is an object $n$ in $M$ which
$M$ thinks to be a model in the language of set theory and
furthermore, every individual axiom of ZFC is true in $n$.

The proof is relatively simple (and it seems that each part
of it was known classically, although Brice has pulled them
nicely together). Suppose that $langle M,{in}^Mrangle$
is a model of ZFC. This implies, of course, that ZFC is
consistent. If it happens that $M$ is $omega$-standard,
meaning that it has no nonstandard natural numbers, then
$M$ will have the same proofs that we do outside of $M$,
and so $M$ will agree that ZFC is consistent. Hence, by the
Completeness theorem, $M$ will be able to build a model of
ZFC, such as by the Henkin method. Alternatively, suppose
that $M$ is $omega$-nonstandard. We know that for any
natural number $m$, the Reflection theorem ensures that
some $V_alpha$ is a model of the $Sigma_m$-fragment of
ZFC. Thus, inside $M$, every standard $m$ has the property
that there is some $(V_alpha)^M$ satisfying the $Sigma_m$
fragment of the (nonstandard) version of ZFC inside $M$.
Since the standard cut of the natural numbers is not
amenable to $M$, it must be that there is some nonstandard
natural number $k$ such that $M$ believes that there is
some $(V_alpha)^M$ satisfying what $M$ thinks is the
$Sigma_k$ fragment of ZFC. Since this includes all the
standard part of ZFC, we find in this case that there is a
model of ZFC inside $M$, as desired. QED

The reason set-theorists often find the result surprising
is that on its face, it seems to conflict with the
consequence of the Incompleteness theorem, that if ZFC is
consistent, then there are models of
$ZFC+negtext{Con}(ZFC)$. A model of this theory can have
no element that it thinks is a model of ZFC. The difference
between this result and the result above is exactly the
difference that your question is about: the model $n$
inside $M$ is not a model of the full nonstandard version
of ZFC inside $M$, but it is a model of all the standard
ZFC axioms.