Finite Lévy collapse to omega-one
ID: finite-levy-collapse-to-omega-one
With an uncountable regular cardinal, finite partial functions on assigning a value below the first coordinate collapse every ground ordinal below to countable size. The Delta-system lemma gives the chain in a partial order condition; the possible-values lemma for chain-condition forcing then preserves the regularity of . Therefore becomes the extension . Strong inaccessibility is enough but is not needed for this identification.
New to topics? Read the docs here!