# Theory Erdos_Milner

```theory Erdos_Milner
imports Partitions

begin

subsection ‹Erdős-Milner theorem›

text ‹P. Erdős and E. C. Milner, A Theorem in the Partition Calculus.
Canadian Math. Bull. 15:4 (1972), 501-505.
Corrigendum, Canadian Math. Bull. 17:2 (1974), 305.›

text ‹The paper defines strong types as satisfying the criteria below.
It remarks that ordinals satisfy those criteria. Here is a (too complicated) proof.›
proposition strong_ordertype_eq:
assumes D: "D ⊆ elts β" and "Ord β"
obtains L where "⋃(List.set L) = D" "⋀X. X ∈ List.set L ⟹ indecomposable (tp X)"
and "⋀M. ⟦M ⊆ D; ⋀X. X ∈ List.set L ⟹ tp (M ∩ X) ≥ tp X⟧ ⟹ tp M = tp D"
proof -
define φ where "φ ≡ inv_into D (ordermap D VWF)"
then have bij_φ: "bij_betw φ (elts (tp D)) D"
using D bij_betw_inv_into down ordermap_bij by blast
have φ_cancel_left: "⋀d. d ∈ D ⟹ φ (ordermap D VWF d) = d"
by (metis D φ_def bij_betw_inv_into_left down ordermap_bij total_on_VWF wf_VWF)
have φ_cancel_right: "⋀γ. γ ∈ elts (tp D) ⟹ ordermap D VWF (φ γ) = γ"
by (metis φ_def f_inv_into_f ordermap_surj subsetD)
have "small D" "D ⊆ ON"
using assms down elts_subset_ON [of β] by auto
then have φ_less_iff: "⋀γ δ. ⟦γ ∈ elts (tp D); δ ∈ elts (tp D)⟧ ⟹ φ γ < φ δ ⟷ γ < δ"
by (metis φ_def inv_ordermap_VWF_mono_iff inv_ordermap_mono_eq less_V_def)
obtain αs where "List.set αs ⊆ ON" and "ω_dec αs" and tpD_eq: "tp D = ω_sum αs"
using Ord_ordertype ω_nf_exists by blast                ― ‹Cantor normal form of the ordertype›
have ord [simp]: "Ord (αs ! k)" "Ord (ω_sum (take k αs))" if "k < length αs" for k
using that ‹list.set αs ⊆ ON›
by (auto simp: dual_order.trans set_take_subset elim: ON_imp_Ord)
define E where "E ≡ λk. lift (ω_sum (take k αs)) (ω↑(αs!k))"
define L where "L ≡ map (λk. φ ` (elts (E k))) [0..<length αs]"
have lengthL [simp]: "length L = length αs"
have in_elts_E_less: "elts (E k') ≪ elts (E k)" if "k'<k" "k < length αs" for k k'
― ‹The ordinals have been partitioned into disjoint intervals›
proof -
have ordω: "Ord (ω ↑ αs ! k')"
using that by auto
from that id_take_nth_drop [of k' "take k αs"]
obtain l where "take k αs = take k' αs @ (αs!k') # l"
then show ?thesis
using that unfolding E_def lift_def less_sets_def
by (auto dest!: OrdmemD [OF ordω] intro: less_le_trans)
qed
have elts_E: "elts (E k) ⊆ elts (ω_sum αs)"
if "k < length αs" for k
proof -
have "ω ↑ (αs!k) ≤ ω_sum (drop k αs)"
by (metis that Cons_nth_drop_Suc ω_sum_Cons add_le_cancel_left0)
then have "(+) (ω_sum (take k αs)) ` elts (ω ↑ (αs!k)) ⊆ elts (ω_sum (take k αs) + ω_sum (drop k αs))"
by blast
also have "… = elts (ω_sum αs)"
using ω_sum_take_drop by auto
finally show ?thesis
qed
have ω_sum_in_tpD: "ω_sum (take k αs) + γ ∈ elts (tp D)"
if "γ ∈ elts (ω ↑ αs!k)" "k < length αs" for γ k
using elts_E lift_def that tpD_eq by (auto simp: E_def)
have Ord_φ: "Ord (φ (ω_sum (take k αs) + γ))"
if "γ ∈ elts (ω ↑ αs!k)" "k < length αs" for γ k
using ω_sum_in_tpD ‹D ⊆ ON› bij_φ bij_betw_imp_surj_on that by fastforce
define π where "π ≡ λk. ((λy. odiff y (ω_sum (take k αs))) ∘ ordermap D VWF)"
― ‹mapping the segments of @{term D} into some power of @{term ω}›
have bij_π: "bij_betw (π k) (φ ` elts (E k)) (elts (ω ↑ (αs!k)))"
if "k < length αs" for k
using that by (auto simp: bij_betw_def π_def E_def inj_on_def lift_def image_comp ω_sum_in_tpD φ_cancel_right that)
have π_iff: "π k x < π k y ⟷ (x,y) ∈ VWF"
if "x ∈ φ ` elts (E k)" "y ∈ φ ` elts (E k)" "k < length αs" for k x y
using that
by (auto simp: π_def E_def lift_def ω_sum_in_tpD φ_cancel_right Ord_φ φ_less_iff)
have tp_E_eq [simp]: "tp (φ ` elts (E k)) = ω↑(αs!k)"
if k: "k < length αs" for k
by (metis Ord_ω Ord_oexp π_iff bij_π ord(1) ordertype_VWF_eq_iff replacement small_elts that)
have tp_L_eq [simp]: "tp (L!k) = ω↑(αs!k)" if "k < length αs" for k
have UL_eq_D: "⋃ (list.set L) = D"
proof (rule antisym)
show "⋃ (list.set L) ⊆ D"
by (force simp: L_def tpD_eq bij_betw_apply [OF bij_φ] dest: elts_E)
show "D ⊆ ⋃ (list.set L)"
proof
fix δ
assume "δ ∈ D"
then have "ordermap D VWF δ ∈ elts (ω_sum αs)"
by (metis ‹small D› ordermap_in_ordertype tpD_eq)
then show "δ ∈ ⋃ (list.set L)"
using ‹δ ∈ D› φ_cancel_left in_elts_ω_sum
by (fastforce simp: L_def E_def image_iff lift_def)
qed
qed
show thesis
proof
show "indecomposable (tp X)" if "X ∈ list.set L" for X
using that by (auto simp: L_def indecomposable_ω_power)
next
fix M
assume "M ⊆ D" and *: "⋀X. X ∈ list.set L ⟹ tp X ≤ tp (M ∩ X)"
show "tp M = tp D"
proof (rule antisym)
show "tp M ≤ tp D"
by (simp add: ‹M ⊆ D› ‹small D› ordertype_VWF_mono)
define σ where "σ ≡ λX. inv_into (M ∩ X) (ordermap (M ∩ X) VWF)"
― ‹The bijection from an @{term ω}-power into the appropriate segment of @{term M}›
have bij_σ: "bij_betw (σ X) (elts (tp (M ∩ X))) (M ∩ X)" for X
unfolding σ_def
by (meson ‹M ⊆ D› ‹small D› bij_betw_inv_into inf_le1 ordermap_bij smaller_than_small total_on_VWF wf_VWF)
have Ord_σ: "Ord (σ X α)" if "α ∈ elts (tp (M ∩ X))" for α X
using ‹D ⊆ ON› ‹M ⊆ D› bij_betw_apply [OF bij_σ] that by blast
have σ_cancel_right: "⋀γ X. γ ∈ elts (tp (M ∩ X)) ⟹ ordermap (M ∩ X) VWF (σ X γ) = γ"
by (metis σ_def f_inv_into_f ordermap_surj subsetD)
have smM: "small (M ∩ X)" for X
by (meson ‹M ⊆ D› ‹small D› inf_le1 subset_iff_less_eq_V)
have "∃k < length αs. γ ∈ elts (E k)" if γ: "γ ∈ elts (tp D)" for γ
proof -
obtain X where "X ∈ set L" and X: "φ γ ∈ X"
by (metis UL_eq_D γ Union_iff φ_def in_mono inv_into_into ordermap_surj)
then have "∃k < length αs. γ ∈ elts (E k) ∧ X = φ ` elts (E k)"
apply (clarsimp simp: L_def)
by (metis γ φ_cancel_right elts_E in_mono tpD_eq)
then show ?thesis
by blast
qed
then obtain K where K: "⋀γ. γ ∈ elts (tp D) ⟹ K γ < length αs ∧ γ ∈ elts (E (K γ))"
by metis  ― ‹The index from @{term "tp D"} to the appropriate segment number›
define ψ where "ψ ≡ λd. σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d)"
show "tp D ≤ tp M"
proof (rule ordertype_inc_le)
show "small D" "small M"
using ‹M ⊆ D› ‹small D› subset_iff_less_eq_V by auto
next
fix d' d
assume xy: "d' ∈ D" "d ∈ D" and "(d',d) ∈ VWF"
then have "d' < d"
using ON_imp_Ord ‹D ⊆ ON› by auto
let ?γ' = "ordermap D VWF d'"
let ?γ = "ordermap D VWF d"
have len': "K ?γ' < length αs" and elts': "?γ' ∈ elts (E (K ?γ'))"
and len: "K ?γ < length αs" and elts: "?γ ∈ elts (E (K ?γ))"
using K ‹d' ∈ D› ‹d ∈ D› by (auto simp: ‹small D› ordermap_in_ordertype)
have Ord_σL: "Ord (σ (L!k) (π k d))" if "d ∈ φ ` elts (E k)" "k < length αs" for k d
by (metis (mono_tags) "*" Ord_σ bij_π bij_betw_apply lengthL nth_mem that tp_L_eq vsubsetD)
have "?γ' < ?γ"
by (simp add: ‹(d', d) ∈ VWF› ‹small D› ordermap_mono_less xy)
then have "K ?γ' ≤ K ?γ"
using elts' elts in_elts_E_less by (meson leI len' less_asym less_sets_def)
then consider (less) "K ?γ' < K ?γ" | (equal) "K ?γ' = K ?γ"
by linarith
then have "σ (L ! K ?γ') (π (K ?γ') d') < σ (L ! K ?γ) (π (K ?γ) d)"
proof cases
case less
obtain †: "σ (L ! K ?γ') (π (K ?γ') d') ∈ M ∩ L ! K ?γ'" "σ (L ! K ?γ) (π (K ?γ) d) ∈ M ∩ L ! K ?γ"
using elts' elts len' len * [THEN vsubsetD]
by (metis lengthL φ_cancel_left bij_π bij_σ bij_betw_imp_surj_on imageI nth_mem tp_L_eq xy)
then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) ∈ elts (E (K ?γ'))" "ordermap D VWF (σ (L ! K ?γ) (π (K ?γ) d)) ∈ elts (E (K ?γ))"
using len' len elts_E tpD_eq
by (fastforce simp: L_def φ_cancel_right)+
then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) < ordermap D VWF (σ (L ! K ?γ) (π (K ?γ) d))"
using in_elts_E_less len less by (meson less_sets_def)
moreover have "σ (L ! K ?γ') (π (K ?γ') d') ∈ D" "σ (L ! K ?γ) (π (K ?γ) d) ∈ D"
using ‹M ⊆ D› † by auto
ultimately show ?thesis
by (metis ‹small D› φ_cancel_left φ_less_iff ordermap_in_ordertype)
next
case equal
have σ_less: "⋀X γ δ. ⟦γ < δ; γ ∈ elts (tp (M ∩ X)); δ ∈ elts (tp (M ∩ X))⟧
⟹ σ X γ < σ X δ"
by (metis ‹D ⊆ ON› ‹M ⊆ D› σ_def dual_order.trans inv_ordermap_VWF_strict_mono_iff le_infI1 smM)
have "π (K ?γ) d' < π (K ?γ) d"
by (metis equal ‹(d', d) ∈ VWF› φ_cancel_left π_iff elts elts' imageI len xy)
then show ?thesis
unfolding equal
by (metis * [THEN vsubsetD] lengthL φ_cancel_left σ_less bij_π
bij_betw_imp_surj_on elts elts' image_eqI len local.equal nth_mem tp_L_eq xy)
qed
moreover have "Ord (σ (L ! K ?γ') (π (K ?γ') d'))" "Ord (σ (L ! K ?γ) (π (K ?γ) d))"
using Ord_σL φ_cancel_left elts len elts' len' xy by fastforce+
ultimately show "(ψ d', ψ d) ∈ VWF"
next
show "ψ ` D ⊆ M"
proof (clarsimp simp: ψ_def)
fix d
assume "d ∈ D"
let ?γ = "ordermap D VWF d"
have len: "K ?γ < length αs" and elts: "?γ ∈ elts (E (K ?γ))"
using K ‹d ∈ D› by (auto simp: ‹small D› ordermap_in_ordertype)
have "π (K ?γ) d ∈ elts (tp (L! (K ?γ)))"
using bij_π [OF len] ‹d ∈ D›
by (metis φ_cancel_left bij_betw_apply elts imageI len tp_L_eq)
then show "σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d) ∈ M"
by (metis "*" lengthL Int_iff bij_σ bij_betw_apply len nth_mem vsubsetD)
qed
qed auto
qed
qed

text ‹The ``remark'' of Erdős and E. C. Milner, Canad. Math. Bull. Vol. 17 (2), 1974›

proposition indecomposable_imp_Ex_less_sets:
assumes indec: "indecomposable α" and "α ≥ ω"
and A: "tp A = α" "small A" "A ⊆ ON"
and "x ∈ A" and A1: "tp A1 = α" "A1 ⊆ A"
obtains A2 where "tp A2 = α" "A2 ⊆ A1" "{x} ≪ A2"
proof -
have "Ord α"
using indec indecomposable_imp_Ord by blast
have "Limit α"
by (meson ω_gt1 assms indec indecomposable_imp_Limit less_le_trans)
define φ where "φ ≡ inv_into A (ordermap A VWF)"
then have bij_φ: "bij_betw φ (elts α) A"
using A bij_betw_inv_into down ordermap_bij by blast
have bij_om: "bij_betw (ordermap A VWF) A (elts α)"
using A down ordermap_bij by blast
define γ where "γ ≡ ordermap A VWF x"
have γ: "γ ∈ elts α"
unfolding γ_def using A ‹x ∈ A› down by auto
then have "Ord γ"
using Ord_in_Ord ‹Ord α› by blast
define B where "B ≡ φ ` (elts (succ γ))"
have B: "{y ∈ A. ordermap A VWF y ≤ ordermap A VWF x} ⊆ B"
apply (clarsimp simp add: B_def γ_def image_iff φ_def)
by (metis Ord_linear Ord_ordermap OrdmemD bij_betw_inv_into_left bij_om leD)
show thesis
proof
have "small A1"
by (meson ‹small A› A1 smaller_than_small)
then have "tp (A1 - B) ≤ tp A1"
moreover have "tp (A1 - B) ≥ α"
proof -
have "¬ (α ≤ tp B)"
unfolding B_def
proof (subst ordertype_VWF_inc_eq)
show "elts (succ  γ) ⊆ ON"
by (auto simp: γ_def ordertype_VWF_inc_eq intro: Ord_in_Ord)
have sub: "elts (succ  γ) ⊆ elts α"
using Ord_trans γ ‹Ord α› by auto
then show "φ ` elts (succ  γ) ⊆ ON"
using ‹A ⊆ ON› bij_φ bij_betw_imp_surj_on by blast
have "succ γ ∈ elts α"
using γ Limit_def ‹Limit α› by blast
with A sub show "φ u < φ v"
if "u ∈ elts (succ  γ)" and "v ∈ elts (succ  γ)" and "u < v" for u v
by (metis φ_def inv_ordermap_VWF_strict_mono_iff subsetD that)
show "¬ α ≤ tp (elts (succ  γ))"
by (metis Limit_def Ord_succ γ ‹Limit α› ‹Ord γ› mem_not_refl ordertype_eq_Ord vsubsetD)
qed auto
then show ?thesis
using indecomposable_ordertype_ge [OF indec, of A1 B] ‹small A1› A1 by (auto simp: B_def)
qed
ultimately show "tp (A1 - B) = α"
using A1 by blast
have "{x} ≪ (A - B)"
using assms B
apply (clarsimp simp: less_sets_def φ_def subset_iff)
by (metis Ord_not_le VWF_iff_Ord_less less_V_def order_refl ordermap_mono_less trans_VWF wf_VWF)
with ‹A1 ⊆ A› show "{x} ≪ (A1 - B)" by auto
qed auto
qed

text ‹the main theorem, from which they derive the headline result›
theorem Erdos_Milner_aux:
assumes part: "partn_lst_VWF α [k, γ] 2"
and indec: "indecomposable α" and "k > 1" "Ord γ" and β: "β ∈ elts ω1"
shows "partn_lst_VWF (α*β) [ord_of_nat (2*k), min γ (ω*β)] 2"
proof (cases "α≤1 ∨ β=0")
case True
have "Ord α"
using indec indecomposable_def by blast
show ?thesis
proof (cases "β=0")
case True then show ?thesis
by (simp add: partn_lst_triv0 [where i=1])
next
case False
then consider (0) "α=0" | (1) "α=1"
by (metis Ord_0 OrdmemD True ‹Ord α› mem_0_Ord one_V_def order.antisym succ_le_iff)
then show ?thesis
proof cases
case 0
with part show ?thesis
by (force simp add: partn_lst_def nsets_empty_iff less_Suc_eq)
next
case 1
then obtain "Ord β"
by (meson ON_imp_Ord Ord_ω1 True β elts_subset_ON)
then obtain i where "i < Suc (Suc 0)" "[ord_of_nat k, γ] ! i ≤ α"
using partn_lst_VWF_nontriv [OF part] 1 by auto
then have "γ ≤ 1"
using ‹α=1› ‹k > 1› by (fastforce simp: less_Suc_eq)
then have "min γ (ω*β) ≤ 1"
by (metis Ord_1 Ord_ω Ord_linear_le Ord_mult ‹Ord β› min_def order_trans)
then show ?thesis
using False by (auto simp: True ‹Ord β› ‹β≠0› ‹α=1› intro!: partn_lst_triv1 [where i=1])
qed
qed
next
case False
then have "α ≥ ω"
by (meson Ord_1 Ord_not_less indec indecomposable_def indecomposable_imp_Limit omega_le_Limit)
have "0 ∈ elts β" "β ≠ 0"
using False Ord_ω1 Ord_in_Ord β mem_0_Ord by blast+
show ?thesis
unfolding partn_lst_def
proof clarsimp
fix f
assume "f ∈ [elts (α*β)]⇗2⇖ → {..<Suc (Suc 0)}"
then have f: "f ∈ [elts (α*β)]⇗2⇖ → {..<2::nat}"
obtain ord [iff]: "Ord α" "Ord β" "Ord (α*β)"
using Ord_ω1 Ord_in_Ord β indec indecomposable_imp_Ord Ord_mult by blast
have *: False
if i [rule_format]: "∀H. tp H = ord_of_nat (2*k) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {0}"
and ii [rule_format]: "∀H. tp H = γ ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}"
and iii [rule_format]: "∀H. tp H = (ω*β) ⟶ H ⊆ elts (α*β) ⟶ ¬ f ` [H]⇗2⇖ ⊆ {1}"
proof -
have Ak0: "∃X ∈ [A]⇗k⇖. f ` [X]⇗2⇖ ⊆ {0}" ―‹remark (8) about @{term"A ⊆ S"}›
if A_αβ: "A ⊆ elts (α*β)" and ot: "tp A ≥ α" for A
proof -
let ?g = "inv_into A (ordermap A VWF)"
have "small A"
using down that by auto
then have inj_g: "inj_on ?g (elts α)"
by (meson inj_on_inv_into less_eq_V_def ordermap_surj ot subset_trans)
have om_A_less: "⋀x y. ⟦x ∈ A; y ∈ A; x < y⟧ ⟹ ordermap A VWF x < ordermap A VWF y"
using ord
by (meson A_αβ Ord_in_Ord VWF_iff_Ord_less ‹small A› in_mono ordermap_mono_less trans_VWF wf_VWF)
have α_sub: "elts α ⊆ ordermap A VWF ` A"
by (metis ‹small A› elts_of_set less_eq_V_def ordertype_def ot replacement)
have g: "?g ∈ elts α → elts (α*β)"
by (meson A_αβ Pi_I' α_sub inv_into_into subset_eq)
then have fg: "f ∘ (λX. ?g ` X) ∈ [elts α]⇗2⇖ → {..<2}"
by (rule nsets_compose_image_funcset [OF f _ inj_g])
obtain i H where "i < 2" "H ⊆ elts α"
and ot_eq: "tp H = [k,γ]!i" "(f ∘ (λX. ?g ` X)) ` (nsets H 2) ⊆ {i}"
using ii partn_lst_E [OF part fg] by (auto simp: eval_nat_numeral)
then consider (0) "i=0" | (1) "i=1"
by linarith
then show ?thesis
proof cases
case 0
then have "f ` [inv_into A (ordermap A VWF) ` H]⇗2⇖ ⊆ {0}"
using ot_eq ‹H ⊆ elts α› α_sub by (auto simp: nsets_def [of _ k] inj_on_inv_into elim!: nset_image_obtains)
moreover have "finite H ∧ card H = k"
using 0 ot_eq ‹H ⊆ elts α› down by (simp add: finite_ordertype_eq_card)
then have "inv_into A (ordermap A VWF) ` H ∈ [A]⇗k⇖"
using ‹H ⊆ elts α› α_sub by (auto simp: nsets_def [of _ k] card_image inj_on_inv_into inv_into_into)
ultimately show ?thesis
by blast
next
case 1
have gH: "?g ` H ⊆ elts (α*β)"
by (metis A_αβ α_sub ‹H ⊆ elts α› image_subsetI inv_into_into subset_eq)
have g_less: "?g x < ?g y" if "x < y" "x ∈ elts α" "y ∈ elts α" for x y
using Pi_mem [OF g] ord that
by (meson A_αβ Ord_in_Ord Ord_not_le ‹small A› dual_order.trans elts_subset_ON inv_ordermap_VWF_mono_le ot vsubsetD)
have [simp]: "tp (?g ` H) = tp H"
by (meson ‹H ⊆ elts α› ord down dual_order.trans elts_subset_ON gH g_less ordertype_VWF_inc_eq subsetD)
show ?thesis
using ii [of "?g ` H"] subset_inj_on [OF inj_g ‹H ⊆ elts α›] ot_eq 1
by (auto simp: gH elim!: nset_image_obtains)
qed
qed
define K where "K ≡ λi x. {y ∈ elts (α*β). x ≠ y ∧ f{x,y} = i}"
have small_K: "small (K i x)" for i x
define KI where "KI ≡ λi X. (⋂x∈X. K i x)"
have KI_disj_self: "X ∩ KI i X = {}" for i X
by (auto simp: KI_def K_def)
define M where "M ≡ λD 𝔄 x. {ν::V. ν ∈ D ∧ tp (K 1 x ∩ 𝔄 ν) ≥ α}"
have M_sub_D: "M D 𝔄 x ⊆ D" for D 𝔄 x
by (auto simp: M_def)
have small_M [simp]: "small (M D 𝔄 x)" if "small D" for D 𝔄 x
have 9: "tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D} ≥ α" (is "ordertype ?AD _ ≥ α")
if inD: "indecomposable (tp D)" and D: "D ⊆ elts β" and A: "A ⊆ elts (α*β)" and tpA: "tp A = α"
and 𝔄: "𝔄 ∈ D → {X. X ⊆ elts (α*β) ∧ tp X = α}"  for D A 𝔄
―‹remark (9), assuming an indecomposable order type›
proof (rule ccontr)
define A' where "A' ≡ {x ∈ A. ¬ tp (M D 𝔄 x) ≥ tp D}"
have small [iff]: "small A" "small D"
using A D down by (auto simp: M_def)
have small_𝔄: "small (𝔄 δ)" if "δ ∈ D" for δ
using that 𝔄 by (auto simp: Pi_iff subset_iff_less_eq_V)
assume not_α_le: "¬ α ≤ tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D}"
moreover
obtain "small A" "small A'" "A' ⊆ A" and A'_sub: "A' ⊆ elts (α*β)"
using A'_def A down by auto
moreover have "A' = A - ?AD"
by (force simp: A'_def)
ultimately have A'_ge: "tp A' ≥ α"
by (metis (no_types, lifting) dual_order.refl indec indecomposable_ordertype_eq mem_Collect_eq subsetI tpA)
obtain X where "X ⊆ A'" "finite X" "card X = k" and fX0: "f ` [X]⇗2⇖ ⊆ {0}"
using Ak0 [OF A'_sub A'_ge] by (auto simp: nsets_def [of _ k])
then have ‡: "¬ tp (M D 𝔄 x) ≥ tp D" if "x ∈ X" for x
using that by (auto simp: A'_def)
obtain x where "x ∈ X"
using ‹card X = k› ‹k>1› by fastforce
have "¬ D ⊆ (⋃ x∈X. M D 𝔄 x)"
proof
assume not: "D ⊆ (⋃x∈X. M D 𝔄 x)"
have "∃X∈M D 𝔄 ` X. tp D ≤ tp X"
proof (rule indecomposable_ordertype_finite_ge [OF inD])
show "M D 𝔄 ` X ≠ {}"
using A'_def A'_ge not not_α_le by auto
show "small (⋃ (M D 𝔄 ` X))"
using ‹finite X› by (simp add: finite_imp_small)
qed (use ‹finite X› not in auto)
then show False
qed
then obtain ν where "ν ∈ D" and ν: "ν ∉ (⋃ x∈X. M D 𝔄 x)"
by blast
define 𝒜 where "𝒜 ≡ {KI 0 X ∩ 𝔄 ν, ⋃x∈X. K 1 x ∩ 𝔄 ν, X ∩ 𝔄 ν}"
have αβ: "X ⊆ elts (α*β)" "𝔄 ν ⊆ elts (α*β)"
using A'_sub ‹X ⊆ A'› 𝔄 ‹ν ∈ D› by auto
then have "KI 0 X ∪ (⋃x∈X. K 1 x) ∪ X = elts (α*β)"
using ‹x ∈ X› f by (force simp: K_def KI_def Pi_iff less_2_cases_iff)
with αβ have 𝔄ν_𝒜: "finite 𝒜" "𝔄 ν ⊆ ⋃𝒜"
by (auto simp: 𝒜_def)
then have "¬ tp (K 1 x ∩ 𝔄 ν) ≥ α" if "x ∈ X" for x
using that ‹ν ∈ D› ν ‹k > 1› ‹card X = k› by (fastforce simp: M_def)
moreover have sm_K1: "small (⋃x∈X. K 1 x ∩ 𝔄 ν)"
by (meson Finite_V Int_lower2 ‹ν ∈ D› ‹finite X› small_𝔄 small_UN smaller_than_small)
ultimately have not1: "¬ tp (⋃x∈X. K 1 x ∩ 𝔄 ν) ≥ α"
using ‹finite X› ‹x ∈ X› indecomposable_ordertype_finite_ge [OF indec, of "(λx. K 1 x ∩ 𝔄 ν) ` X"] by blast
moreover have "¬ tp (X ∩ 𝔄 ν) ≥ α"
using ‹finite X› ‹α ≥ ω›
by (meson finite_Int mem_not_refl ordertype_VWF_ω vsubsetD)
moreover have "α ≤ tp (𝔄 ν)"
using 𝔄 ‹ν ∈ D› small_𝔄 by fastforce+
moreover have "small (⋃ 𝒜)"
using ‹ν ∈ D› small_𝔄 by (fastforce simp: 𝒜_def intro: smaller_than_small sm_K1)
ultimately have K0𝔄_ge: "tp (KI 0 X ∩ 𝔄 ν) ≥ α"
using indecomposable_ordertype_finite_ge [OF indec 𝔄ν_𝒜] by (auto simp: 𝒜_def)
have 𝔄ν: "𝔄 ν ⊆ elts (α*β)" "tp (𝔄 ν) = α"
using ‹ν ∈ D› 𝔄 by blast+
then obtain Y where Ysub: "Y ⊆ KI 0 X ∩ 𝔄 ν" and "finite Y" "card Y = k" and fY0: "f ` [Y]⇗2⇖ ⊆ {0}"
using Ak0 [OF _ K0𝔄_ge] by (auto simp: nsets_def [of _ k])
have †: "X ∩ Y = {}"
using Ysub KI_disj_self by blast
then have "card (X ∪ Y) = 2*k"
by (simp add: ‹card X = k› ‹card Y = k› ‹finite X› ‹finite Y› card_Un_disjoint)
moreover have "X ∪ Y ⊆ elts (α*β)"
using A'_sub ‹X ⊆ A'› 𝔄ν(1) ‹Y ⊆ KI 0 X ∩ 𝔄 ν› by auto
moreover have "f ` [X ∪ Y]⇗2⇖ ⊆ {0}"
using fX0 fY0 Ysub by (auto simp: † nsets_disjoint_2 image_Un image_UN KI_def K_def)
ultimately show False
using i ‹finite X› ‹finite Y› ordertype_VWF_finite_nat by auto
qed
have IX: "tp {x ∈ A. tp (M D 𝔄 x) ≥ tp D} ≥ α"
if D: "D ⊆ elts β" and A: "A ⊆ elts (α*β)" and tpA: "tp A = α"
and 𝔄: "𝔄 ∈ D → {X. X ⊆ elts (α*β) ∧ tp X = α}" for D A 𝔄
―‹remark (9) for any order type›
proof -
obtain L where UL: "⋃(List.set L) ⊆ D"
and indL: "⋀X. X ∈ List.set L ⟹ indecomposable (tp X)"
and eqL: "⋀M. ⟦M ⊆ D; ⋀X. X ∈ List.set L ⟹ tp (M ∩ X) ≥ tp X⟧ ⟹ tp M = tp D"
using ord by (metis strong_ordertype_eq D order_refl)
obtain A'' where A'': "A'' ⊆ A" "tp A'' ≥ α"
and "⋀x X. ⟦x ∈ A''; X ∈ List.set L⟧ ⟹ tp (M D 𝔄 x ∩ X) ≥ tp X"
using UL indL
proof (induction L arbitrary: thesis)
case (Cons X L)
then obtain A'' where A'': "A'' ⊆ A" "tp A'' ≥ α" and "X ⊆ D"
and ge_X: "⋀x X. ⟦x ∈ A''; X ∈ List.set L⟧ ⟹ tp (M D 𝔄 x ∩ X) ≥ tp X" by auto
then have tp_A'': "tp A'' = α"
by (metis A antisym down ordertype_VWF_mono tpA)
have ge_α: "tp {x ∈ A''. tp (M X 𝔄 x) ≥ tp X} ≥ α"
by (rule 9) (use A A'' tp_A'' Cons.prems ‹D ⊆ elts β› ‹X ⊆ D› 𝔄 in auto)
let ?A = "{x ∈ A''. tp (M D 𝔄 x ∩ X) ≥ tp X}"
have M_eq: "M D 𝔄 x ∩ X = M X 𝔄 x" if "x ∈ A''" for x
using that ‹X ⊆ D› by (auto simp: M_def)
show thesis
proof (rule Cons.prems)
show "α ≤ tp ?A"
using ge_α by (simp add: M_eq cong: conj_cong)
show "tp Y ≤ tp (M D 𝔄 x ∩ Y)" if "x ∈ ?A" "Y ∈ list.set (X # L)" for x Y
using that ge_X by force
qed (use A'' in auto)
qed (use tpA in auto)
then have tp_M_ge: "tp (M D 𝔄 x) ≥ tp D" if "x ∈ A''" for x
using eqL that by (auto simp: M_def)
have "α ≤ tp A''"
also have "… ≤ tp {x ∈ A''. tp (M D 𝔄 x) ≥ tp D}"
by (metis (mono_tags, lifting) tp_M_ge eq_iff mem_Collect_eq subsetI)
also have "… ≤ tp {x ∈ A. tp D ≤ tp (M D 𝔄 x)}"
by (rule ordertype_mono) (use A'' A down in auto)
finally show ?thesis .
qed
have IX': "tp {x ∈ A'. tp (K 1 x ∩ A) ≥ α} ≥ α"
if A: "A ⊆ elts (α*β)" "tp A = α" and A': "A' ⊆ elts (α*β)" "tp A' = α" for A A'
proof -
have ‡: "α ≤ tp (K 1 t ∩ A)" if "1 ≤ tp {ν. ν = 0 ∧ α ≤ tp (K 1 t ∩ A)}" for t
using that
by (metis Collect_empty_eq less_eq_V_0_iff ordertype_empty zero_neq_one)
have "tp {x ∈ A'. 1 ≤ tp {ν. ν = 0 ∧ α ≤ tp (K 1 x ∩ A)}}
≤ tp {x ∈ A'. α ≤ tp (K 1 x ∩ A)}"
by (rule ordertype_mono) (use "‡" A' in ‹auto simp: down›)
then show ?thesis
using IX [of "{0}" A' "λx. A"] that ‹0 ∈ elts β› by (force simp: M_def)
qed

have 10: "∃x0 ∈ A. ∃g ∈ elts β → elts β. strict_mono_on (elts β) g ∧ (∀ν ∈ F. g ν = ν)
∧ (∀ν ∈ elts β. tp (K 1 x0 ∩ 𝔄 (g ν)) ≥ α)"
if F: "finite F" "F ⊆ elts β"
and A: "A ⊆ elts (α*β)" "tp A = α"
and 𝔄: "𝔄 ∈ elts β → {X. X ⊆ elts (α*β) ∧ tp X = α}"
for F A 𝔄
proof -
define p where "p ≡ card F"
have "β ∉ F"
using that by auto
then obtain ι :: "nat ⇒ V" where bijι: "bij_betw ι {..p} (insert β F)" and monι: "strict_mono_on {..p} ι"
using ZFC_Cardinals.ex_bij_betw_strict_mono_card [of "insert β F"] elts_subset_ON ‹Ord β› F
by (simp add: p_def lessThan_Suc_atMost) blast
have less_ι_I: "ι k < ι l" if "k < l" "l ≤ p" for k l
using monι that by (auto simp: strict_mono_on_def)
then have less_ι_D: "k < l" if "ι k < ι l" "k ≤ p" for k l
by (metis less_asym linorder_neqE_nat that)
have Ord_ι: "Ord (ι k)" if "k ≤ p" for k
by (metis (no_types, lifting) ON_imp_Ord atMost_iff insert_subset mem_Collect_eq order_trans  ‹F ⊆ elts β› bijι bij_betwE elts_subset_ON ‹Ord β› that)
have le_ι0 [simp]: "⋀j. j ≤ p ⟹ ι 0 ≤ ι j"
by (metis eq_refl leI le_0_eq less_ι_I less_imp_le)
have le_ι: "ι i ≤ ι (j - Suc 0)" if "i < j" "j ≤ p" for i j
proof (cases i)
case 0 then show ?thesis
using le_ι0 that by auto
next
case (Suc i') then show ?thesis
by (metis (no_types, opaque_lifting) Suc_pred le_less less_Suc_eq less_Suc_eq_0_disj less_ι_I not_less_eq that)
qed

have [simp]: "ι p = β"
proof -
obtain k where k: "ι k = β" "k ≤ p"
by (meson atMost_iff bijι bij_betw_iff_bijections insertI1)
then have "k = p ∨ k < p"
by linarith
then show ?thesis
using bijι ord k that(2)
by (metis OrdmemD atMost_iff bij_betw_iff_bijections insert_iff leD less_ι_D order_refl subsetD)
qed

have F_imp_Ex: "∃k < p. ξ = ι k" if "ξ ∈ F" for ξ
proof -
obtain k where k: "k ≤ p" "ξ = ι k"
by (metis ‹ξ ∈ F› atMost_iff bijι bij_betw_def imageE insert_iff)
then show ?thesis
using ‹β ∉ F› ‹ι p = β› le_imp_less_or_eq that by blast
qed
have F_imp_ge: "ξ ≥ ι 0" if "ξ ∈ F" for ξ
using F_imp_Ex [OF that] by (metis dual_order.order_iff_strict le0 less_ι_I)
define D where "D ≡ λk. (if k=0 then {..<ι 0} else {ι (k-1)<..<ι k}) ∩ elts β"
have Dβ: "D k ⊆ elts β" for k
by (auto simp: D_def)
then have small_D [simp]: "small (D k)" for k
by (meson down)
have M_Int_D: "M (elts β) 𝔄 x ∩ D k = M (D k) 𝔄 x" if "k ≤ p" for x k
using Dβ by (auto simp: M_def)
have ι_le_if_D: "ι k ≤ μ" if "μ ∈ D (Suc k)" for μ k
using that by (simp add: D_def order.order_iff_strict)
have mono_D: "D i ≪ D j" if "i < j" "j ≤ p" for i j
proof (cases j)
case (Suc j')
with that show ?thesis
apply (simp add: less_sets_def D_def Ball_def)
by (metis One_nat_def diff_Suc_1 le_ι less_le_trans less_trans)
qed (use that in auto)
then have disjnt_DD: "disjnt (D i) (D j)" if "i ≠ j" "i ≤ p" "j ≤ p" for i j
by (meson disjnt_sym less_linear less_sets_imp_disjnt that)
have UN_D_eq: "(⋃l ≤ k. D l) = {..<ι k} ∩ (elts β - F)" if "k ≤ p" for k
using that
proof (induction k)
case 0
then show ?case
by (auto simp: D_def F_imp_ge leD)
next
case (Suc k)
have "D (Suc k) ∪ {..<ι k} ∩ (elts β - F) = {..<ι (Suc k)} ∩ (elts β - F)"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
using Suc.prems
by (auto simp: D_def if_split_mem2 intro: less_ι_I less_trans dest!: less_ι_D F_imp_Ex)
have "⋀x. ⟦x < ι (Suc k); x ∈ elts β; x ∉ F; ι k ≤ x⟧ ⟹ ι k < x"
using Suc.prems ‹F ⊆ elts β› bijι le_imp_less_or_eq
by (fastforce simp: bij_betw_iff_bijections)
then show "?rhs ⊆ ?lhs"
using Suc.prems by (auto simp: D_def Ord_not_less Ord_in_Ord [OF ‹Ord β›] Ord_ι if_split_mem2)
qed
then
show ?case
using Suc by (simp add: atMost_Suc)
qed
have β_decomp: "elts β = F ∪ (⋃k ≤ p. D k)"
using ‹F ⊆ elts β› OrdmemD [OF ‹Ord β›] by (auto simp: UN_D_eq)
define βidx where "βidx ≡ λν. @k. ν ∈ D k ∧ k ≤ p"
have βidx: "ν ∈ D (βidx ν) ∧ βidx ν ≤ p" if "ν ∈ elts β - F" for ν
using that by (force simp: βidx_def β_decomp intro: someI_ex del: conjI)
have any_imp_βidx: "k = βidx ν" if "ν ∈ D k" "k ≤ p" for k ν
proof (rule ccontr)
assume non: "k ≠ βidx ν"
have "ν ∉ F"
using that UN_D_eq by auto
then show False
using disjnt_DD [OF non] by (metis Dβ Diff_iff βidx disjnt_iff subsetD that)
qed
have "∃A'. A' ⊆ A ∧ tp A' = α ∧ (∀x ∈ A'. F ⊆ M (elts β) 𝔄 x)"
using F
proof induction
case (insert ν F)
then obtain A' where "A' ⊆ A" and A': "A' ⊆ elts (α*β)" "tp A' = α" and FN: "⋀x. x ∈ A' ⟹ F ⊆ M (elts β) 𝔄 x"
using A(1) by auto
define A'' where "A'' ≡ {x ∈ A'. α ≤ tp (K 1 x ∩ 𝔄 ν)}"
have "ν ∈ elts β" "F ⊆ elts β"
using insert by auto
note ordertype_eq_Ord [OF ‹Ord β›, simp]
show ?case
proof (intro exI conjI)
show "A'' ⊆ A"
using ‹A' ⊆ A› by (auto simp: A''_def)
show "tp A'' = α"
proof (rule antisym)
show "tp A'' ≤ α"
using ‹A'' ⊆ A› down ordertype_VWF_mono A by blast
have "𝔄 ν ⊆ elts (α*β)" "tp (𝔄 ν) = α"
using 𝔄 ‹ν ∈ elts β› by auto
then show "α ≤ tp A''"
using IX' [OF _ _ A'] by (simp add: A''_def)
qed
show "∀x∈A''. insert ν F ⊆ M (elts β) 𝔄 x"
using A''_def FN M_def ‹ν ∈ elts β› by blast
qed
qed (use A in auto)
then obtain A' where A': "A' ⊆ A" "tp A' = α" and FN: "⋀x. x ∈ A' ⟹ F ⊆ M (elts β) 𝔄 x"
by metis
have False
if *: "⋀x0 g. ⟦x0 ∈ A; g ∈ elts β → elts β; strict_mono_on (elts β) g⟧
⟹ (∃ν∈F. g ν ≠ ν) ∨ (∃ν∈elts β. tp (K 1 x0 ∩ 𝔄 (g ν)) < α)"
proof -
{ fix x       ― ‹construction of the monotone map @{term g} mentioned above›
assume "x ∈ A'"
with A' have "x ∈ A" by blast
have "∃k. k ≤ p ∧ tp (M (D k) 𝔄 x) < tp (D k)" (is "?P")
proof (rule ccontr)
assume "¬ ?P"
then have le: "tp (D k) ≤ tp (M (D k) 𝔄 x)" if "k ≤ p" for k
by (meson Ord_linear2 Ord_ordertype that)
have "∃f∈D k → M (D k) 𝔄 x. inj_on f (D k) ∧ (strict_mono_on (D k) f)"
if "k ≤ p" for k
using le [OF that] that VWF_iff_Ord_less
apply (clarsimp simp: ordertype_le_ordertype strict_mono_on_def)
by (metis (full_types) Dβ M_sub_D Ord_in_Ord PiE VWF_iff_Ord_less ord(2) subsetD)
then obtain h where fun_h: "⋀k. k ≤ p ⟹ h k ∈ D k → M (D k) 𝔄 x"
and inj_h: "⋀k. k ≤ p ⟹ inj_on (h k) (D k)"
and mono_h: "⋀k x y. k ≤ p ⟹ strict_mono_on (D k) (h k)"
by metis
then have fun_hD: "⋀k. k ≤ p ⟹ h k ∈ D k → D k"
by (auto simp: M_def)
have h_increasing: "ν ≤ h k ν"
if "k ≤ p" "ν ∈ D k" for k ν
by (meson Dβ Ord_mono_imp_increasing ord dual_order.trans elts_subset_ON fun_hD mono_h that)
define g where "g ≡ λν. if ν ∈ F then ν else h (βidx ν) ν"
have [simp]: "g ν = ν" if "ν ∈ F" for ν
using that by (auto simp: g_def)
have fun_g: "g ∈ elts β → elts β"
proof (rule Pi_I)
fix x assume "x ∈ elts β"
then have "x ∈ D (βidx x)" "βidx x ≤ p" if "x ∉ F"
using that by (auto simp: βidx)
then show "g x ∈ elts β"
by (metis fun_h Dβ M_sub_D ‹x ∈ elts β› PiE g_def subsetD)
qed
have h_in_D: "h (βidx ν) ν ∈ D (βidx ν)" if "ν ∉ F" "ν ∈ elts β" for ν
using βidx fun_hD that by fastforce
have 1: "ι k < h (βidx ν) ν"
if "k < p" and ν: "ν ∉ F" "ν ∈ elts β" and "ι k < ν" for k ν
by (meson that h_in_D [OF ν] βidx DiffI h_increasing order_less_le_trans)
moreover have 2: "h (βidx μ) μ < ι k"
if μ: "μ ∉ F" "μ ∈ elts β" and "k < p" "μ < ι k" for μ k
proof -
have "βidx μ ≤ k"
proof (rule ccontr)
assume "¬ βidx μ ≤ k"
then have "k < βidx μ"
by linarith
then show False
using ι_le_if_D βidx that by (metis Diff_iff Suc_pred le0 leD le_ι le_less_trans)
qed
then show ?thesis
using that h_in_D [OF μ]
by (smt (verit, best) Int_lower1 UN_D_eq UN_I atMost_iff lessThan_iff less_imp_le subset_eq)
qed
moreover have "h (βidx μ) μ < h (βidx ν) ν"
if μ: "μ ∉ F" "μ ∈ elts β" and ν: "ν ∉ F" "ν ∈ elts β" and "μ < ν" for μ ν
proof -
have le: "βidx μ ≤ βidx ν" if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)"
by (metis 2 DiffI βidx μ ν ‹μ < ν› order.strict_trans h_increasing leI le_ι order_less_asym order_less_le_trans that)
have "h 0 μ < h 0 ν" if "βidx μ = 0" "βidx ν = 0"
using that mono_h unfolding strict_mono_on_def
by (metis Diff_iff βidx μ ν ‹μ < ν›)
moreover have "h 0 μ < h (βidx ν) ν"
if "0 < βidx ν" "h 0 μ < ι 0" and "ι (βidx ν - Suc 0) < h (βidx ν) ν"
by (meson DiffI βidx ν le_ι le_less_trans less_le_not_le that)
moreover have "βidx ν ≠ 0"
if "0 < βidx μ" "h 0 ν < ι 0" "ι (βidx μ - Suc 0) < h (βidx μ) μ"
using le le_0_eq that by fastforce
moreover have "h (βidx μ) μ < h (βidx ν) ν"
if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)"
"h (βidx μ) μ < ι (βidx μ)" "ι (βidx ν - Suc 0) < h (βidx ν) ν"
using mono_h unfolding strict_mono_on_def
by (metis le Diff_iff βidx μ ν ‹μ < ν› le_ι le_less le_less_trans that)
ultimately show  ?thesis
using h_in_D [OF μ] h_in_D [OF ν] by (simp add: D_def split: if_split_asm)
qed
ultimately have sm_g: "strict_mono_on (elts β) g"
by (auto simp: g_def strict_mono_on_def dest!: F_imp_Ex)
have False if "ν ∈ elts β" and ν: "tp (K 1 x ∩ 𝔄 (g ν)) < α" for ν
proof -
have "F ⊆ M (elts β) 𝔄 x"
by (meson FN ‹x ∈ A'›)
then have False if "tp (K (Suc 0) x ∩ 𝔄 ν) < α" "ν ∈ F"
using that by (auto simp: M_def)
moreover have False if "tp (K (Suc 0) x ∩ 𝔄 (g ν)) < α" "ν ∈ D k" "k ≤ p" "ν ∉ F" for k
proof -
have "h (βidx ν) ν ∈ M (D (βidx ν)) 𝔄 x"
using fun_h βidx ‹ν ∈ elts β› ‹ν ∉ F› by auto
then show False
using that by (simp add: M_def g_def leD)
qed
ultimately show False
using ‹ν ∈ elts β› ν by (force simp: β_decomp)
qed
then show False
using * [OF ‹x ∈ A› fun_g sm_g] by auto
qed
then have "∃l. l ≤ p ∧ tp (M (elts β) 𝔄 x ∩ D l) < tp (D l)"
using M_Int_D by auto
}
then obtain l where lp: "⋀x. x ∈ A'⟹ l x ≤ p"
and lless: "⋀x. x ∈ A'⟹ tp (M (elts β) 𝔄 x ∩ D (l x)) < tp (D (l x))"
by metis
obtain A'' L where "A'' ⊆ A'" and A'': "A'' ⊆ elts (α*β)" "tp A'' = α" and lL: "⋀x. x ∈ A'' ⟹ l x = L"
proof -
have eq: "A' = (⋃i≤p. {x ∈ A'. l x = i})"
using lp by auto
have "∃X∈(λi. {x ∈ A'. l x = i}) ` {..p}. α ≤ tp X"
proof (rule indecomposable_ordertype_finite_ge [OF indec])
show "small (⋃i≤p. {x ∈ A'. l x = i})"
by (metis A'(1) A(1) eq down smaller_than_small)
qed (use A' eq in auto)
then show thesis
proof
fix A''
assume A'': "A'' ∈ (λi. {x ∈ A'. l x = i}) ` {..p}" and "α ≤ tp A''"
then obtain L where L: "⋀x. x ∈ A'' ⟹ l x = L"
by auto
have "A'' ⊆ A'"
using A'' by force
then have "tp A'' ≤ tp A'"
by (meson A' A down order_trans ordertype_VWF_mono)
with ‹α ≤ tp A''› have "tp A'' = α"
using A'(2) by auto
moreover have "A'' ⊆ elts (α*β)"
using A' A ‹A'' ⊆ A'› by auto
ultimately show thesis
using L that [OF ‹A'' ⊆ A'›] by blast
qed
qed
have 𝔄D: "𝔄 ∈ D L → {X. X ⊆ elts (α*β) ∧ tp X = α}"
using 𝔄 Dβ by blast
have α: "α ≤ tp {x ∈ A''. tp (D L) ≤ tp (M (D L) 𝔄 x)}"
using IX [OF Dβ A'' 𝔄D] by simp
have "M (elts β) 𝔄 x ∩ D L = M (D L) 𝔄 x" for x
using Dβ by (auto simp: M_def)
then have "tp (M (D L) 𝔄 x) < tp (D L)" if "x ∈ A''" for x
using lless that ‹A'' ⊆ A'› lL by force
then have [simp]: "{x ∈ A''. tp (D L) ≤ tp (M (D L) 𝔄 x)} = {}"
using leD by blast
show False
using α ‹α ≥ ω› by simp
qed
then show ?thesis
by (meson Ord_linear2 Ord_ordertype ‹Ord α›)
qed
let ?U = "UNIV :: nat set"
define μ where "μ ≡ fst ∘ from_nat_into (elts β × ?U)"
define q where "q ≡ to_nat_on (elts β × ?U)"
have co_βU: "countable (elts β × ?U)"
moreover have "elts β × ?U ≠ {}"
using ‹0 ∈ elts β› by blast
ultimately have "range (from_nat_into (elts β × ?U)) = (elts β × ?U)"
by (metis range_from_nat_into)
then have μ_in_β [simp]: "μ i ∈ elts β" for i
by (metis SigmaE μ_def comp_apply fst_conv range_eqI)

then have Ord_μ [simp]: "Ord (μ i)" for i
using Ord_in_Ord by blast

have inf_βU: "infinite (elts β × ?U)"
using ‹0 ∈ elts β› finite_cartesian_productD2 by auto

have 11 [simp]: "μ (q (ν,n)) = ν" if "ν ∈ elts β" for ν n
by (simp add: μ_def q_def that co_βU)
have range_μ [simp]: "range μ = elts β"
by (auto simp: image_iff) (metis 11)
have [simp]: "KI i {} = UNIV" "KI i (insert a X) = K i a ∩ KI i X" for i a X
by (auto simp: KI_def)
define Φ where "Φ ≡ λn::nat. λ𝔄 x. (∀ν ∈ elts β. 𝔄 ν ⊆ elts (α*β) ∧ tp (𝔄 ν) = α)
∧ x ` {..<n} ⊆ elts (α*β)
∧ (⋃ν ∈ elts β. 𝔄 ν) ⊆ KI 1 (x ` {..<n})
∧ strict_mono_sets (elts β) 𝔄"
define Ψ where "Ψ ≡ λn::nat. λg 𝔄 𝔄' xn. g ∈ elts β → elts β ∧ strict_mono_on (elts β) g
∧ (∀i≤n. g (μ i) = μ i)
∧ (∀ν ∈ elts β. 𝔄' ν ⊆ K 1 xn ∩ 𝔄 (g ν))
∧ {xn} ≪ (𝔄' (μ n)) ∧ xn ∈ 𝔄 (μ n)"
let ?𝔄0 = "λν. plus (α * ν) ` elts α"
have base: "Φ 0 ?𝔄0 x" for x
have step: "Ex (λ(g,𝔄',xn). Ψ n g 𝔄 𝔄' xn ∧ Φ (Suc n) 𝔄' (x(n:=xn)))" if "Φ n 𝔄 x" for n 𝔄 x
proof -
have 𝔄: "⋀ν. ν ∈ elts β ⟹ 𝔄 ν ⊆ elts (α*β) ∧ tp (𝔄 ν) = α"
and x: "x ` {..<n} ⊆ elts (α*β)"
and sub: "⋃ (𝔄 ` elts β) ⊆ KI (Suc 0) (x ` {..<n})"
and sm: "strict_mono_sets (elts β) 𝔄"
and μβ: "μ ` {..n} ⊆ elts β" and 𝔄sub: "𝔄 (μ n) ⊆ elts (α*β)"
and 𝔄fun: "𝔄 ∈ elts β → {X. X ⊆ elts (α*β) ∧ tp X = α}"
using that by (auto simp: Φ_def)
then obtain xn g where xn: "xn ∈ 𝔄 (μ n)" and g: "g ∈ elts β → elts β"
and sm_g: "strict_mono_on (elts β) g" and g_μ: "∀ν ∈ μ`{..n}. g ν = ν"
and g_α: "∀ν ∈ elts β. α ≤ tp (K 1 xn ∩ 𝔄 (g ν))"
using 10 [OF _ μβ 𝔄sub _ 𝔄fun] by (auto simp: 𝔄)
have tp1: "tp (K 1 xn ∩ 𝔄 (g ν)) = α" if "ν ∈ elts β" for ν
by (metis antisym Int_lower2 PiE 𝔄 down g g_α ordertype_VWF_mono that)
have tp2: "tp (𝔄 (μ n)) = α"
by (auto simp: 𝔄)
obtain "small (𝔄 (μ n))" "𝔄 (μ n) ⊆ ON"
by (meson 𝔄sub ord down elts_subset_ON subset_trans)
then obtain A2 where A2: "tp A2 = α" "A2 ⊆ K 1 xn ∩ 𝔄 (μ n)" "{xn} ≪ A2"
using indecomposable_imp_Ex_less_sets [OF indec ‹α ≥ ω› tp2]
by (metis μ_in_β atMost_iff image_eqI inf_le2 le_refl xn tp1 g_μ)
then have A2_sub: "A2 ⊆ 𝔄 (μ n)" by simp
let ?𝔄 = "λν. if ν = μ n then A2 else K 1 xn ∩ 𝔄 (g ν)"
have [simp]: "({..<Suc n} ∩ {x. x ≠ n}) = ({..<n})"
by auto
have "K (Suc 0) xn ∩ (⋃x∈elts β ∩ {ν. ν ≠ μ n}. 𝔄 (g x)) ⊆ KI (Suc 0) (x ` {..<n})"
using sub g by (auto simp: KI_def)
moreover have "A2 ⊆ KI (Suc 0) (x ` {..<n})" "A2 ⊆ elts (α*β)" "xn ∈ elts (α*β)"
using 𝔄sub sub A2 xn by fastforce+
moreover have "strict_mono_sets (elts β) ?𝔄"
using sm sm_g g g_μ A2_sub
unfolding strict_mono_sets_def strict_mono_on_def less_sets_def Pi_iff subset_iff Ball_def Bex_def image_iff
by (simp (no_asm_use) add: if_split_mem2) (smt order_refl)
ultimately have "Φ (Suc n) ?𝔄 (x(n := xn))"
using tp1 x A2 by (auto simp: Φ_def K_def)
with A2 show ?thesis
by (rule_tac x="(g,?𝔄,xn)" in exI) (simp add: Ψ_def g sm_g g_μ xn)
qed
define G where "G ≡ λn 𝔄 x. @(g,𝔄',x'). ∃xn. Ψ n g 𝔄 𝔄' xn ∧ x' = (x(n:=xn)) ∧ Φ (Suc n) 𝔄' x'"
have GΦ: "(λ(g,𝔄',x'). Φ (Suc n) 𝔄' x') (G n 𝔄 x)"
and GΨ: "(λ(g,𝔄',x'). Ψ n g 𝔄 𝔄' (x' n)) (G n 𝔄 x)"  if "Φ n 𝔄 x" for n 𝔄 x
using step [OF that] by (force simp: G_def dest: some_eq_imp)+
define H where "H ≡ rec_nat (id,?𝔄0,undefined) (λn (g0,𝔄,x0). G n 𝔄 x0)"
have "(λ(g,𝔄,x). Φ n 𝔄 x) (H n)" for n
unfolding H_def by (induction n) (use GΦ base in fastforce)+
then have H_imp_Φ: "Φ n 𝔄 x" if "H n = (g,𝔄,x)" for g 𝔄 x n
by (metis case_prodD that)
then have H_imp_Ψ: "(λ(g,𝔄',x'). let (g0,𝔄,x) = H n in Ψ n g 𝔄 𝔄' (x' n)) (H (Suc n))" for n
using GΨ by (fastforce simp: H_def split: prod.split)
define g where "g ≡ λn. (λ(g,𝔄,x). g) (H (Suc n))"
have g: "g n ∈ elts β → elts β" and sm_g: "strict_mono_on (elts β) (g n)"
and 13: "⋀i. i≤n ⟹ g n (μ i) = μ i" for n
using H_imp_Ψ [of n] by (auto simp: g_def Ψ_def)
define 𝔄 where "𝔄 ≡ λn. (λ(g,𝔄,x). 𝔄) (H n)"
define x where "x ≡ λn. (λ(g,𝔄,x). x n) (H (Suc n))"
have 14: "𝔄 (Suc n) ν ⊆ K 1 (x n) ∩ 𝔄 n (g n ν)" if "ν ∈ elts β" for ν n
using H_imp_Ψ [of n] that by (force simp: Ψ_def 𝔄_def x_def g_def)
then have x14: "𝔄 (Suc n) ν ⊆ 𝔄 n (g n ν)" if "ν ∈ elts β" for ν n
using that by blast
have 15: "x n ∈ 𝔄 n (μ n)" and 16: "{x n} ≪ (𝔄 (Suc n) (μ n))" for n
using H_imp_Ψ [of n] by (force simp: Ψ_def 𝔄_def x_def)+
have 𝔄_αβ: "𝔄 n ν ⊆ elts (α*β)" if "ν ∈ elts β" for ν n
using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split)
have 12: "strict_mono_sets (elts β) (𝔄 n)" for n
using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split)
let ?Z = "range x"
have S_dec: "⋃ (𝔄 (m+k) ` elts β) ⊆ ⋃ (𝔄 m ` elts β)" for k m
by (induction k) (use 14 g in ‹fastforce+›)
have "x n ∈ K 1 (x m)" if "m<n" for m n
proof -
have "x n ∈ (⋃ν ∈ elts β. 𝔄 n ν)"
by (meson "15" UN_I μ_in_β)
also have "… ⊆ (⋃ν ∈ elts β. 𝔄 (Suc m) ν)"
using S_dec [of "Suc m"] less_iff_Suc_add that by auto
also have "… ⊆ K 1 (x m)"
using 14 by auto
finally show ?thesis .
qed
then have "f{x m, x n} = 1" if "m<n" for m n
using that by (auto simp: K_def)
then have Z_K1: "f ` [?Z]⇗2⇖ ⊆ {1}"
by (clarsimp simp: nsets_2_eq) (metis insert_commute less_linear)
moreover have Z_sub: "?Z ⊆ elts (α*β)"
using "15" 𝔄_αβ μ_in_β by blast
moreover have "tp ?Z ≥ ω * β"
proof -
define 𝔤 where "𝔤 ≡ λi j x. wfrec (measure (λk. j-k)) (λ𝔤 k. if k<j then g k (𝔤 (Suc k)) else x) i"
have 𝔤: "𝔤 i j x = (if i<j then g i (𝔤 (Suc i) j x) else x)" for i j x
by (simp add: 𝔤_def wfrec cut_apply)
have 17: "𝔤 k j (μ i) = μ i" if "i ≤ k" for i j k
using wf_measure [of "λk. j-k"] that
by (induction k rule: wf_induct_rule) (simp add: "13" 𝔤 le_imp_less_Suc)
have 𝔤_in_β: "𝔤 i j ν  ∈ elts β" if "ν ∈ elts β" for i j ν
using wf_measure [of "λk. j-k"] that
proof (induction i rule: wf_induct_rule)
case (less i)
with g show ?case by (force simp: 𝔤 [of i])
qed
then have 𝔤_fun: "𝔤 i j ∈ elts β → elts β" for i j
by simp
have sm_𝔤: "strict_mono_on (elts β) (𝔤 i j)" for i j
using wf_measure [of "λk. j-k"]
proof (induction i rule: wf_induct_rule)
case (less i)
with sm_g show ?case
by (auto simp: 𝔤 [of i] strict_mono_on_def 𝔤_in_β)
qed
have *: "𝔄 j (μ j) ⊆ 𝔄 i (𝔤 i j (μ j))" if "i < j" for i j
using wf_measure [of "λk. j-k"] that
proof (induction i rule: wf_induct_rule)
case (less i)
then have "j - Suc i < j - i"
by (metis (no_types) Suc_diff_Suc lessI)
with less 𝔤_in_β show ?case
by (simp add: 𝔤 [of i]) (metis 17 Suc_lessI μ_in_β order_refl order_trans x14)
qed
have le_iff: "𝔤 i j (μ j) ≤ μ i ⟷ μ j ≤ μ i" for i j
using sm_𝔤 unfolding strict_mono_on_def
by (metis "17" Ord_in_Ord Ord_linear2 μ_in_β leD le_refl less_V_def ‹Ord β›)
then have less_iff: "𝔤 i j (μ j) < μ i ⟷ μ j < μ i" for i j
by (metis (no_types, lifting) "17" μ_in_β less_V_def order_refl sm_𝔤 strict_mono_on_def)
have eq_iff: "𝔤 i j (μ j) = μ i ⟷ μ j = μ i" for i j
by (metis eq_refl le_iff less_iff less_le)
have μ_if_ne: "μ m < μ n" if mn: "𝔄 m (μ m) ≪ 𝔄 n (μ n)" "m ≠ n" for m n
proof -
have xmn: "x m < x n"
using "15" less_setsD that(1) by blast
have Ord𝔤: "Ord (𝔤 n m (μ m))"
using Ord_in_Ord 𝔤_in_β μ_in_β ord(2) by presburger
have "¬ 𝔄 m (μ m) ≪ 𝔄 n (μ n)" if "μ n = μ m"
using  "*" "15" eq_iff that unfolding less_sets_def
by (metis in_mono less_irrefl not_less_iff_gr_or_eq)
moreover
have "𝔄 n (μ n) ⊆ 𝔄 m (𝔤 m n (μ n)) ∨ 𝔄 m (μ m) ⊆ 𝔄 n (𝔤 n m (μ m))"
using * mn
by (meson antisym_conv3)
then have False if "μ n < μ m"
using strict_mono_setsD [OF 12] 15 xmn 𝔤_in_β μ_in_β that
by (smt (verit, best) Ord𝔤 Ord_μ Ord_linear2 leD le_iff less_asym less_iff less_setsD subset_iff)
ultimately show "μ m < μ n"
by (meson that(1) Ord_μ Ord_linear_lt)
qed
have 18: "𝔄 m (μ m) ≪ 𝔄 n (μ n) ⟷ μ m < μ n" for m n
proof (cases n m rule: linorder_cases)
case less
show ?thesis
proof (intro iffI)
assume "μ m < μ n"
then have "𝔄 n (𝔤 n m (μ m)) ≪ 𝔄 n (μ n)"
by (metis "12" 𝔤_in_β μ_in_β eq_iff le_iff less_V_def strict_mono_sets_def)
then show "𝔄 m (μ m) ≪ 𝔄 n (μ n)"
by (meson "*" less less_sets_weaken1)
qed (use μ_if_ne less in blast)
next
case equal
with 15 show ?thesis by auto
next
case greater
show ?thesis
proof (intro iffI)
assume "μ m < μ n"
then have "𝔄 m (μ m) ≪ (𝔄 m (𝔤 m n (μ n)))"
by (meson 12 Ord_in_Ord Ord_linear2 𝔤_in_β μ_in_β le_iff leD ord(2) strict_mono_sets_def)
then show "𝔄 m (μ m) ≪ 𝔄 n (μ n)"
by (meson "*" greater less_sets_weaken2)
qed (use μ_if_ne greater in blast)
qed
have 𝔄_increasing_μ: "𝔄 n (μ n) ⊆ 𝔄 m (μ m)" if "m ≤ n" "μ m = μ n" for m n
by (metis "*" "17" dual_order.order_iff_strict that)
moreover have INF: "infinite {n. n ≥ m ∧ μ m = μ n}" for m
proof -
have "infinite (range (λn. q (μ m, n)))"
unfolding q_def
using to_nat_on_infinite [OF co_βU inf_βU] finite_image_iff
moreover have "(range (λn. q (μ m, n))) ⊆ {n. μ m = μ n}"
using 11 [of "μ m"] by auto
ultimately have "infinite {n. μ m = μ n}"
using finite_subset by auto
then have "infinite ({n. μ m = μ n} - {..<m})"
by simp
then show ?thesis
by (auto simp: finite_nat_set_iff_bounded Bex_def not_less)
qed
let ?eqv = "λm. {n. m ≤ n ∧ μ m = μ n}"
have sm_x: "strict_mono_on (?eqv m) x" for m
proof (clarsimp simp: strict_mono_on_def)
fix n p
assume "m ≤ n" "μ p = μ n" "μ m = μ n" "n < p"
with 16 [of n] show "x n < x p"
by (metis "*" "15" "17" Suc_lessI insert_absorb insert_subset le_SucI less_sets_singleton1)
qed
then have inj_x: "inj_on x (?eqv m)" for m
using strict_mono_on_imp_inj_on by blast
define ZA where "ZA ≡ λm. ?Z ∩ 𝔄 m (μ m)"
have small_ZA [simp]: "small (ZA m)" for m
by (metis ZA_def inf_le1 small_image_nat smaller_than_small)
have 19: "tp (ZA m) ≥ ω" for m
proof -
have "x ` {n. m ≤ n ∧ μ m = μ n} ⊆ ZA m"
unfolding ZA_def using "15" 𝔄_increasing_μ by blast
then have "infinite (ZA m)"
using INF [of m] finite_image_iff [OF inj_x] by (meson finite_subset)
then show ?thesis
qed
have "∃f ∈ elts ω → ZA m. strict_mono_on (elts ω) f" for m
proof -
obtain Z where "Z ⊆ ZA m" "tp Z = ω"
by (meson 19 Ord_ω le_ordertype_obtains_subset small_ZA)
moreover have "ZA m ⊆ ON"
using Ord_in_Ord 𝔄_αβ μ_in_β unfolding ZA_def by blast
ultimately show ?thesis
by (metis strict_mono_on_ordertype Pi_mono small_ZA smaller_than_small subset_iff)
qed
then obtain φ where φ: "⋀m. φ m ∈ elts ω → ZA m"
and sm_φ: "⋀m. strict_mono_on (elts ω) (φ m)"
by metis
have "Ex(λ(m,ν). ν ∈ elts β ∧ γ = ω * ν + ord_of_nat m)" if "γ ∈ elts (ω * β)" for γ
using that by (auto simp: mult [of ω β] lift_def elts_ω)
then obtain split where split: "⋀γ. γ ∈ ```