Does Con(ZFC) imply Con(ZFC+Con(ZFC))? Assume that the consistency of ZFC set theory implies the consistency of ZFC+Con(ZFC), where the latter adds the axiom that ZFC is consistent. $ZFC+Con(ZFC) \vdash Con(ZFC)$, because it took it as an axiom. So by our hypothesis $ZFC+Con(ZFC) \vdash Con(ZFC+Con(ZFC))$. Then Gödel's second incompleteness theorem tells that Con(ZFC+Con(ZFC)) is false. And still by our hypothesis, that means ZFC itself is inconsistent.
So if we believe that ZFC is consistent (as I do), we would prefer that Con(ZFC) does not imply Con(ZFC+Con(ZFC)). In other words, a contradiction in ZFC+Con(ZFC) would not translate into a contradiction in ZFC. But by the deduction theorem, a contradiction in ZFC+Con(ZFC) would translate into $ZFC \vdash \lnot Con(ZFC)$, i.e. a refutation of Con(ZFC) by ZFC. And that unfolds into $ZFC \vdash (\exists P, ZFC \vdash P \text{ and } ZFC \vdash \lnot P)$. Then this P seems a contradiction in ZFC again ?
 A: It is quite possible that $\sf ZFC$ proves $\lnot\operatorname{Con}\sf (ZFC)$ without $\sf ZFC$ being actually inconsistent.
We know that if $\sf ZFC$ is consistent, then $\sf ZFC+\lnot\operatorname{Con}(ZFC)$ is consistent. So we can look at the following theory: $$\sf ZFC+\operatorname{Con}(ZFC+\lnot\operatorname{Con}(ZFC))+\lnot\operatorname{Con}(ZFC+\operatorname{Con}(ZFC))$$ which is just a bit stronger than $\sf ZFC$, about the same as $\sf ZFC+\operatorname{Con}(ZFC)$.
Take a universe in which this theory holds. Then $\sf ZFC$ is consistent, but there is no model of $\sf ZFC$ in which $\operatorname{Con}\sf (ZFC)$ is true. Therefore $\sf ZFC$ proves, in that universe, $\lnot\operatorname{Con}\sf (ZFC)$.

The point here is that we very much depend on the meta-theory, but there is no problem with a consistent theory proving its own inconsistency.
The key issue here, which is what bothers you, is that while it is true that a real proof translates to an arithmetic sequence coding that proof, therefore $T\vdash\varphi$ translates to the arithmetic statement corresponding to this proof; but in the other direction, if we have non-standard integers, these will encode proofs that are not "real proofs" from the [meta-]meta-theory perspective, so they are not representing "reality".
So, it's true that if there is an actual proof from $\sf ZFC$ that $0=1$, then $\lnot\operatorname{Con}\sf (ZFC)$ is true. But by assuming $\sf\operatorname{Con}(ZFC+\lnot\operatorname{Con}(ZFC))$, one is essentially assuming the existence of non-standard integers which code that proof of inconsistency, which will not correspond to an actual proof (as that would contradict the fact that a theory containing $\sf ZFC$ was assumed to be consistent in the first place!).
