ZFC proves there is an inaccessible cardinal

Fix, externally, a purported finite ZFC derivation p of the sentence E asserting that an inaccessible exists. Only finitely many ZFC axiom instances occur as assumptions in p; call their conjunction A_p. Soundness F2 applied to this fixed finite derivation is a theorem of ZF saying that any nonempty set structure satisfying those instances satisfies E. No assertion about a truth predicate for V is involved.

Work now inside ZFC under E. Choose the least inaccessible kappa by ordinal minimization below one witness. F1 proves each of the finitely many instances in A_p relativized to V_kappa; combining these finite proofs and F3 makes its nonempty membership structure a model of A_p. Step 1.1 gives that V_kappa satisfies E. Thus some alpha in V_kappa is internally an inaccessible ordinal. Transitivity gives an actual ordinal alpha<kappa. Its internal cardinalhood is actual cardinalhood: any external bijection between alpha and a smaller ordinal has a graph of rank at most alpha plus finitely many successors, hence belongs to V_kappa, contradicting internal cardinalhood if it existed. F1's inaccessibility absoluteness now applies to this actual cardinal and makes alpha an actual inaccessible, contradicting leastness of kappa.

The preceding construction is a finite ZFC derivation of E implies contradiction, depending on the fixed finite proof p. Append it to p, which derives E, and infer a contradiction in ZFC. Therefore the existence of such p implies inconsistency of ZFC. Contraposition yields exactly the stated conditional nonprovability. This neither extracts a transitive model from Con(ZFC) nor invokes a uniform universe satisfaction relation.