A question on metamathematics of forcing.

This question might be a duplicate but i have found no other questions related to this so here we go.

In kunens (An introduction to independence proofs) and Nik weavers (forcing for mathematicians) books there is a way to deal with c.t.m.s as follows:
Construct another theory named $\text{ZFC}^+$ which it's language is that of $\text{ZFC}$ but has an additional constant symbol $M$. And it's axioms are:
1) All axioms of $\text{ZFC}$.
2) The single assertion that $M$ is countable and transitive.
3) All axioms of $\text{ZFC}$ relativized to $M$.
Then we prove that $\vdash \text{Con}(\text{ZFC}) \rightarrow \text{Con}(\text{ZFC}^+)$

Now my question: Since we know that $\text{ZFC}^+$ contains a model of $\text{ZFC}$, we can say that $\text{ZFC}^+ \vdash \text{Con}(\text{ZFC})$ and we have $\vdash \text{Con}(\text{ZFC}) \rightarrow \text{Con}(\text{ZFC}^+)$ so we get $\text{ZFC}^+ \vdash \text{Con}(\text{ZFC}^+)$, a contradiction with incompleteness?

No, $\text{ZFC}^+$ does not prove $\text{Con}(\text{ZFC})$. It does not prove that $M$ is a model of ZFC. For each individual axiom $\varphi$ of ZFC, it proves that $M\vDash\varphi$. But it does not prove the single sentence $\forall\varphi\in\mathrm{ZFC} (M\vDash\varphi)$ which is what it would mean to prove that $M$ is a model of ZFC.
(Note that by the completeness theorem, this means it is possible to have a model of $\text{ZFC}^+$ in which the sentence $\forall\varphi\in\mathrm{ZFC} (M\vDash\varphi)$ is false. How can this be? The reason is that in this sentence, $\mathrm{ZFC}$ refers to the set in your model which encodes the set of axioms of ZFC. If the natural numbers of your model are nonstandard, this set will have elements that do not actually correspond to true axioms of ZFC (since their length is actually a nonstandard natural number). So, even though $M$ satisfies every actual axiom of ZFC, your model may not think that $M$ satisfies every element of the set it calls ZFC.)
• Thanks! Another question: i know that when dealing with $\text{PA}$ due to the Lowenheim-Skolem theorem we can have nonstandard models. How can we have nonstandard natural numbers in a model of set theory? I know that our model shouldn't be transitive but what else do we need to do? – Shervin Sorouri Sep 15 '18 at 7:08
• Add a new constant symbol $c$ to ZFC and add axioms saying $c\in\omega$ and $c>n$ for each natural number $n$. Any finite subset of these is satisfiable (assuming ZFC is consistent), since $c$ could just be a sufficiently large number. So, by compactness, there is a model of all of them at once. – Eric Wofsey Sep 15 '18 at 7:10