[proofplan] The proof separates the syntactic relative consistency claim from the well-founded-model claim. For consistency, we use the Completeness Theorem to pass from consistency to a model $M$ of $\mathrm{ZFC}$ with an internally strongly inaccessible cardinal $\kappa$, and then apply the inaccessible-rank theorem inside $M$ to see that $M$ contains a set-coded model of $\mathrm{ZFC}$. For the well-founded version, we first collapse the whole externally well-founded model to a transitive model, then take its rank segment below the collapsed inaccessible cardinal and apply the inaccessible-rank theorem externally. [/proofplan] [step:Formalize the assertion that a set-coded model of $\mathrm{ZFC}$ exists] Fix a recursive axiom predicate $\operatorname{Ax}_{\mathrm{ZFC}}(n)$ on natural-number codes of formulas in the language $\{\in\}$. The sentence “there is a model of $\mathrm{ZFC}$” is understood as the first-order set-theoretic assertion that there exist a set $A$ and a binary relation $E \subset A \times A$ such that, for every natural number $n$ coding a $\mathrm{ZFC}$ axiom, the set structure $(A,E)$ satisfies the formula coded by $n$ under the usual first-order satisfaction relation for set structures. Thus the target theory is the first-order theory \begin{align*} \mathrm{ZFC} + \exists A\,\exists E \subset A \times A\ \bigl((A,E)\models \mathrm{ZFC}\bigr). \end{align*} [guided] Because $\mathrm{ZFC}$ is an axiom scheme, the phrase “there is a model of $\mathrm{ZFC}$” must be formalized with a coding convention. We fix a recursive predicate $\operatorname{Ax}_{\mathrm{ZFC}}(n)$ which says that $n$ is the Gödel code of one of the axioms of $\mathrm{ZFC}$ in the language $\{\in\}$. A set-coded structure consists of a set $A$ and a binary relation $E \subset A \times A$. Since $A$ is a set, the satisfaction relation for formulas interpreted in $(A,E)$ is definable by recursion on formulas. Therefore the assertion $(A,E)\models \mathrm{ZFC}$ means: for every natural number $n$, if $\operatorname{Ax}_{\mathrm{ZFC}}(n)$ holds, then the structure $(A,E)$ satisfies the sentence coded by $n$. This is the precise first-order meaning of “there is a model of $\mathrm{ZFC}$” used below. [/guided] [/step] [step:Use completeness to obtain a model with an inaccessible cardinal] Assume that $\mathrm{ZFC} +$ “there exists a strongly inaccessible cardinal” is consistent. By the Completeness Theorem (citing a result not yet in the wiki: Completeness Theorem), there exists a set-coded first-order model $M = (|M|,E_M)$ such that \begin{align*} M \models \mathrm{ZFC} + \text{“there exists a strongly inaccessible cardinal.”} \end{align*} Choose an element $\kappa \in |M|$ such that $M \models \text{“$\kappa$ is a strongly inaccessible cardinal.”}$ [/step] [step:Apply the inaccessible rank segment theorem inside $M$] Inside $M$, let $V_\kappa^M$ denote the $M$-set produced by the internal cumulative-hierarchy recursion up to stage $\kappa$; equivalently, $M$ satisfies that the $M$-elements of $V_\kappa^M$ are exactly the objects of internal rank below $\kappa$. The inaccessible-rank theorem is a theorem provable in $\mathrm{ZFC}$: $\mathrm{ZFC}$ proves that whenever $\kappa$ is strongly inaccessible, the structure $(V_\kappa,\in\!\upharpoonright V_\kappa)$ satisfies $\mathrm{ZFC}$. Since $M$ satisfies $\mathrm{ZFC}$ and $M$ satisfies that $\kappa$ is strongly inaccessible, this ZFC-provable theorem applies internally in $M$. Hence \begin{align*} M \models \text{“$(V_\kappa^M,\in^M\!\upharpoonright V_\kappa^M)$ is a model of $\mathrm{ZFC}$.”} \end{align*} Here $\in^M\!\upharpoonright V_\kappa^M$ denotes the binary relation on $V_\kappa^M$ inherited from $E_M$. Thus $M \models \mathrm{ZFC} + \text{“there exists a model of $\mathrm{ZFC}$.”}$. Therefore $\mathrm{ZFC} +$ “there exists a model of $\mathrm{ZFC}$” has a model, and hence is consistent. [guided] We now use the large-cardinal hypothesis exactly once. In the model $M$, the element $\kappa$ is believed to be a strongly inaccessible cardinal. Therefore $M$ can form its internal cumulative hierarchy up to $\kappa$; denote that internal rank segment by $V_\kappa^M$. The theorem needed here is the inaccessible rank segment theorem, formalized as a ZFC-provable statement: $\mathrm{ZFC}$ proves that if $\kappa$ is strongly inaccessible, then $(V_\kappa,\in\!\upharpoonright V_\kappa)$ satisfies $\mathrm{ZFC}$ (citing a result not yet in the wiki: Inaccessible Rank Segment Models ZFC). Because $M\models \mathrm{ZFC}$, every ZFC theorem holds in $M$. The hypotheses are verified internally to $M$: first, $M\models \mathrm{ZFC}$; second, \begin{align*} M \models \text{“$\kappa$ is strongly inaccessible.”} \end{align*} Therefore, applying the theorem inside $M$ gives \begin{align*} M \models \text{“$(V_\kappa^M,\in^M\!\upharpoonright V_\kappa^M)$ satisfies $\mathrm{ZFC}$.”} \end{align*} This produces exactly the witness demanded by the sentence “there exists a model of $\mathrm{ZFC}$”: the set is $V_\kappa^M$, and the membership relation is the restriction of $M$'s membership relation to that set. Hence $M$ satisfies \begin{align*} \mathrm{ZFC} + \text{“there exists a model of $\mathrm{ZFC}$.”} \end{align*} Since a model of this theory exists, the theory is consistent. [/guided] [/step] [step:Collapse the well-founded model before taking the inaccessible rank segment] Assume now that $M = (|M|,E_M)$ is an externally well-founded set-coded model of $\mathrm{ZFC} +$ “there exists a strongly inaccessible cardinal.” Because $M$ satisfies extensionality and $E_M$ is externally well-founded, the relation $E_M$ is externally well-founded and extensional on $|M|$. By the Mostowski Collapse Theorem (citing a result not yet in the wiki: Mostowski Collapse Theorem), there are a transitive set $P$ and an isomorphism $\pi : (|M|,E_M) \to (P,\in)$. Since first-order satisfaction is preserved under isomorphism, $(P,\in)\models \mathrm{ZFC} + \text{“there exists a strongly inaccessible cardinal.”}$. Choose $\lambda \in P$ such that $(P,\in)$ satisfies that $\lambda$ is strongly inaccessible. Define $N$ to be the rank-initial segment computed in $P$ below $\lambda$: \begin{align*} N := V_\lambda^P. \end{align*} Since $P$ is transitive and satisfies $\mathrm{ZFC}$, and since $P$ satisfies that $\lambda$ is strongly inaccessible, the inaccessible-rank theorem applies externally to the transitive model $P$. Hence $N$ is a transitive set and $(N,\in)\models \mathrm{ZFC}$. Thus there exists a transitive model of $\mathrm{ZFC}$. [guided] We use the external well-foundedness hypothesis before extracting the rank segment. The structure $M=(|M|,E_M)$ is assumed to be externally well-founded, and $M\models\mathrm{ZFC}$ includes the axiom of extensionality. Thus if two elements of $|M|$ have exactly the same $E_M$-members, extensionality as interpreted in $M$ identifies them. Therefore $E_M$ is an externally well-founded and extensional relation on the set $|M|$. The Mostowski Collapse Theorem applies to any set equipped with a well-founded extensional relation. Applying it to $(|M|,E_M)$ gives a transitive set $P$ and an isomorphism \begin{align*} \pi : (|M|,E_M) \to (P,\in). \end{align*} First-order satisfaction is invariant under isomorphism of structures, so the collapsed transitive structure satisfies the same first-order theory: \begin{align*} (P,\in)\models \mathrm{ZFC} + \text{“there exists a strongly inaccessible cardinal.”} \end{align*} This move avoids any appeal to a compressed absoluteness statement about a possibly nonstandard internal satisfaction assertion; after the collapse, we are working with an actual transitive set and the real membership relation. Choose $\lambda\in P$ such that $(P,\in)$ satisfies that $\lambda$ is strongly inaccessible. Let $N$ be the rank segment computed by the transitive model $P$ below $\lambda$: \begin{align*} N := V_\lambda^P. \end{align*} The inaccessible-rank theorem says that in any model of $\mathrm{ZFC}$, a strongly inaccessible cardinal cuts off a rank segment satisfying $\mathrm{ZFC}$. Here the hypotheses hold for the transitive model $P$: it satisfies $\mathrm{ZFC}$, and it satisfies that $\lambda$ is strongly inaccessible. Therefore the theorem gives \begin{align*} (N,\in)\models \mathrm{ZFC}. \end{align*} Moreover $N$ is transitive because it is a rank-initial segment inside the transitive set $P$. Hence $N$ is a transitive model of $\mathrm{ZFC}$, as required. [/guided] [/step]