"Proof" that ZFC is inconsistent using Turing machines

I came across the following "proof" for the inconsistency of ZFC and can't find the flaw in it (if there is one...):

Construct a Turing machine A which sequentially runs on all proofs in ZFC and checks if the claim "A does not halt or ZFC is inconsistent" is proved. If such a proof is found, A halts.

Note that A can know its encoding - see Kleene's recursion theorem - and even if it can't this "obstacle" can be overcome. So it seems to me such A is constructible.

Now, if A halts then it is because it has found a proof for "A does not halt or ZFC is inconsistent". Since A halted, it is implied that ZFC is inconsistent. So either A does not halt, or ZFC is inconsistent.

Now (and my guess is that this is the part where this proof "cheats") we have just proved the claim "A does not halt or ZFC is inconsistent", so such a proof exists in ZFC. So A must halt on this proof - and we have seen that this implies that ZFC is inconsistent.

Where is the mistake?

Here's my take on it. Use $(A \uparrow)$ to mean $A$ does not halt, and $(A \downarrow)$ to mean $A$ does halt. Let $\Phi$ be any sentence; the question uses $\lnot\operatorname{Con}\mathrm{(ZFC)}$ but this is not material. Let $\operatorname{Pvbl}(b)$ be the standard $\mathrm{ZFC}$-formalized provability predicate, which says that there is a coded proof of the formula with number $b$.

The question is right that, by the recursion theorem, we can create a specific machine $A$ such that $$ (A \downarrow) \Leftrightarrow \operatorname{Pvbl}((A\uparrow) \lor \Phi) $$

Moreover, because of the specific form of the formula $(A \downarrow)$, $\mathrm{ZFC}$ is able to prove $$ (A \downarrow) \to \operatorname{Pvbl}(A\downarrow) $$

Working in ZFC, assume $(A \downarrow)$. Then we know $\operatorname{Pvbl}(A \downarrow)$ and $\operatorname{Pvbl}((A \uparrow) \lor \Phi)$. ZFC is able to prove enough about the $\operatorname{Pvbl}$ predicate to ensure that $$\operatorname{Pvbl}(\psi) \land \operatorname{Pvbl}(\lnot \psi \lor \theta) \rightarrow \operatorname{Pvbl}(\theta) $$ for all $\psi$ and $\theta$. So we can obtain $\operatorname{Pvbl}(\Phi)$.

Now: what we have obtained is: "A does not halt or $\operatorname{Pvbl}(\Phi)$". In the fourth paragraph of the question, it instead claims we can obtain "A does not halt or $\Phi$". That is a stronger statement, and this is the first error I see in the proof. In the fourth paragraph, it is silently assumed that provability implies truth, but this is not correct for formalized provability.

$\mathrm{ZFC}$ does not prove $\operatorname{Pvbl}(\Phi) \to \Phi$ in general. In particular, $\mathrm{ZFC}$ does not prove $\operatorname{Pvbl}(0=1) \to (0=1)$ because there are models of $\mathrm{ZFC}$ in which both $\operatorname{Pvbl}(0=1)$ and $0 \not = 1$ are satisfied.

Addendum: Löb's theorem addresses this exact question. Applied to $\mathrm{ZFC}$, it states that if $\mathrm{ZFC}$ proves $\operatorname{Pvbl}(\Phi) \to \Phi$ then ZFC already proves $\Phi$. So, in particular, $\mathrm{ZFC}$ does not prove that $\operatorname{Pvbl}\mathrm{(\lnot Con(ZFC))}$ implies $\lnot \operatorname{Con}\mathrm{(ZFC)}$.

You've just proved that "either A does not halt or ZFC is inconsistent" must be true, not that this statement is provable in ZFC. There exist unprovable true statements in ZFC (if it is consistent). See Gödel's first incompleteness theorem.