Relative condensation lemma

ID: relative-condensation-lemma

If is a nonzero limit ordinal and with , the Mostowski collapse theorem sends to for some nonzero limit and fixes pointwise. The base is fixed by transitivity and inclusion of all its members. Transfer the relative constructible level recognition formula first by elementarity and then through the collapse isomorphism to identify its image. If , ordinal heights are and , giving the bound. Having only does not guarantee this base-fixing version.

New to topics? Read the docs here!