Chain-poset nonembedding lemma

ID: chain-poset-nonembedding-lemma

If is the inclusion-ordered collection of every chain in a partial order, including the empty chain, it has no order-preserving injection into . Supposing exists, recursively set for . By induction the earlier values form a chain; its proper initial chains are distinct, so monotonicity and injectivity make strictly greater than every earlier value. This would inject the Hartogs ordinal into .

New to topics? Read the docs here!