Closed forcing adds no short ground-valued sequences
ID: closed-forcing-adds-no-short-ground-valued-sequences
If a forcing is -closed in the ground model, then it adds no functions from a ground ordinal into a ground set . Recursively decide each value inside the ground model and take common stronger bounds at limit stages and after the final step. Conditions deciding a whole ground function are dense below any condition asserting this type of function. The dense-below generic meeting lemma ensures the generic filter meets that dense subset of a forcing order. One arbitrary bound need not be in the filter in an ordered set.
New to topics? Read the docs here!