 Everything above will work at any limit stage except the treatment of the existential quantifier. The existential quantifier argument will work if the ordinal stage at which the model is being constructed is a weakly compact cardinal. This is a moderately strong large cardinal property (for an uncountable cardinal): it implies, for example, the existence of proper classes of inaccessibles and of \(n\)-Mahlo cardinals for each \(n\).