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!