Solution (source code)

= Solution

Let $T$ be <ZFC> together with the assertion of unboundedly many <inaccessible cardinals>. Given a model of $T$, if it has no <inaccessible limit of inaccessibles>, it already witnesses the required nonimplication. Otherwise let $\iota$ be its least <inaccessible limit of inaccessibles> and pass to its rank segment $V_\iota$.

Because $\iota$ is an <inaccessible cardinal>, $V_\iota$ satisfies <ZFC>. Its <ordinals> are precisely those below $\iota$, and below $\iota$ the inaccessible cardinals are unbounded by the choice of $\iota$. Inaccessibility of any smaller ordinal is absolute to this segment: it has the same subsets and functions on all smaller ordinals, as in <strong-inaccessibility absoluteness from rank agreement>. Thus $V_\iota$ satisfies the unbounded-inaccessibles assertion.

No smaller ordinal can be an <inaccessible limit of inaccessibles>, by minimality of $\iota$ and the same absoluteness. Also $\iota$ is not an ordinal of $V_\iota$ itself. Consequently
$$
\boxed{V_\iota\models T+\neg\mathrm{ILI}}.
$$
This <rank cutoff at the first inaccessible limit of inaccessibles> proves $\operatorname{Con}(T)\Rightarrow\operatorname{Con}(T+\neg\mathrm{ILI})$. The <soundness theorem for first-order logic> then gives $T\not\vdash\mathrm{ILI}$ if $T$ is consistent. This is a model-theoretic relative-consistency argument, and does not infer external transitivity from mere consistency.