diff --git a/thys/Ordinal_Partitions/Erdos_Milner.thy b/thys/Ordinal_Partitions/Erdos_Milner.thy
--- a/thys/Ordinal_Partitions/Erdos_Milner.thy
+++ b/thys/Ordinal_Partitions/Erdos_Milner.thy
@@ -1,1294 +1,1282 @@
 theory Erdos_Milner
   imports Partitions
 
 begin
 
 subsection \<open>Erdős-Milner theorem\<close>
 
 text \<open>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.\<close>
 
 text \<open>The paper defines strong types as satisfying the criteria below.
       It remarks that ordinals satisfy those criteria. Here is a (too complicated) proof.\<close>
 proposition strong_ordertype_eq:
   assumes D: "D \<subseteq> elts \<beta>" and "Ord \<beta>"
   obtains L where "\<Union>(List.set L) = D" "\<And>X. X \<in> List.set L \<Longrightarrow> indecomposable (tp X)"
     and "\<And>M. \<lbrakk>M \<subseteq> D; \<And>X. X \<in> List.set L \<Longrightarrow> tp (M \<inter> X) \<ge> tp X\<rbrakk> \<Longrightarrow> tp M = tp D"
 proof -
   define \<phi> where "\<phi> \<equiv> inv_into D (ordermap D VWF)"
   then have bij_\<phi>: "bij_betw \<phi> (elts (tp D)) D"
     using D bij_betw_inv_into down ordermap_bij by blast
   have \<phi>_cancel_left: "\<And>d. d \<in> D \<Longrightarrow> \<phi> (ordermap D VWF d) = d"
-    by (metis D \<phi>_def bij_betw_inv_into_left down_raw ordermap_bij small_iff_range total_on_VWF wf_VWF)
+    by (metis D \<phi>_def bij_betw_inv_into_left down ordermap_bij total_on_VWF wf_VWF)
   have \<phi>_cancel_right: "\<And>\<gamma>. \<gamma> \<in> elts (tp D) \<Longrightarrow> ordermap D VWF (\<phi> \<gamma>) = \<gamma>"
     by (metis \<phi>_def f_inv_into_f ordermap_surj subsetD)
   have "small D" "D \<subseteq> ON"
     using assms down elts_subset_ON [of \<beta>] by auto
   then have \<phi>_less_iff: "\<And>\<gamma> \<delta>. \<lbrakk>\<gamma> \<in> elts (tp D); \<delta> \<in> elts (tp D)\<rbrakk> \<Longrightarrow> \<phi> \<gamma> < \<phi> \<delta> \<longleftrightarrow> \<gamma> < \<delta>"
-    by (metis ON_imp_Ord Ord_linear2 \<phi>_def inv_into_ordermap inv_ordermap_VWF_mono_le leD less_V_def)
+    by (metis \<phi>_def inv_ordermap_VWF_mono_iff inv_ordermap_mono_eq less_V_def)
   obtain \<alpha>s where "List.set \<alpha>s \<subseteq> ON" and "\<omega>_dec \<alpha>s" and tpD_eq: "tp D = \<omega>_sum \<alpha>s"
     using Ord_ordertype \<omega>_nf_exists by blast                \<comment> \<open>Cantor normal form of the ordertype\<close>
   have ord [simp]: "Ord (\<alpha>s ! k)" "Ord (\<omega>_sum (take k \<alpha>s))" if "k < length \<alpha>s" for k
     using that \<open>list.set \<alpha>s \<subseteq> ON\<close>
     by (auto simp: dual_order.trans set_take_subset elim: ON_imp_Ord)
   define E where "E \<equiv> \<lambda>k. lift (\<omega>_sum (take k \<alpha>s)) (\<omega>\<up>(\<alpha>s!k))"
   define L where "L \<equiv> map (\<lambda>k. \<phi> ` (elts (E k))) [0..<length \<alpha>s]"
   have [simp]: "length L = length \<alpha>s"
     by (simp add: L_def)
-  have in_elts_E_less: "x' < x"
-    if "x' \<in> elts (E k')" "x \<in> elts (E k)" "k'<k" "k < length \<alpha>s" for k k' x' x
-                                      \<comment> \<open>The ordinals have been partitioned into disjoint intervals\<close>
+  have in_elts_E_less: "elts (E k') \<lless> elts (E k)" if "k'<k" "k < length \<alpha>s" for k k'
+    \<comment> \<open>The ordinals have been partitioned into disjoint intervals\<close>
   proof -
     have ord\<omega>: "Ord (\<omega> \<up> \<alpha>s ! k')"
       using that by auto
     from that id_take_nth_drop [of k' "take k \<alpha>s"]
     obtain l where "take k \<alpha>s = take k' \<alpha>s @ (\<alpha>s!k') # l"
       by (simp add: min_def)
     then show ?thesis
-      using that  by (auto simp: E_def lift_def add.assoc dest!: OrdmemD [OF ord\<omega>] intro: less_le_trans)
+      using that unfolding E_def lift_def less_sets_def
+      by (auto dest!: OrdmemD [OF ord\<omega>] intro: less_le_trans)
   qed
   have elts_E: "elts (E k) \<subseteq> elts (\<omega>_sum \<alpha>s)"
     if "k < length \<alpha>s" for k
   proof -
     have "\<omega> \<up> (\<alpha>s!k) \<le> \<omega>_sum (drop k \<alpha>s)"
       by (metis that Cons_nth_drop_Suc \<omega>_sum_Cons add_le_cancel_left0)
     then have "(+) (\<omega>_sum (take k \<alpha>s)) ` elts (\<omega> \<up> (\<alpha>s!k)) \<subseteq> elts (\<omega>_sum (take k \<alpha>s) + \<omega>_sum (drop k \<alpha>s))"
       by blast
     also have "\<dots> = elts (\<omega>_sum \<alpha>s)"
       using \<omega>_sum_take_drop by auto
     finally show ?thesis
       by (simp add: lift_def E_def)
   qed
   have \<omega>_sum_in_tpD: "\<omega>_sum (take k \<alpha>s) + \<gamma> \<in> elts (tp D)"
     if "\<gamma> \<in> elts (\<omega> \<up> \<alpha>s!k)" "k < length \<alpha>s" for \<gamma> k
     using elts_E lift_def that tpD_eq by (auto simp: E_def)
   have Ord_\<phi>: "Ord (\<phi> (\<omega>_sum (take k \<alpha>s) + \<gamma>))"
     if "\<gamma> \<in> elts (\<omega> \<up> \<alpha>s!k)" "k < length \<alpha>s" for \<gamma> k
     using \<omega>_sum_in_tpD \<open>D \<subseteq> ON\<close> bij_\<phi> bij_betw_imp_surj_on that by fastforce
   define \<pi> where "\<pi> \<equiv> \<lambda>k. ((\<lambda>y. odiff y (\<omega>_sum (take k \<alpha>s))) \<circ> ordermap D VWF)"
       \<comment> \<open>mapping the segments of @{term D} into some power of @{term \<omega>}\<close>
   have bij_\<pi>: "bij_betw (\<pi> k) (\<phi> ` elts (E k)) (elts (\<omega> \<up> (\<alpha>s!k)))"
     if "k < length \<alpha>s" for k
     using that by (auto simp: bij_betw_def \<pi>_def E_def inj_on_def lift_def image_comp \<omega>_sum_in_tpD \<phi>_cancel_right that)
   have \<pi>_iff: "\<pi> k x < \<pi> k y \<longleftrightarrow> (x,y) \<in> VWF"
     if "x \<in> \<phi> ` elts (E k)" "y \<in> \<phi> ` elts (E k)" "k < length \<alpha>s" for k x y
     using that
     by (auto simp: \<pi>_def E_def lift_def \<omega>_sum_in_tpD \<phi>_cancel_right Ord_\<phi> \<phi>_less_iff)
   have tp_E_eq [simp]: "tp (\<phi> ` elts (E k)) = \<omega>\<up>(\<alpha>s!k)"
     if k: "k < length \<alpha>s" for k
-    using ordertype_eq_iff \<pi>_iff bij_\<pi> that
-    by (meson Ord_\<omega> Ord_oexp ord(1) ordertype_VWF_eq_iff replacement small_elts)
-  have tp_L_eq [simp]: "tp (L!k) = \<omega>\<up>(\<alpha>s!k)"
-    if "k < length \<alpha>s" for k
+    by (metis Ord_\<omega> Ord_oexp \<pi>_iff bij_\<pi> ord(1) ordertype_VWF_eq_iff replacement small_elts that)
+  have tp_L_eq [simp]: "tp (L!k) = \<omega>\<up>(\<alpha>s!k)" if "k < length \<alpha>s" for k
     by (simp add: L_def that)
   have UL_eq_D: "\<Union> (list.set L) = D"
   proof (rule antisym)
     show "\<Union> (list.set L) \<subseteq> D"
       by (force simp: L_def tpD_eq bij_betw_apply [OF bij_\<phi>] dest: elts_E)
     show "D \<subseteq> \<Union> (list.set L)"
     proof
       fix \<delta>
       assume "\<delta> \<in> D"
       then have "ordermap D VWF \<delta> \<in> elts (\<omega>_sum \<alpha>s)"
         by (metis \<open>small D\<close> ordermap_in_ordertype tpD_eq)
       then show "\<delta> \<in> \<Union> (list.set L)"
         using \<open>\<delta> \<in> D\<close> \<phi>_cancel_left in_elts_\<omega>_sum
         by (fastforce simp: L_def E_def image_iff lift_def)
     qed
   qed
   show thesis
   proof
     show "indecomposable (tp X)" if "X \<in> list.set L" for X
       using that by (auto simp: L_def indecomposable_\<omega>_power)
   next
     fix M
     assume "M \<subseteq> D" and *: "\<And>X. X \<in> list.set L \<Longrightarrow> tp X \<le> tp (M \<inter> X)"
     show "tp M = tp D"
     proof (rule antisym)
       show "tp M \<le> tp D"
         by (simp add: \<open>M \<subseteq> D\<close> \<open>small D\<close> ordertype_VWF_mono)
       define \<sigma> where "\<sigma> \<equiv> \<lambda>X. inv_into (M \<inter> X) (ordermap (M \<inter> X) VWF)"
                               \<comment> \<open>The bijection from an @{term \<omega>}-power into the appropriate segment of @{term M}\<close>
       have bij_\<sigma>: "bij_betw (\<sigma> X) (elts (tp (M \<inter> X))) (M \<inter> X)" for X
         unfolding \<sigma>_def
-        by (metis (no_types) \<open>M \<subseteq> D\<close> \<open>small D\<close> bij_betw_inv_into inf_le1 ordermap_bij subset_iff_less_eq_V total_on_VWF wf_VWF)
+        by (meson \<open>M \<subseteq> D\<close> \<open>small D\<close> bij_betw_inv_into inf_le1 ordermap_bij smaller_than_small total_on_VWF wf_VWF)
       have Ord_\<sigma>: "Ord (\<sigma> X \<alpha>)" if "\<alpha> \<in> elts (tp (M \<inter> X))" for \<alpha> X
         using \<open>D \<subseteq> ON\<close> \<open>M \<subseteq> D\<close> bij_betw_apply [OF bij_\<sigma>] that by blast
       have \<sigma>_cancel_right: "\<And>\<gamma> X. \<gamma> \<in> elts (tp (M \<inter> X)) \<Longrightarrow> ordermap (M \<inter> X) VWF (\<sigma> X \<gamma>) = \<gamma>"
         by (metis \<sigma>_def f_inv_into_f ordermap_surj subsetD)
       have smM: "small (M \<inter> X)" for X
         by (meson \<open>M \<subseteq> D\<close> \<open>small D\<close> inf_le1 subset_iff_less_eq_V)
-      then have \<sigma>_less: "\<And>X \<gamma> \<delta>. \<lbrakk>\<gamma> < \<delta>; \<gamma> \<in> elts (tp (M \<inter> X)); \<delta> \<in> elts (tp (M \<inter> X))\<rbrakk>
-                          \<Longrightarrow> \<sigma> X \<gamma> < \<sigma> X \<delta>"
-        using ordermap_mono_less bij_betw_apply [OF bij_\<sigma>] VWF_iff_Ord_less \<sigma>_cancel_right trans_VWF wf_VWF
-        by (metis Ord_\<sigma> Ord_linear_lt less_imp_not_less ordermap_mono_less)
       have "\<exists>k < length \<alpha>s. \<gamma> \<in> elts (E k)" if \<gamma>: "\<gamma> \<in> elts (tp D)" for \<gamma>
       proof -
         obtain X where "X \<in> set L" and X: "\<phi> \<gamma> \<in> X"
           by (metis UL_eq_D \<gamma> Union_iff \<phi>_def in_mono inv_into_into ordermap_surj)
         then have "\<exists>k < length \<alpha>s. \<gamma> \<in> elts (E k) \<and> X = \<phi> ` elts (E k)"
           apply (clarsimp simp: L_def)
           by (metis \<gamma> \<phi>_cancel_right elts_E in_mono tpD_eq)
         then show ?thesis
           by blast
       qed
       then obtain K where K: "\<And>\<gamma>. \<gamma> \<in> elts (tp D) \<Longrightarrow> K \<gamma> < length \<alpha>s \<and> \<gamma> \<in> elts (E (K \<gamma>))"
         by metis  \<comment> \<open>The index from @{term "tp D"} to the appropriate segment number\<close>
       define \<psi> where "\<psi> \<equiv> \<lambda>d. \<sigma> (L ! K (ordermap D VWF d)) (\<pi> (K (ordermap D VWF d)) d)"
       show "tp D \<le> tp M"
       proof (rule ordertype_inc_le)
         show "small D" "small M"
           using \<open>M \<subseteq> D\<close> \<open>small D\<close> subset_iff_less_eq_V by auto
       next
         fix d' d
         assume xy: "d' \<in> D" "d \<in> D" and "(d',d) \<in> VWF"
         then have "d' < d"
           using ON_imp_Ord \<open>D \<subseteq> ON\<close> by auto
         define \<gamma>' where "\<gamma>' \<equiv> ordermap D VWF d'"
         define \<gamma> where "\<gamma> \<equiv> ordermap D VWF d"
         have len': "K \<gamma>' < length \<alpha>s" and elts': "\<gamma>' \<in> elts (E (K \<gamma>'))"
             and len: "K \<gamma> < length \<alpha>s" and elts: "\<gamma> \<in> elts (E (K \<gamma>))"
           using K \<open>d' \<in> D\<close> \<open>d \<in> D\<close> by (auto simp: \<gamma>'_def \<gamma>_def \<open>small D\<close> ordermap_in_ordertype)
         have **: "\<And>X w. \<lbrakk>X \<in> list.set L; w \<in> elts (tp X)\<rbrakk> \<Longrightarrow> w \<in> elts (tp (M \<inter> X))"
           using "*" by blast
         have Ord_\<sigma>L: "Ord (\<sigma> (L!k) (\<pi> k d))" if "d \<in> \<phi> ` elts (E k)" "k < length \<alpha>s" for k d
           by (metis "**" Ord_\<sigma> \<open>length L = length \<alpha>s\<close> bij_\<pi> bij_betw_imp_surj_on imageI nth_mem that tp_L_eq)
         have "\<gamma>' < \<gamma>"
-          by (metis \<gamma>'_def \<gamma>_def \<open>d' < d\<close> \<open>small D\<close> \<phi>_cancel_left \<phi>_less_iff ordermap_in_ordertype xy)
+          by (simp add: \<gamma>'_def \<gamma>_def \<open>(d', d) \<in> VWF\<close> \<open>small D\<close> ordermap_mono_less xy)
         then have "K \<gamma>' \<le> K \<gamma>"
-          using elts' elts by (meson in_elts_E_less leI len' less_asym)
+          using elts' elts in_elts_E_less by (meson leI len' less_asym less_sets_def)
         then consider (less) "K \<gamma>' < K \<gamma>" | (equal) "K \<gamma>' = K \<gamma>"
           by linarith
         then have "\<sigma> (L ! K \<gamma>') (\<pi> (K \<gamma>') d') < \<sigma> (L ! K \<gamma>) (\<pi> (K \<gamma>) d)"
         proof cases
           case less
           obtain \<dagger>: "\<sigma> (L ! K \<gamma>') (\<pi> (K \<gamma>') d') \<in> M \<inter> L ! K \<gamma>'" "\<sigma> (L ! K \<gamma>) (\<pi> (K \<gamma>) d) \<in> M \<inter> L ! K \<gamma>"
             using elts' elts len' len
             unfolding \<gamma>'_def \<gamma>_def
             by (metis "**" \<open>length L = length \<alpha>s\<close> \<phi>_cancel_left bij_\<pi> bij_\<sigma> bij_betw_imp_surj_on imageI nth_mem tp_L_eq xy)
           then have "ordermap D VWF (\<sigma> (L ! K \<gamma>') (\<pi> (K \<gamma>') d')) \<in> elts (E (K \<gamma>'))" "ordermap D VWF (\<sigma> (L ! K \<gamma>) (\<pi> (K \<gamma>) d)) \<in> elts (E (K \<gamma>))"
             using len' len elts_E tpD_eq
             by (fastforce simp: L_def \<gamma>'_def \<gamma>_def \<phi>_cancel_right)+
           then have "ordermap D VWF (\<sigma> (L ! K \<gamma>') (\<pi> (K \<gamma>') d')) < ordermap D VWF (\<sigma> (L ! K \<gamma>) (\<pi> (K \<gamma>) d))"
-            using in_elts_E_less len less by blast
+            using in_elts_E_less len less by (meson less_sets_def)
           moreover have "\<sigma> (L ! K \<gamma>') (\<pi> (K \<gamma>') d') \<in> D" "\<sigma> (L ! K \<gamma>) (\<pi> (K \<gamma>) d) \<in> D"
             using \<open>M \<subseteq> D\<close> \<dagger> by auto
           ultimately show ?thesis
             by (metis \<open>small D\<close> \<phi>_cancel_left \<phi>_less_iff ordermap_in_ordertype)
         next
           case equal
-          show ?thesis
+          have \<sigma>_less: "\<And>X \<gamma> \<delta>. \<lbrakk>\<gamma> < \<delta>; \<gamma> \<in> elts (tp (M \<inter> X)); \<delta> \<in> elts (tp (M \<inter> X))\<rbrakk>
+                          \<Longrightarrow> \<sigma> X \<gamma> < \<sigma> X \<delta>"
+            by (metis \<open>D \<subseteq> ON\<close> \<open>M \<subseteq> D\<close> \<sigma>_def dual_order.trans inv_ordermap_VWF_strict_mono_iff le_infI1 smM)
+          have "\<pi> (K \<gamma>) d' < \<pi> (K \<gamma>) d"
+            by (metis equal \<gamma>'_def \<gamma>_def \<open>(d', d) \<in> VWF\<close> \<phi>_cancel_left \<pi>_iff elts elts' imageI len xy)
+          then show ?thesis
             unfolding equal
-          proof (rule \<sigma>_less)
-            show "\<pi> (K \<gamma>) d' < \<pi> (K \<gamma>) d"
-              by (metis equal \<gamma>'_def \<gamma>_def \<open>(d', d) \<in> VWF\<close> \<phi>_cancel_left \<pi>_iff elts elts' imageI len xy)
-            have "\<pi> (K \<gamma>) d' \<in> elts (tp (L ! K \<gamma>))" "\<pi> (K \<gamma>) d \<in> elts (tp (L ! K \<gamma>))"
-              using equal \<phi>_cancel_left \<gamma>'_def elts' len' \<gamma>_def elts len xy
-              by (force intro: bij_betw_apply [OF bij_\<pi>])+
-            then show "\<pi> (K \<gamma>) d' \<in> elts (tp (M \<inter> L ! K \<gamma>))" "\<pi> (K \<gamma>) d \<in> elts (tp (M \<inter> L ! K \<gamma>))"
-              by (simp_all add: "**" len)
-          qed
+            by (metis "**" \<gamma>'_def \<gamma>_def \<open>length L = length \<alpha>s\<close> \<phi>_cancel_left \<sigma>_less bij_\<pi> 
+                 bij_betw_imp_surj_on elts elts' image_eqI len local.equal nth_mem tp_L_eq xy)
         qed
         moreover have "Ord (\<sigma> (L ! K \<gamma>') (\<pi> (K \<gamma>') d'))"
           using Ord_\<sigma>L \<gamma>'_def \<phi>_cancel_left elts' len' xy(1) by fastforce
         moreover have "Ord (\<sigma> (L ! K \<gamma>) (\<pi> (K \<gamma>) d))"
           using Ord_\<sigma>L \<gamma>_def \<phi>_cancel_left elts len xy by fastforce
         ultimately show "(\<psi> d', \<psi> d) \<in> VWF"
           by (simp add: \<psi>_def \<gamma>'_def \<gamma>_def)
       next
         show "\<psi> ` D \<subseteq> M"
         proof (clarsimp simp: \<psi>_def)
           fix d
           assume "d \<in> D"
           define \<gamma> where "\<gamma> \<equiv> ordermap D VWF d"
           have len: "K \<gamma> < length \<alpha>s" and elts: "\<gamma> \<in> elts (E (K \<gamma>))"
             using K \<open>d \<in> D\<close> by (auto simp: \<gamma>_def \<open>small D\<close> ordermap_in_ordertype)
           have "\<pi> (K \<gamma>) d \<in> elts (tp (L! (K \<gamma>)))"
             using bij_\<pi> [OF len] \<open>d \<in> D\<close>
-            apply (simp add: L_def len)
-            by (metis \<gamma>_def \<phi>_cancel_left bij_betw_imp_surj_on elts imageI)
-          then have "\<sigma> (L! (K \<gamma>)) (\<pi> (K \<gamma>) d) \<in> M \<inter> (L! (K \<gamma>))"
-            using smM bij_betw_imp_surj_on [OF ordermap_bij] \<open>length L = length \<alpha>s\<close>
-            unfolding \<sigma>_def
-            by (metis (no_types) "*" inv_into_into len nth_mem vsubsetD total_on_VWF wf_VWF)
+            by (metis \<gamma>_def \<phi>_cancel_left bij_betw_apply elts imageI len tp_L_eq)
           then show "\<sigma> (L ! K (ordermap D VWF d)) (\<pi> (K (ordermap D VWF d)) d) \<in> M"
-            using \<gamma>_def by blast
+            using \<gamma>_def \<open>length L = length \<alpha>s\<close>
+            by (metis "*" Int_iff bij_\<sigma> bij_betw_apply len nth_mem vsubsetD) 
         qed
       qed auto
     qed
   qed (simp add: UL_eq_D)
 qed
 
 
 text \<open>The ``remark'' of Erdős and E. C. Milner, Canad. Math. Bull. Vol. 17 (2), 1974\<close>
 
 proposition indecomposable_imp_Ex_less_sets:
   assumes indec: "indecomposable \<alpha>" and "\<alpha> > 1" 
     and A: "tp A = \<alpha>" "small A" "A \<subseteq> ON"
     and "x \<in> A" and A1: "tp A1 = \<alpha>" "A1 \<subseteq> A"
   obtains A2 where "tp A2 = \<alpha>" "A2 \<subseteq> A1" "{x} \<lless> A2"
 proof -
   have "Ord \<alpha>"
     using indec indecomposable_imp_Ord by blast
   have "Limit \<alpha>"
     by (simp add: assms indecomposable_imp_Limit)
   define \<phi> where "\<phi> \<equiv> inv_into A (ordermap A VWF)"
   then have bij_\<phi>: "bij_betw \<phi> (elts \<alpha>) A"
     using A bij_betw_inv_into down ordermap_bij by blast
   have bij_om: "bij_betw (ordermap A VWF) A (elts \<alpha>)"
     using A down ordermap_bij by blast
   define \<gamma> where "\<gamma> \<equiv> ordermap A VWF x"
   have \<gamma>: "\<gamma> \<in> elts \<alpha>"
     unfolding \<gamma>_def using A \<open>x \<in> A\<close> down by auto
   then have "Ord \<gamma>"
     using Ord_in_Ord \<open>Ord \<alpha>\<close> by blast
   define B where "B \<equiv> \<phi> ` (elts (succ \<gamma>))"
   have B: "{y \<in> A. ordermap A VWF y \<le> ordermap A VWF x} \<subseteq> B"
     apply (clarsimp simp add: B_def \<gamma>_def image_iff \<phi>_def)
     by (metis Ord_linear Ord_ordermap OrdmemD bij_betw_inv_into_left bij_om leD)
   show thesis
   proof
     have "small A1"
       by (meson \<open>small A\<close> A1 smaller_than_small)
     then have "tp (A1 - B) \<le> tp A1"
       by (simp add: ordertype_VWF_mono)
     moreover have "tp (A1 - B) \<ge> \<alpha>"
     proof -
       have "\<not> (\<alpha> \<le> tp B)"
         unfolding B_def
       proof (subst ordertype_VWF_inc_eq)
         show "elts (succ  \<gamma>) \<subseteq> ON"
           by (auto simp: \<gamma>_def ordertype_VWF_inc_eq intro: Ord_in_Ord)
         have sub: "elts (succ  \<gamma>) \<subseteq> elts \<alpha>"
           using Ord_trans \<gamma> \<open>Ord \<alpha>\<close> by auto
         then show "\<phi> ` elts (succ  \<gamma>) \<subseteq> ON"
           using \<open>A \<subseteq> ON\<close> bij_\<phi> bij_betw_imp_surj_on by blast
         have "succ \<gamma> \<in> elts \<alpha>"
           using \<gamma> Limit_def \<open>Limit \<alpha>\<close> by blast
         with A sub show "\<phi> u < \<phi> v"
           if "u \<in> elts (succ  \<gamma>)" and "v \<in> elts (succ  \<gamma>)" and "u < v" for u v
           by (metis ON_imp_Ord Ord_linear2 \<phi>_def inv_into_ordermap inv_ordermap_VWF_mono_le leD subset_iff that)
         show "\<not> \<alpha> \<le> tp (elts (succ  \<gamma>))"
           by (metis Limit_def Ord_succ \<gamma> \<open>Limit \<alpha>\<close> \<open>Ord \<gamma>\<close> mem_not_refl ordertype_eq_Ord vsubsetD)
       qed auto
       then show ?thesis
         using indecomposable_ordertype_ge [OF indec, of A1 B] \<open>small A1\<close> A1 by (auto simp: B_def)
     qed
     ultimately show "tp (A1 - B) = \<alpha>"
       using A1 by blast
     have "{x} \<lless> (A - B)"
       using assms B 
       apply (clarsimp simp: less_sets_def  \<phi>_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 \<open>A1 \<subseteq> A\<close> show "{x} \<lless> (A1 - B)" by auto
   qed auto
 qed
 
 
 text \<open>the main theorem, from which they derive the headline result\<close>
 theorem Erdos_Milner_aux:
   assumes part: "partn_lst_VWF \<alpha> [k, \<gamma>] 2"
     and indec: "indecomposable \<alpha>" and "k > 1" "Ord \<gamma>" and \<beta>: "\<beta> \<in> elts \<omega>1"
   shows "partn_lst_VWF (\<alpha>*\<beta>) [ord_of_nat (2*k), min \<gamma> (\<omega>*\<beta>)] 2"
 proof (cases "\<alpha>\<le>1 \<or> \<beta>=0")
   case True
   have "Ord \<alpha>"
     using indec indecomposable_def by blast
   show ?thesis
   proof (cases "\<beta>=0")
     case True
     moreover have "min \<gamma> 0 = 0"
       by (simp add: min_def)
     ultimately show ?thesis
       by (simp add: partn_lst_triv0 [where i=1])
   next
     case False
     then consider (0) "\<alpha>=0" | (1) "\<alpha>=1"
       by (metis Ord_0 OrdmemD True \<open>Ord \<alpha>\<close> 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 \<beta>"
         by (meson ON_imp_Ord Ord_\<omega>1 True \<beta> elts_subset_ON)
       then obtain i where "i < Suc (Suc 0)" "[ord_of_nat k, \<gamma>] ! i \<le> \<alpha>"
         using partn_lst_VWF_nontriv [OF part] 1 by auto
       then have "\<gamma> \<le> 1"
         using \<open>\<alpha>=1\<close> \<open>k > 1\<close> by (fastforce simp: less_Suc_eq)
       then have "min \<gamma> (\<omega>*\<beta>) \<le> 1"
         by (metis Ord_1 Ord_\<omega> Ord_linear_le Ord_mult \<open>Ord \<beta>\<close> min_def order_trans)
       moreover have "elts \<beta> \<noteq> {}"
         using False by auto
       ultimately show ?thesis
         by (auto simp: True \<open>Ord \<beta>\<close> \<open>\<beta>\<noteq>0\<close> \<open>\<alpha>=1\<close> intro!: partn_lst_triv1 [where i=1])
     qed
   qed
 next
   case False
   then have "\<alpha> > 1"
     by (meson Ord_1 Ord_not_le indec indecomposable_def)
   then have "\<alpha> \<ge> \<omega>"
     by (simp add: indec indecomposable_imp_Limit omega_le_Limit)
   have "0 \<in> elts \<beta>"
     using False Ord_\<omega>1 Ord_in_Ord \<beta> mem_0_Ord by blast
   then have "\<beta> \<noteq> 0"
     by force 
   show ?thesis
     unfolding partn_lst_def
   proof clarsimp
     fix f
     assume "f \<in> [elts (\<alpha>*\<beta>)]\<^bsup>2\<^esup> \<rightarrow> {..<Suc (Suc 0)}"
     then have f: "f \<in> [elts (\<alpha>*\<beta>)]\<^bsup>2\<^esup> \<rightarrow> {..<2::nat}"
       by (simp add: eval_nat_numeral)
     obtain ord [iff]: "Ord \<alpha>" "Ord \<beta>" "Ord (\<alpha>*\<beta>)"
       using Ord_\<omega>1 Ord_in_Ord \<beta> indec indecomposable_imp_Ord Ord_mult by blast
     have *: False
       if i [rule_format]: "\<forall>H. tp H = ord_of_nat (2*k) \<longrightarrow> H \<subseteq> elts (\<alpha>*\<beta>) \<longrightarrow> \<not> f ` [H]\<^bsup>2\<^esup> \<subseteq> {0}"
         and ii [rule_format]: "\<forall>H. tp H = \<gamma> \<longrightarrow> H \<subseteq> elts (\<alpha>*\<beta>) \<longrightarrow> \<not> f ` [H]\<^bsup>2\<^esup> \<subseteq> {1}"
         and iii [rule_format]: "\<forall>H. tp H = (\<omega>*\<beta>) \<longrightarrow> H \<subseteq> elts (\<alpha>*\<beta>) \<longrightarrow> \<not> f ` [H]\<^bsup>2\<^esup> \<subseteq> {1}"
     proof -
       have Ak0: "\<exists>X \<in> [A]\<^bsup>k\<^esup>. f ` [X]\<^bsup>2\<^esup> \<subseteq> {0}" \<comment>\<open>remark (8) about @{term"A \<subseteq> S"}\<close>
         if A_\<alpha>\<beta>: "A \<subseteq> elts (\<alpha>*\<beta>)" and ot: "tp A \<ge> \<alpha>" 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 \<alpha>)"
           by (meson inj_on_inv_into less_eq_V_def ordermap_surj ot subset_trans)
         have om_A_less: "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x < y\<rbrakk> \<Longrightarrow> ordermap A VWF x < ordermap A VWF y"
           using ord
           by (meson A_\<alpha>\<beta> Ord_in_Ord VWF_iff_Ord_less \<open>small A\<close> in_mono ordermap_mono_less trans_VWF wf_VWF)
         have \<alpha>_sub: "elts \<alpha> \<subseteq> ordermap A VWF ` A"
           by (metis \<open>small A\<close> elts_of_set less_eq_V_def ordertype_def ot replacement)
         have g: "?g \<in> elts \<alpha> \<rightarrow> elts (\<alpha>*\<beta>)"
           by (meson A_\<alpha>\<beta> Pi_I' \<alpha>_sub inv_into_into subset_eq)
         then have fg: "f \<circ> (\<lambda>X. ?g ` X) \<in> [elts \<alpha>]\<^bsup>2\<^esup> \<rightarrow> {..<2}"
           by (rule nsets_compose_image_funcset [OF f _ inj_g])
         obtain i H where "i < 2" "H \<subseteq> elts \<alpha>"
           and ot_eq: "tp H = [k,\<gamma>]!i" "(f \<circ> (\<lambda>X. ?g ` X)) ` (nsets H 2) \<subseteq> {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]\<^bsup>2\<^esup> \<subseteq> {0}"
             using ot_eq \<open>H \<subseteq> elts \<alpha>\<close> \<alpha>_sub by (auto simp: nsets_def [of _ k] inj_on_inv_into elim!: nset_image_obtains)
           moreover have "finite H \<and> card H = k"
             using 0 ot_eq \<open>H \<subseteq> elts \<alpha>\<close> down by (simp add: finite_ordertype_eq_card)
           then have "inv_into A (ordermap A VWF) ` H \<in> [A]\<^bsup>k\<^esup>"
             using \<open>H \<subseteq> elts \<alpha>\<close> \<alpha>_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 \<subseteq> elts (\<alpha>*\<beta>)"
             by (metis A_\<alpha>\<beta> \<alpha>_sub \<open>H \<subseteq> elts \<alpha>\<close> image_subsetI inv_into_into subset_eq)
           have g_less: "?g x < ?g y" if "x < y" "x \<in> elts \<alpha>" "y \<in> elts \<alpha>" for x y
             using Pi_mem [OF g] ord that
             by (meson A_\<alpha>\<beta> Ord_in_Ord Ord_not_le \<open>small A\<close> dual_order.trans elts_subset_ON inv_ordermap_VWF_mono_le ot vsubsetD)
           have [simp]: "tp (?g ` H) = tp H"
             by (meson \<open>H \<subseteq> elts \<alpha>\<close> 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 \<open>H \<subseteq> elts \<alpha>\<close>] ot_eq 1 
             by (auto simp: gH elim!: nset_image_obtains)
         qed
       qed
       define K where "K \<equiv> \<lambda>i x. {y \<in> elts (\<alpha>*\<beta>). x \<noteq> y \<and> f{x,y} = i}"
       have small_K: "small (K i x)" for i x
         by (simp add: K_def)
       define KI where "KI \<equiv> \<lambda>i X. (\<Inter>x\<in>X. K i x)"
       have KI_disj_self: "X \<inter> KI i X = {}" for i X
         by (auto simp: KI_def K_def)
       define M where "M \<equiv> \<lambda>D \<AA> x. {\<nu>::V. \<nu> \<in> D \<and> tp (K 1 x \<inter> \<AA> \<nu>) \<ge> \<alpha>}"
       have M_sub_D: "M D \<AA> x \<subseteq> D" for D \<AA> x
         by (auto simp: M_def)
       have small_M [simp]: "small (M D \<AA> x)" if "small D" for D \<AA> x
         by (simp add: M_def that)
       have 9: "tp {x \<in> A. tp (M D \<AA> x) \<ge> tp D} \<ge> \<alpha>" (is "ordertype ?AD _ \<ge> \<alpha>")
         if inD: "indecomposable (tp D)" and D: "D \<subseteq> elts \<beta>" and A: "A \<subseteq> elts (\<alpha>*\<beta>)" and tpA: "tp A = \<alpha>"
           and \<AA>: "\<AA> \<in> D \<rightarrow> {X. X \<subseteq> elts (\<alpha>*\<beta>) \<and> tp X = \<alpha>}"  for D A \<AA>
           \<comment>\<open>remark (9), assuming an indecomposable order type\<close>
       proof (rule ccontr)
         define A' where "A' \<equiv> {x \<in> A. \<not> tp (M D \<AA> x) \<ge> tp D}"
         have small [iff]: "small A" "small D"
           using A D down by (auto simp: M_def)
         have small_\<AA>: "small (\<AA> \<delta>)" if "\<delta> \<in> D" for \<delta>
           using that \<AA> by (auto simp: Pi_iff subset_iff_less_eq_V)
         assume not_\<alpha>_le: "\<not> \<alpha> \<le> tp {x \<in> A. tp (M D \<AA> x) \<ge> tp D}"
         moreover
         obtain "small A" "small A'" "A' \<subseteq> A" and A'_sub: "A' \<subseteq> elts (\<alpha>*\<beta>)"
           using A'_def A down by auto
         moreover have "A' = A - ?AD"
           by (force simp: A'_def)
         ultimately have A'_ge: "tp A' \<ge> \<alpha>"
           by (metis (no_types, lifting) dual_order.refl indec indecomposable_ordertype_eq mem_Collect_eq subsetI tpA)
         obtain X where "X \<subseteq> A'" "finite X" "card X = k" and fX0: "f ` [X]\<^bsup>2\<^esup> \<subseteq> {0}"
           using Ak0 [OF A'_sub A'_ge] by (auto simp: nsets_def [of _ k])
         then have \<ddagger>: "\<not> tp (M D \<AA> x) \<ge> tp D" if "x \<in> X" for x
           using that by (auto simp: A'_def)
         obtain x where "x \<in> X"
           using \<open>card X = k\<close> \<open>k>1\<close> by fastforce
         have "\<not> D \<subseteq> (\<Union> x\<in>X. M D \<AA> x)"
         proof
           assume not: "D \<subseteq> (\<Union>x\<in>X. M D \<AA> x)"
           have "\<exists>X\<in>M D \<AA> ` X. tp D \<le> tp X"
           proof (rule indecomposable_ordertype_finite_ge [OF inD])
             show "M D \<AA> ` X \<noteq> {}"
               using A'_def A'_ge not not_\<alpha>_le by auto
             show "small (\<Union> (M D \<AA> ` X))"
               using \<open>finite X\<close> by (simp add: finite_imp_small)
           qed (use \<open>finite X\<close> not in auto)
           then show False
             by (simp add: \<ddagger>)
         qed
         then obtain \<nu> where "\<nu> \<in> D" and \<nu>: "\<nu> \<notin> (\<Union> x\<in>X. M D \<AA> x)"
           by blast
         define \<A> where "\<A> \<equiv> {KI 0 X \<inter> \<AA> \<nu>, \<Union>x\<in>X. K 1 x \<inter> \<AA> \<nu>, X \<inter> \<AA> \<nu>}"
         have \<alpha>\<beta>: "X \<subseteq> elts (\<alpha>*\<beta>)" "\<AA> \<nu> \<subseteq> elts (\<alpha>*\<beta>)"
           using A'_sub \<open>X \<subseteq> A'\<close> \<AA> \<open>\<nu> \<in> D\<close> by auto
         then have "KI 0 X \<union> (\<Union>x\<in>X. K 1 x) \<union> X = elts (\<alpha>*\<beta>)"
           using \<open>x \<in> X\<close> f by (force simp: K_def KI_def Pi_iff less_2_cases_iff)
         with \<alpha>\<beta> have \<AA>\<nu>_\<A>: "finite \<A>" "\<AA> \<nu> \<subseteq> \<Union>\<A>"
           by (auto simp: \<A>_def)
         then have "\<not> tp (K 1 x \<inter> \<AA> \<nu>) \<ge> \<alpha>" if "x \<in> X" for x
           using that \<open>\<nu> \<in> D\<close> \<nu> \<open>k > 1\<close> \<open>card X = k\<close> by (fastforce simp: M_def)
         moreover have sm_K1: "small (\<Union>x\<in>X. K 1 x \<inter> \<AA> \<nu>)"
           by (meson Finite_V Int_lower2 \<open>\<nu> \<in> D\<close> \<open>finite X\<close> small_\<AA> small_UN smaller_than_small)
         ultimately have not1: "\<not> tp (\<Union>x\<in>X. K 1 x \<inter> \<AA> \<nu>) \<ge> \<alpha>"
           using \<open>finite X\<close> \<open>x \<in> X\<close> indecomposable_ordertype_finite_ge [OF indec, of "(\<lambda>x. K 1 x \<inter> \<AA> \<nu>) ` X"] by blast
         moreover have "\<not> tp (X \<inter> \<AA> \<nu>) \<ge> \<alpha>"
           using \<open>finite X\<close> \<open>\<alpha> \<ge> \<omega>\<close>
           by (meson finite_Int mem_not_refl ordertype_VWF_\<omega> vsubsetD)
         moreover have "\<alpha> \<le> tp (\<AA> \<nu>)"
           using \<AA> \<open>\<nu> \<in> D\<close> small_\<AA> by fastforce+
         moreover have "small (\<Union> \<A>)"
           using \<open>\<nu> \<in> D\<close> small_\<AA> by (fastforce simp: \<A>_def intro: smaller_than_small sm_K1)
         ultimately have K0\<AA>_ge: "tp (KI 0 X \<inter> \<AA> \<nu>) \<ge> \<alpha>"
           using indecomposable_ordertype_finite_ge [OF indec \<AA>\<nu>_\<A>] by (auto simp: \<A>_def)
         have \<AA>\<nu>: "\<AA> \<nu> \<subseteq> elts (\<alpha>*\<beta>)" "tp (\<AA> \<nu>) = \<alpha>"
           using \<open>\<nu> \<in> D\<close> \<AA> by blast+
         then obtain Y where Ysub: "Y \<subseteq> KI 0 X \<inter> \<AA> \<nu>" and "finite Y" "card Y = k" and fY0: "f ` [Y]\<^bsup>2\<^esup> \<subseteq> {0}"
           using Ak0 [OF _ K0\<AA>_ge] by (auto simp: nsets_def [of _ k])
         have \<dagger>: "X \<inter> Y = {}"
           using Ysub KI_disj_self by blast
         then have "card (X \<union> Y) = 2*k"
           by (simp add: \<open>card X = k\<close> \<open>card Y = k\<close> \<open>finite X\<close> \<open>finite Y\<close> card_Un_disjoint)
         moreover have "X \<union> Y \<subseteq> elts (\<alpha>*\<beta>)"
           using A'_sub \<open>X \<subseteq> A'\<close> \<AA>\<nu>(1) \<open>Y \<subseteq> KI 0 X \<inter> \<AA> \<nu>\<close> by auto
         moreover have "f ` [X \<union> Y]\<^bsup>2\<^esup> \<subseteq> {0}"
           using fX0 fY0 Ysub by (auto simp: \<dagger> nsets_disjoint_2 image_Un image_UN KI_def K_def)
         ultimately show False
           using i \<open>finite X\<close> \<open>finite Y\<close> ordertype_VWF_finite_nat by auto
       qed
       have IX: "tp {x \<in> A. tp (M D \<AA> x) \<ge> tp D} \<ge> \<alpha>"
         if D: "D \<subseteq> elts \<beta>" and A: "A \<subseteq> elts (\<alpha>*\<beta>)" and tpA: "tp A = \<alpha>"
           and \<AA>: "\<AA> \<in> D \<rightarrow> {X. X \<subseteq> elts (\<alpha>*\<beta>) \<and> tp X = \<alpha>}" for D A \<AA>
           \<comment>\<open>remark (9) for any order type\<close>
       proof -
         obtain L where UL: "\<Union>(List.set L) \<subseteq> D"
           and indL: "\<And>X. X \<in> List.set L \<Longrightarrow> indecomposable (tp X)"
           and eqL: "\<And>M. \<lbrakk>M \<subseteq> D; \<And>X. X \<in> List.set L \<Longrightarrow> tp (M \<inter> X) \<ge> tp X\<rbrakk> \<Longrightarrow> tp M = tp D"
           using ord by (metis strong_ordertype_eq D order_refl)
         obtain A'' where A'': "A'' \<subseteq> A" "tp A'' \<ge> \<alpha>"
           and "\<And>x X. \<lbrakk>x \<in> A''; X \<in> List.set L\<rbrakk> \<Longrightarrow> tp (M D \<AA> x \<inter> X) \<ge> tp X"
           using UL indL
         proof (induction L arbitrary: thesis)
           case (Cons X L)
           then obtain A'' where A'': "A'' \<subseteq> A" "tp A'' \<ge> \<alpha>" and "X \<subseteq> D"
             and ge_X: "\<And>x X. \<lbrakk>x \<in> A''; X \<in> List.set L\<rbrakk> \<Longrightarrow> tp (M D \<AA> x \<inter> X) \<ge> tp X" by auto
           then have tp_A'': "tp A'' = \<alpha>"
             by (metis A antisym down ordertype_VWF_mono tpA)
           have ge_\<alpha>: "tp {x \<in> A''. tp (M X \<AA> x) \<ge> tp X} \<ge> \<alpha>"
             by (rule 9) (use A A'' tp_A'' Cons.prems \<open>D \<subseteq> elts \<beta>\<close> \<open>X \<subseteq> D\<close> \<AA> in auto)
           let ?A = "{x \<in> A''. tp (M D \<AA> x \<inter> X) \<ge> tp X}"
           have M_eq: "M D \<AA> x \<inter> X = M X \<AA> x" if "x \<in> A''" for x
             using that \<open>X \<subseteq> D\<close> by (auto simp: M_def)
           show thesis
           proof (rule Cons.prems)
             show "\<alpha> \<le> tp ?A"
               using ge_\<alpha> by (simp add: M_eq cong: conj_cong)
             show "tp Y \<le> tp (M D \<AA> x \<inter> Y)" if "x \<in> ?A" "Y \<in> 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 \<AA> x) \<ge> tp D" if "x \<in> A''" for x
           using eqL that by (auto simp: M_def)
         have "\<alpha> \<le> tp A''"
           by (simp add: A'')
         also have "\<dots> \<le> tp {x \<in> A''. tp (M D \<AA> x) \<ge> tp D}"
           by (metis (mono_tags, lifting) tp_M_ge eq_iff mem_Collect_eq subsetI)
         also have "\<dots> \<le> tp {x \<in> A. tp D \<le> tp (M D \<AA> x)}"
           by (rule ordertype_mono) (use A'' A down in auto)
         finally show ?thesis .
       qed
       have IX': "tp {x \<in> A'. tp (K 1 x \<inter> A) \<ge> \<alpha>} \<ge> \<alpha>"
         if A: "A \<subseteq> elts (\<alpha>*\<beta>)" "tp A = \<alpha>" and A': "A' \<subseteq> elts (\<alpha>*\<beta>)" "tp A' = \<alpha>" for A A'
       proof -
         have \<ddagger>: "\<alpha> \<le> tp (K 1 t \<inter> A)" if "1 \<le> tp {\<nu>. \<nu> = 0 \<and> \<alpha> \<le> tp (K 1 t \<inter> A)}" for t
           using that
           by (metis Collect_empty_eq less_eq_V_0_iff ordertype_empty zero_neq_one)
         have "tp {x \<in> A'. 1 \<le> tp {\<nu>. \<nu> = 0 \<and> \<alpha> \<le> tp (K 1 x \<inter> A)}}
             \<le> tp {x \<in> A'. \<alpha> \<le> tp (K 1 x \<inter> A)}"
           by (rule ordertype_mono) (use "\<ddagger>" A' in \<open>auto simp: down\<close>)
         then show ?thesis
           using IX [of "{0}" A' "\<lambda>x. A"] that \<open>0 \<in> elts \<beta>\<close> by (force simp: M_def)
       qed
 
       have 10: "\<exists>x0 \<in> A. \<exists>g \<in> elts \<beta> \<rightarrow> elts \<beta>. strict_mono_on g (elts \<beta>) \<and> (\<forall>\<nu> \<in> F. g \<nu> = \<nu>)
                                       \<and> (\<forall>\<nu> \<in> elts \<beta>. tp (K 1 x0 \<inter> \<AA> (g \<nu>)) \<ge> \<alpha>)"
         if F: "finite F" "F \<subseteq> elts \<beta>"
           and A: "A \<subseteq> elts (\<alpha>*\<beta>)" "tp A = \<alpha>"
           and \<AA>: "\<AA> \<in> elts \<beta> \<rightarrow> {X. X \<subseteq> elts (\<alpha>*\<beta>) \<and> tp X = \<alpha>}"
         for F A \<AA>
       proof -
         define p where "p \<equiv> card F"
         have "\<beta> \<notin> F"
           using that by auto
         then obtain \<iota> :: "nat \<Rightarrow> V" where bij\<iota>: "bij_betw \<iota> {..p} (insert \<beta> F)" and mon\<iota>: "strict_mono_on \<iota> {..p}"
           using ZFC_Cardinals.ex_bij_betw_strict_mono_card [of "insert \<beta> F"] elts_subset_ON \<open>Ord \<beta>\<close> F
           by (simp add: p_def lessThan_Suc_atMost) blast
         have less_\<iota>_I: "\<iota> k < \<iota> l" if "k < l" "l \<le> p" for k l
           using mon\<iota> that by (auto simp: strict_mono_on_def)
         then have less_\<iota>_D: "k < l" if "\<iota> k < \<iota> l" "k \<le> p" for k l
           by (metis less_asym linorder_neqE_nat that)
         have Ord_\<iota>: "Ord (\<iota> k)" if "k \<le> p" for k
           by (metis (no_types, lifting) ON_imp_Ord atMost_iff insert_subset mem_Collect_eq order_trans  \<open>F \<subseteq> elts \<beta>\<close> bij\<iota> bij_betwE elts_subset_ON \<open>Ord \<beta>\<close> that)
         have le_\<iota>0 [simp]: "\<And>j. j \<le> p \<Longrightarrow> \<iota> 0 \<le> \<iota> j"
           by (metis eq_refl leI le_0_eq less_\<iota>_I less_imp_le)
         have le_\<iota>: "\<iota> i \<le> \<iota> (j - Suc 0)" if "i < j" "j \<le> p" for i j
         proof (cases i)
           case 0 then show ?thesis
             using le_\<iota>0 that by auto
         next
           case (Suc i') then show ?thesis
             by (metis (no_types, hide_lams) Suc_pred le_less less_Suc_eq less_Suc_eq_0_disj less_\<iota>_I not_less_eq that)
         qed
 
         have [simp]: "\<iota> p = \<beta>"
         proof -
           obtain k where k: "\<iota> k = \<beta>" "k \<le> p"
             by (meson atMost_iff bij\<iota> bij_betw_iff_bijections insertI1)
           then have "k = p \<or> k < p"
             by linarith
           then show ?thesis
             using bij\<iota> ord k that(2)
             by (metis OrdmemD atMost_iff bij_betw_iff_bijections insert_iff leD less_\<iota>_D order_refl subsetD)
         qed
 
         have F_imp_Ex: "\<exists>k < p. \<xi> = \<iota> k" if "\<xi> \<in> F" for \<xi>
         proof -
           obtain k where k: "k \<le> p" "\<xi> = \<iota> k"
             by (metis \<open>\<xi> \<in> F\<close> atMost_iff bij\<iota> bij_betw_def imageE insert_iff)
           then show ?thesis
             using \<open>\<beta> \<notin> F\<close> \<open>\<iota> p = \<beta>\<close> le_imp_less_or_eq that by blast
         qed
         have F_imp_ge: "\<xi> \<ge> \<iota> 0" if "\<xi> \<in> F" for \<xi>
           using F_imp_Ex [OF that] by (metis dual_order.order_iff_strict le0 less_\<iota>_I)
         define D where "D \<equiv> \<lambda>k. (if k=0 then {..<\<iota> 0} else {\<iota> (k-1)<..<\<iota> k}) \<inter> elts \<beta>"
         have D\<beta>: "D k \<subseteq> elts \<beta>" 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 \<beta>) \<AA> x \<inter> D k = M (D k) \<AA> x" if "k \<le> p" for x k
           using D\<beta> by (auto simp: M_def)
         have \<iota>_le_if_D: "\<iota> k \<le> \<mu>" if "\<mu> \<in> D (Suc k)" for \<mu> k
           using that by (simp add: D_def order.order_iff_strict)
         have mono_D: "D i \<lless> D j" if "i < j" "j \<le> 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_\<iota> less_le_trans less_trans)
         qed (use that in auto)
         then have disjnt_DD: "disjnt (D i) (D j)" if "i \<noteq> j" "i \<le> p" "j \<le> p" for i j
           by (meson disjnt_sym less_linear less_sets_imp_disjnt that)
         have UN_D_eq: "(\<Union>l \<le> k. D l) = {..<\<iota> k} \<inter> (elts \<beta> - F)" if "k \<le> 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) \<union> {..<\<iota> k} \<inter> (elts \<beta> - F) = {..<\<iota> (Suc k)} \<inter> (elts \<beta> - F)"
             (is "?lhs = ?rhs")
           proof
             show "?lhs \<subseteq> ?rhs"
               using Suc.prems
               by (auto simp: D_def if_split_mem2 intro: less_\<iota>_I less_trans dest!: less_\<iota>_D F_imp_Ex)
             have "\<And>x. \<lbrakk>x < \<iota> (Suc k); x \<in> elts \<beta>; x \<notin> F; \<iota> k \<le> x\<rbrakk> \<Longrightarrow> \<iota> k < x"
               using Suc.prems \<open>F \<subseteq> elts \<beta>\<close> bij\<iota> le_imp_less_or_eq
               by (fastforce simp: bij_betw_iff_bijections)
             then show "?rhs \<subseteq> ?lhs"
               using Suc.prems by (auto simp: D_def Ord_not_less Ord_in_Ord [OF \<open>Ord \<beta>\<close>] Ord_\<iota> if_split_mem2)
           qed
           then
           show ?case
             using Suc by (simp add: atMost_Suc)
         qed
         have \<beta>_decomp: "elts \<beta> = F \<union> (\<Union>k \<le> p. D k)"
           using \<open>F \<subseteq> elts \<beta>\<close> OrdmemD [OF \<open>Ord \<beta>\<close>] by (auto simp: UN_D_eq)
         define \<beta>idx where "\<beta>idx \<equiv> \<lambda>\<nu>. @k. \<nu> \<in> D k \<and> k \<le> p"
         have \<beta>idx: "\<nu> \<in> D (\<beta>idx \<nu>) \<and> \<beta>idx \<nu> \<le> p" if "\<nu> \<in> elts \<beta> - F" for \<nu>
           using that by (force simp: \<beta>idx_def \<beta>_decomp intro: someI_ex del: conjI)
         have any_imp_\<beta>idx: "k = \<beta>idx \<nu>" if "\<nu> \<in> D k" "k \<le> p" for k \<nu>
         proof (rule ccontr)
           assume non: "k \<noteq> \<beta>idx \<nu>"
           have "\<nu> \<notin> F"
             using that UN_D_eq by auto
           then show False
             using disjnt_DD [OF non] by (metis D\<beta> Diff_iff \<beta>idx disjnt_iff subsetD that)
         qed
         have "\<exists>A'. A' \<subseteq> A \<and> tp A' = \<alpha> \<and> (\<forall>x \<in> A'. F \<subseteq> M (elts \<beta>) \<AA> x)"
           using F
         proof induction
           case (insert \<nu> F)
           then obtain A' where "A' \<subseteq> A" and A': "A' \<subseteq> elts (\<alpha>*\<beta>)" "tp A' = \<alpha>" and FN: "\<And>x. x \<in> A' \<Longrightarrow> F \<subseteq> M (elts \<beta>) \<AA> x"
             using A(1) by auto
           define A'' where "A'' \<equiv> {x \<in> A'. \<alpha> \<le> tp (K 1 x \<inter> \<AA> \<nu>)}"
           have "\<nu> \<in> elts \<beta>" "F \<subseteq> elts \<beta>"
             using insert by auto
           note ordertype_eq_Ord [OF \<open>Ord \<beta>\<close>, simp]
           show ?case
           proof (intro exI conjI)
             show "A'' \<subseteq> A"
               using \<open>A' \<subseteq> A\<close> by (auto simp: A''_def)
             have "tp A'' \<le> \<alpha>"
               using \<open>A'' \<subseteq> A\<close> down ordertype_VWF_mono A by blast
             moreover have "\<AA> \<nu> \<subseteq> elts (\<alpha>*\<beta>)" "tp (\<AA> \<nu>) = \<alpha>"
               using \<AA> \<open>\<nu> \<in> elts \<beta>\<close> by auto
             then have "\<alpha> \<le> tp A''"
               using IX' [OF _ _ A'] by (simp add: A''_def)
             ultimately show "tp A'' = \<alpha>"
               by (rule antisym)
             have "\<nu> \<in> M (elts \<beta>) \<AA> x" "F \<subseteq> M (elts \<beta>) \<AA> x"
               if "x \<in> A''" for x
             proof -
               show "F \<subseteq> M (elts \<beta>) \<AA> x"
                 using A''_def FN that by blast
               show "\<nu> \<in> M (elts \<beta>) \<AA> x"
                 using \<open>\<nu> \<in> elts \<beta>\<close> that by (simp add: M_def A''_def)
             qed
             then show "\<forall>x\<in>A''. insert \<nu> F \<subseteq> M (elts \<beta>) \<AA> x"
               by blast
           qed
         qed (use A in auto)
         then obtain A' where A': "A' \<subseteq> A" "tp A' = \<alpha>" and FN: "\<And>x. x \<in> A' \<Longrightarrow> F \<subseteq> M (elts \<beta>) \<AA> x"
           by metis
         have False
           if *: "\<And>x0 g. \<lbrakk>x0 \<in> A; g \<in> elts \<beta> \<rightarrow> elts \<beta>; strict_mono_on g (elts \<beta>)\<rbrakk>
                    \<Longrightarrow> (\<exists>\<nu>\<in>F. g \<nu> \<noteq> \<nu>) \<or> (\<exists>\<nu>\<in>elts \<beta>. tp (K 1 x0 \<inter> \<AA> (g \<nu>)) < \<alpha>)"
         proof -
           { fix x       \<comment> \<open>construction of the monotone map @{term g} mentioned above\<close>
             assume "x \<in> A'"
             with A' have "x \<in> A" by blast
             have "\<exists>k. k \<le> p \<and> tp (M (D k) \<AA> x) < tp (D k)" (is "?P")
             proof (rule ccontr)
               assume "\<not> ?P"
               then have le: "tp (D k) \<le> tp (M (D k) \<AA> x)" if "k \<le> p" for k
                 by (meson Ord_linear2 Ord_ordertype that)
               have "\<exists>f\<in>D k \<rightarrow> M (D k) \<AA> x. inj_on f (D k) \<and> (strict_mono_on f (D k))"
                 if "k \<le> 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\<beta> M_sub_D Ord_in_Ord PiE VWF_iff_Ord_less ord(2) subsetD)
               then obtain h where fun_h: "\<And>k. k \<le> p \<Longrightarrow> h k \<in> D k \<rightarrow> M (D k) \<AA> x"
                 and inj_h: "\<And>k. k \<le> p \<Longrightarrow> inj_on (h k) (D k)"
                 and mono_h: "\<And>k x y. k \<le> p \<Longrightarrow> strict_mono_on (h k) (D k)"
                 by metis
               then have fun_hD: "\<And>k. k \<le> p \<Longrightarrow> h k \<in> D k \<rightarrow> D k"
                 by (auto simp: M_def)
               have h_increasing: "\<nu> \<le> h k \<nu>"
                 if "k \<le> p" and \<nu>: "\<nu> \<in> D k" for k \<nu>
               proof (rule Ord_mono_imp_increasing)
                 show "h k \<in> D k \<rightarrow> D k"
                   by (simp add: fun_hD that(1))
                 show "D k \<subseteq> ON"
                   using D\<beta> elts_subset_ON ord(2) by blast
               qed (auto simp: that mono_h)
               define g where "g \<equiv> \<lambda>\<nu>. if \<nu> \<in> F then \<nu> else h (\<beta>idx \<nu>) \<nu>"
               have [simp]: "g \<nu> = \<nu>" if "\<nu> \<in> F" for \<nu>
                 using that by (auto simp: g_def)
               have fun_g: "g \<in> elts \<beta> \<rightarrow> elts \<beta>"
               proof (rule Pi_I)
                 fix x assume "x \<in> elts \<beta>"
                 then have "x \<in> D (\<beta>idx x)" "\<beta>idx x \<le> p" if "x \<notin> F"
                   using that by (auto simp: \<beta>idx)
                 then show "g x \<in> elts \<beta>"
                   using fun_h  D\<beta> M_sub_D \<open>x \<in> elts \<beta>\<close>
                   by (simp add: g_def) blast
               qed
               have h_in_D: "h (\<beta>idx \<nu>) \<nu> \<in> D (\<beta>idx \<nu>)" if "\<nu> \<notin> F" "\<nu> \<in> elts \<beta>" for \<nu>
                 using \<beta>idx fun_hD that by fastforce
               have 1: "\<iota> k < h (\<beta>idx \<nu>) \<nu>"
                 if "k < p" and \<nu>: "\<nu> \<notin> F" "\<nu> \<in> elts \<beta>" and "\<iota> k < \<nu>" for k \<nu>
                 using that h_in_D [OF \<nu>] \<beta>idx
                 by (fastforce simp: D_def dest: h_increasing split: if_split_asm)
               moreover have 2: "h (\<beta>idx \<mu>) \<mu> < \<iota> k"
                 if \<mu>: "\<mu> \<notin> F" "\<mu> \<in> elts \<beta>" and "k < p" "\<mu> < \<iota> k" for \<mu> k
               proof -
                 have "\<beta>idx \<mu> \<le> k"
                 proof (rule ccontr)
                   assume "\<not> \<beta>idx \<mu> \<le> k"
                   then have "k < \<beta>idx \<mu>"
                     by linarith
                   then show False
                     using \<iota>_le_if_D \<beta>idx
                     by (metis Diff_iff Suc_pred le0 leD le_\<iota> le_less_trans \<mu> \<open>\<mu> < \<iota> k\<close>)
                 qed
                 then show ?thesis
                   using that h_in_D [OF \<mu>]
                   by (smt (verit, best) Int_lower1 UN_D_eq UN_I atMost_iff lessThan_iff less_imp_le subset_eq)
               qed
               moreover have "h (\<beta>idx \<mu>) \<mu> < h (\<beta>idx \<nu>) \<nu>"
                 if \<mu>: "\<mu> \<notin> F" "\<mu> \<in> elts \<beta>" and \<nu>: "\<nu> \<notin> F" "\<nu> \<in> elts \<beta>" and "\<mu> < \<nu>" for \<mu> \<nu>
               proof -
                 have le: "\<beta>idx \<mu> \<le> \<beta>idx \<nu>" if "\<iota> (\<beta>idx \<mu> - Suc 0) < h (\<beta>idx \<mu>) \<mu>" "h (\<beta>idx \<nu>) \<nu> < \<iota> (\<beta>idx \<nu>)"
                   by (metis 2 that Diff_iff \<beta>idx \<mu> \<nu> \<open>\<mu> < \<nu>\<close> dual_order.strict_implies_order dual_order.strict_trans1 h_increasing leI le_\<iota> less_asym)
                 have "h 0 \<mu> < h 0 \<nu>" if "\<beta>idx \<mu> = 0" "\<beta>idx \<nu> = 0"
                   using that mono_h unfolding strict_mono_on_def
                   by (metis Diff_iff \<beta>idx \<mu> \<nu> \<open>\<mu> < \<nu>\<close>)
                 moreover have "h 0 \<mu> < h (\<beta>idx \<nu>) \<nu>"
                   if "0 < \<beta>idx \<nu>" "h 0 \<mu> < \<iota> 0" and "\<iota> (\<beta>idx \<nu> - Suc 0) < h (\<beta>idx \<nu>) \<nu>"
                   by (meson DiffI \<beta>idx \<nu> le_\<iota> le_less_trans less_le_not_le that)
                 moreover have "\<beta>idx \<nu> \<noteq> 0"
                   if "0 < \<beta>idx \<mu>" "h 0 \<nu> < \<iota> 0" "\<iota> (\<beta>idx \<mu> - Suc 0) < h (\<beta>idx \<mu>) \<mu>"
                   using le le_0_eq that by fastforce
                 moreover have "h (\<beta>idx \<mu>) \<mu> < h (\<beta>idx \<nu>) \<nu>"
                   if "\<iota> (\<beta>idx \<mu> - Suc 0) < h (\<beta>idx \<mu>) \<mu>" "h (\<beta>idx \<nu>) \<nu> < \<iota> (\<beta>idx \<nu>)"
                     "h (\<beta>idx \<mu>) \<mu> < \<iota> (\<beta>idx \<mu>)" "\<iota> (\<beta>idx \<nu> - Suc 0) < h (\<beta>idx \<nu>) \<nu>"
                   using mono_h unfolding strict_mono_on_def
                   by (metis le Diff_iff \<beta>idx \<mu> \<nu> \<open>\<mu> < \<nu>\<close> le_\<iota> le_less le_less_trans that)
                 ultimately show  ?thesis
                   using h_in_D [OF \<mu>] h_in_D [OF \<nu>] by (simp add: D_def split: if_split_asm)
               qed
               ultimately have sm_g: "strict_mono_on g (elts \<beta>)"
                 by (auto simp: g_def strict_mono_on_def dest!: F_imp_Ex)
               show False
                 using * [OF \<open>x \<in> A\<close> fun_g sm_g]
               proof safe
                 fix \<nu>
                 assume "\<nu> \<in> elts \<beta>" and \<nu>: "tp (K 1 x \<inter> \<AA> (g \<nu>)) < \<alpha>"
                 have FM: "F \<subseteq> M (elts \<beta>) \<AA> x"
                   by (meson FN \<open>x \<in> A'\<close>)
                 have False if "tp (K (Suc 0) x \<inter> \<AA> \<nu>) < \<alpha>" "\<nu> \<in> F"
                   using that FM by (auto simp: M_def)
                 moreover have False if "tp (K (Suc 0) x \<inter> \<AA> (g \<nu>)) < \<alpha>" "\<nu> \<in> D k" "k \<le> p" "\<nu> \<notin> F" for k
                 proof -
                   have "h (\<beta>idx \<nu>) \<nu> \<in> M (D (\<beta>idx \<nu>)) \<AA> x"
                     using fun_h \<beta>idx \<open>\<nu> \<in> elts \<beta>\<close> \<open>\<nu> \<notin> F\<close> by auto
                   then show False
                     using that by (simp add: M_def g_def leD)
                 qed
                 ultimately show False
                   using \<open>\<nu> \<in> elts \<beta>\<close> \<nu> by (force simp: \<beta>_decomp)
               qed auto
             qed
             then have "\<exists>l. l \<le> p \<and> tp (M (elts \<beta>) \<AA> x \<inter> D l) < tp (D l)"
               using M_Int_D by auto
           }
           then obtain l where lp: "\<And>x. x \<in> A'\<Longrightarrow> l x \<le> p"
             and lless: "\<And>x. x \<in> A'\<Longrightarrow> tp (M (elts \<beta>) \<AA> x \<inter> D (l x)) < tp (D (l x))"
             by metis
           obtain A'' L where "A'' \<subseteq> A'" and A'': "A'' \<subseteq> elts (\<alpha>*\<beta>)" "tp A'' = \<alpha>" and lL: "\<And>x. x \<in> A'' \<Longrightarrow> l x = L"
           proof -
             have eq: "A' = (\<Union>i\<le>p. {x \<in> A'. l x = i})"
               using lp by auto
             have "\<exists>X\<in>(\<lambda>i. {x \<in> A'. l x = i}) ` {..p}. \<alpha> \<le> tp X"
             proof (rule indecomposable_ordertype_finite_ge [OF indec])
               show "small (\<Union>i\<le>p. {x \<in> 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'' \<in> (\<lambda>i. {x \<in> A'. l x = i}) ` {..p}" and "\<alpha> \<le> tp A''"
               then obtain L where L: "\<And>x. x \<in> A'' \<Longrightarrow> l x = L"
                 by auto
               have "A'' \<subseteq> A'"
                 using A'' by force
               then have "tp A'' \<le> tp A'"
                 by (meson A' A down order_trans ordertype_VWF_mono)
               with \<open>\<alpha> \<le> tp A''\<close> have "tp A'' = \<alpha>"
                 using A'(2) by auto
               moreover have "A'' \<subseteq> elts (\<alpha>*\<beta>)"
                 using A' A \<open>A'' \<subseteq> A'\<close> by auto
               ultimately show thesis
                 using L that [OF \<open>A'' \<subseteq> A'\<close>] by blast
             qed
           qed
           have \<AA>D: "\<AA> \<in> D L \<rightarrow> {X. X \<subseteq> elts (\<alpha>*\<beta>) \<and> tp X = \<alpha>}"
             using \<AA> D\<beta> by blast
           have "M (elts \<beta>) \<AA> x \<inter> D L = M (D L) \<AA> x" for x
             using D\<beta> by (auto simp: M_def)
           then have "tp (M (D L) \<AA> x) < tp (D L)" if "x \<in> A''" for x
             using lless that \<open>A'' \<subseteq> A'\<close> lL by force
           then have \<dagger>: "{x \<in> A''. tp (D L) \<le> tp (M (D L) \<AA> x)} = {}"
             using leD by blast
           have "\<alpha> \<le> tp {x \<in> A''. tp (D L) \<le> tp (M (D L) \<AA> x)}"
             using IX [OF D\<beta> A'' \<AA>D] by simp
           then show False
             using "\<dagger>" \<open>1 < \<alpha>\<close> by force
         qed
         then show ?thesis
           by (meson Ord_linear2 Ord_ordertype \<open>Ord \<alpha>\<close>)
       qed
       let ?U = "UNIV :: nat set"
       define \<mu> where "\<mu> \<equiv> fst \<circ> from_nat_into (elts \<beta> \<times> ?U)"
       define q where "q \<equiv> to_nat_on (elts \<beta> \<times> ?U)"
       have co_\<beta>U: "countable (elts \<beta> \<times> ?U)"
         by (simp add: \<beta> less_\<omega>1_imp_countable)
       moreover have "elts \<beta> \<times> ?U \<noteq> {}"
         using \<open>0 \<in> elts \<beta>\<close> by blast
       ultimately have "range (from_nat_into (elts \<beta> \<times> ?U)) = (elts \<beta> \<times> ?U)"
         by (metis range_from_nat_into)
       then have \<mu>_in_\<beta> [simp]: "\<mu> i \<in> elts \<beta>" for i
         by (metis SigmaE \<mu>_def comp_apply fst_conv range_eqI)
 
       then have Ord_\<mu> [simp]: "Ord (\<mu> i)" for i
         using Ord_in_Ord by blast
 
       have inf_\<beta>U: "infinite (elts \<beta> \<times> ?U)"
         using \<open>0 \<in> elts \<beta>\<close> finite_cartesian_productD2 by auto
 
       have 11 [simp]: "\<mu> (q (\<nu>,n)) = \<nu>" if "\<nu> \<in> elts \<beta>" for \<nu> n
         by (simp add: \<mu>_def q_def that co_\<beta>U)
       have range_\<mu> [simp]: "range \<mu> = elts \<beta>"
         by (auto simp: image_iff) (metis 11)
       have [simp]: "KI i {} = UNIV" "KI i (insert a X) = K i a \<inter> KI i X" for i a X
         by (auto simp: KI_def)
       define \<Phi> where "\<Phi> \<equiv> \<lambda>n::nat. \<lambda>\<AA> x. (\<forall>\<nu> \<in> elts \<beta>. \<AA> \<nu> \<subseteq> elts (\<alpha>*\<beta>) \<and> tp (\<AA> \<nu>) = \<alpha>) \<and> x ` {..<n} \<subseteq> elts (\<alpha>*\<beta>)
                                          \<and> (\<Union>\<nu> \<in> elts \<beta>. \<AA> \<nu>) \<subseteq> KI 1 (x ` {..<n}) \<and> strict_mono_sets (elts \<beta>) \<AA>"
       define \<Psi> where "\<Psi> \<equiv> \<lambda>n::nat. \<lambda>g \<AA> \<AA>' xn. g \<in> elts \<beta> \<rightarrow> elts \<beta> \<and> strict_mono_on g (elts \<beta>) \<and> (\<forall>i\<le>n. g (\<mu> i) = \<mu> i)
                   \<and> (\<forall>\<nu> \<in> elts \<beta>. \<AA>' \<nu> \<subseteq> K 1 xn \<inter> \<AA> (g \<nu>))
                   \<and> {xn} \<lless> (\<AA>' (\<mu> n)) \<and> xn \<in> \<AA> (\<mu> n)"
       let ?\<AA>0 = "\<lambda>\<nu>. plus (\<alpha> * \<nu>) ` elts \<alpha>"
       have base: "\<Phi> 0 ?\<AA>0 x" for x
         by (auto simp: \<Phi>_def add_mult_less add_mult_less_add_mult ordertype_image_plus strict_mono_sets_def less_sets_def)
       have step: "Ex (\<lambda>(g,\<AA>',xn). \<Psi> n g \<AA> \<AA>' xn \<and> \<Phi> (Suc n) \<AA>' (x(n:=xn)))" if "\<Phi> n \<AA> x" for n \<AA> x
       proof -
         have \<AA>: "\<And>\<nu>. \<nu> \<in> elts \<beta> \<Longrightarrow> \<AA> \<nu> \<subseteq> elts (\<alpha>*\<beta>) \<and> tp (\<AA> \<nu>) = \<alpha>"
           and x: "x ` {..<n} \<subseteq> elts (\<alpha>*\<beta>)"
           and sub: "\<Union> (\<AA> ` elts \<beta>) \<subseteq> KI (Suc 0) (x ` {..<n})"
           and sm: "strict_mono_sets (elts \<beta>) \<AA>"
           using that by (auto simp: \<Phi>_def)
         have \<mu>\<beta>: "\<mu> ` {..n} \<subseteq> elts \<beta>" and \<AA>sub: "\<AA> (\<mu> n) \<subseteq> elts (\<alpha>*\<beta>)"
           by (auto simp: \<AA>)
         have \<AA>fun: "\<AA> \<in> elts \<beta> \<rightarrow> {X. X \<subseteq> elts (\<alpha>*\<beta>) \<and> tp X = \<alpha>}"
           by (simp add: \<AA>)
         then obtain xn g where xn: "xn \<in> \<AA> (\<mu> n)" and g: "g \<in> elts \<beta> \<rightarrow> elts \<beta>"
           and sm_g: "strict_mono_on g (elts \<beta>)" and g_\<mu>: "\<forall>\<nu> \<in> \<mu>`{..n}. g \<nu> = \<nu>"
           and g_\<alpha>: "\<forall>\<nu> \<in> elts \<beta>. \<alpha> \<le> tp (K 1 xn \<inter> \<AA> (g \<nu>))"
           using 10 [OF _ \<mu>\<beta> \<AA>sub _ \<AA>fun] by (auto simp: \<AA>)
         have tp1: "tp (K 1 xn \<inter> \<AA> (g \<nu>)) = \<alpha>" if "\<nu> \<in> elts \<beta>" for \<nu>
         proof (rule antisym)
           have "tp (K 1 xn \<inter> \<AA> (g \<nu>)) \<le> tp (\<AA> (g \<nu>))"
           proof (rule ordertype_VWF_mono)
             show "small (\<AA> (g \<nu>))"
               by (metis PiE \<AA> down g that)
           qed auto
           also have "\<dots> = \<alpha>"
             using \<AA> g that by force
           finally show "tp (K 1 xn \<inter> \<AA> (g \<nu>)) \<le> \<alpha>" .
         qed (use that g_\<alpha> in auto)
         have tp2: "tp (\<AA> (\<mu> n)) = \<alpha>"
           by (auto simp: \<AA>)
         obtain "small (\<AA> (\<mu> n))" "\<AA> (\<mu> n) \<subseteq> ON"
           by (meson \<AA>sub ord down elts_subset_ON subset_trans)
         then obtain A2 where A2: "tp A2 = \<alpha>" "A2 \<subseteq> K 1 xn \<inter> \<AA> (\<mu> n)" "{xn} \<lless> A2"
           using indecomposable_imp_Ex_less_sets [OF indec \<open>\<alpha> > 1\<close> tp2]
           by (metis \<mu>_in_\<beta> atMost_iff image_eqI inf_le2 le_refl xn tp1 g_\<mu>)
         then have A2_sub: "A2 \<subseteq> \<AA> (\<mu> n)" by simp
         let ?\<AA> = "\<lambda>\<nu>. if \<nu> = \<mu> n then A2 else K 1 xn \<inter> \<AA> (g \<nu>)"
         have [simp]: "({..<Suc n} \<inter> {x. x \<noteq> n}) = ({..<n})"
           by auto
         have "K (Suc 0) xn \<inter> (\<Union>x\<in>elts \<beta> \<inter> {\<nu>. \<nu> \<noteq> \<mu> n}. \<AA> (g x)) \<subseteq> KI (Suc 0) (x ` {..<n})"
           using sub g by (auto simp: KI_def)
         moreover have "A2 \<subseteq> KI (Suc 0) (x ` {..<n})" "A2 \<subseteq> elts (\<alpha>*\<beta>)"
           using \<AA>sub sub A2 by fastforce+
         moreover have "xn \<in> elts (\<alpha>*\<beta>)"
           using \<AA>sub xn by blast
         moreover have "strict_mono_sets (elts \<beta>) ?\<AA>"
           using sm sm_g g g_\<mu> 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 "\<Phi> (Suc n) ?\<AA> (x(n := xn))"
           using tp1 x A2 by (auto simp: \<Phi>_def K_def)
         with A2 show ?thesis
           by (rule_tac x="(g,?\<AA>,xn)" in exI) (simp add: \<Psi>_def g sm_g g_\<mu> xn)
       qed
       define G where "G \<equiv> \<lambda>n \<AA> x. @(g,\<AA>',x'). \<exists>xn. \<Psi> n g \<AA> \<AA>' xn \<and> x' = (x(n:=xn)) \<and> \<Phi> (Suc n) \<AA>' x'"
       have G\<Phi>: "(\<lambda>(g,\<AA>',x'). \<Phi> (Suc n) \<AA>' x') (G n \<AA> x)"
         and G\<Psi>: "(\<lambda>(g,\<AA>',x'). \<Psi> n g \<AA> \<AA>' (x' n)) (G n \<AA> x)"  if "\<Phi> n \<AA> x" for n \<AA> x
         using step [OF that] by (force simp: G_def dest: some_eq_imp)+
       define H where "H \<equiv> rec_nat (id,?\<AA>0,undefined) (\<lambda>n (g0,\<AA>,x0). G n \<AA> x0)"
       have H_Suc: "H (Suc n) = (case H n of (g0, xa, xb) \<Rightarrow> G n xa xb)" for n
         by (simp add: H_def)
       have "(\<lambda>(g,\<AA>,x). \<Phi> n \<AA> x) (H n)" for n
       proof (induction n)
         case 0 show ?case
           by (simp add: H_def base)
       next
         case (Suc n) then show ?case
           using G\<Phi> by (fastforce simp: H_Suc)
       qed
       then have H_imp_\<Phi>: "\<Phi> n \<AA> x" if "H n = (g,\<AA>,x)" for g \<AA> x n
         by (metis case_prodD that)
       then have H_imp_\<Psi>: "(\<lambda>(g,\<AA>',x'). let (g0,\<AA>,x) = H n in \<Psi> n g \<AA> \<AA>' (x' n)) (H (Suc n))" for n
         using G\<Psi> by (fastforce simp: H_Suc split: prod.split)
       define g where "g \<equiv> \<lambda>n. (\<lambda>(g,\<AA>,x). g) (H (Suc n))"
       have g: "g n \<in> elts \<beta> \<rightarrow> elts \<beta>" and sm_g: "strict_mono_on (g n) (elts \<beta>)"
         and 13: "\<And>i. i\<le>n \<Longrightarrow> g n (\<mu> i) = \<mu> i" for n
         using H_imp_\<Psi> [of n] by (auto simp: g_def \<Psi>_def)
       define \<AA> where "\<AA> \<equiv> \<lambda>n. (\<lambda>(g,\<AA>,x). \<AA>) (H n)"
       define x where "x \<equiv> \<lambda>n. (\<lambda>(g,\<AA>,x). x n) (H (Suc n))"
       have 14: "\<AA> (Suc n) \<nu> \<subseteq> K 1 (x n) \<inter> \<AA> n (g n \<nu>)" if "\<nu> \<in> elts \<beta>" for \<nu> n
         using H_imp_\<Psi> [of n] that by (force simp: \<Psi>_def \<AA>_def x_def g_def)
       then have x14: "\<AA> (Suc n) \<nu> \<subseteq> \<AA> n (g n \<nu>)" if "\<nu> \<in> elts \<beta>" for \<nu> n
         using that by blast
       have 15: "x n \<in> \<AA> n (\<mu> n)" and 16: "{x n} \<lless> (\<AA> (Suc n) (\<mu> n))" for n
         using H_imp_\<Psi> [of n] by (force simp: \<Psi>_def \<AA>_def x_def)+
       have \<AA>_\<alpha>\<beta>: "\<AA> n \<nu> \<subseteq> elts (\<alpha>*\<beta>)" if "\<nu> \<in> elts \<beta>" for \<nu> n
         using H_imp_\<Phi> [of n] that by (auto simp: \<Phi>_def \<AA>_def split: prod.split)
       have 12: "strict_mono_sets (elts \<beta>) (\<AA> n)" for n
         using H_imp_\<Phi> [of n] that by (auto simp: \<Phi>_def \<AA>_def split: prod.split)
       have tp_\<AA>: "tp (\<AA> n \<nu>) = \<alpha>" if "\<nu> \<in> elts \<beta>" for \<nu> n
         using H_imp_\<Phi> [of n] that by (auto simp: \<Phi>_def \<AA>_def split: prod.split)
       let ?Z = "range x"
       have S_dec: "\<Union> (\<AA> (m+k) ` elts \<beta>) \<subseteq> \<Union> (\<AA> m ` elts \<beta>)" for k m
         by (induction k) (use 14 g in \<open>fastforce+\<close>)
       have "x n \<in> K 1 (x m)" if "m<n" for m n
       proof -
         have "x n \<in> (\<Union>\<nu> \<in> elts \<beta>. \<AA> n \<nu>)"
           by (meson "15" UN_I \<mu>_in_\<beta>)
         also have "\<dots> \<subseteq> (\<Union>\<nu> \<in> elts \<beta>. \<AA> (Suc m) \<nu>)"
           using S_dec [of "Suc m"] less_iff_Suc_add that by auto
         also have "\<dots> \<subseteq> 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]\<^bsup>2\<^esup> \<subseteq> {1}"
         by (clarsimp simp: nsets_2_eq) (metis insert_commute less_linear)
       moreover have Z_sub: "?Z \<subseteq> elts (\<alpha>*\<beta>)"
         using "15" \<AA>_\<alpha>\<beta> \<mu>_in_\<beta> by blast
       moreover have "tp ?Z \<ge> \<omega> * \<beta>"
       proof -
         define \<gg> where "\<gg> \<equiv> \<lambda>i j x. wfrec (measure (\<lambda>k. j-k)) (\<lambda>\<gg> k. if k<j then g k (\<gg> (Suc k)) else x) i"
         have \<gg>: "\<gg> i j x = (if i<j then g i (\<gg> (Suc i) j x) else x)" for i j x
           by (simp add: \<gg>_def wfrec cut_apply)
         have 17: "\<gg> k j (\<mu> i) = \<mu> i" if "i \<le> k" for i j k
           using wf_measure [of "\<lambda>k. j-k"] that
           by (induction k rule: wf_induct_rule) (simp add: "13" \<gg> le_imp_less_Suc)
         have \<gg>_in_\<beta>: "\<gg> i j \<nu>  \<in> elts \<beta>" if "\<nu> \<in> elts \<beta>" for i j \<nu>
           using wf_measure [of "\<lambda>k. j-k"] that
         proof (induction i rule: wf_induct_rule)
           case (less i)
           with g show ?case by (force simp: \<gg> [of i])
         qed
         then have \<gg>_fun: "\<gg> i j \<in> elts \<beta> \<rightarrow> elts \<beta>" for i j
           by simp
         have sm_\<gg>: "strict_mono_on (\<gg> i j) (elts \<beta>)" for i j
           using wf_measure [of "\<lambda>k. j-k"]
         proof (induction i rule: wf_induct_rule)
           case (less i)
           with sm_g show ?case
             by (auto simp: \<gg> [of i] strict_mono_on_def \<gg>_in_\<beta>)
         qed
         have *: "\<AA> j (\<mu> j) \<subseteq> \<AA> i (\<gg> i j (\<mu> j))" if "i < j" for i j
           using wf_measure [of "\<lambda>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 \<gg>_in_\<beta> show ?case
             by (simp add: \<gg> [of i]) (metis 17 Suc_lessI \<mu>_in_\<beta> order_refl order_trans x14)
         qed
         have le: "\<gg> i j (\<mu> j) \<le> \<mu> i \<longleftrightarrow> \<mu> j \<le> \<mu> i" for i j
           using sm_\<gg> unfolding strict_mono_on_def
           by (metis "17" Ord_in_Ord Ord_linear2 \<mu>_in_\<beta> leD le_refl less_V_def \<open>Ord \<beta>\<close>)
         then have less: "\<gg> i j (\<mu> j) < \<mu> i \<longleftrightarrow> \<mu> j < \<mu> i" for i j
           by (metis (no_types, lifting) "17" \<mu>_in_\<beta> less_V_def order_refl sm_\<gg> strict_mono_on_def)
         have eq: "\<gg> i j (\<mu> j) = \<mu> i \<longleftrightarrow> \<mu> j = \<mu> i" for i j
           by (metis eq_refl le less less_le)
         have 18: "\<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n) \<longleftrightarrow> \<mu> m < \<mu> n" for m n
         proof (cases n m rule: linorder_cases)
           case less
           show ?thesis
           proof (intro iffI)
             assume "\<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)"
             moreover
             have "\<not> \<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)" if "\<mu> n = \<mu> m"
               by (metis "*" "15" eq less less_V_def less_sets_def less_sets_weaken2 that)
             moreover
             have "\<not> \<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)" if "\<mu> n < \<mu> m"
               using that 12 15 * [OF less]
               apply (clarsimp simp: less_sets_def strict_mono_sets_def)
               by (metis Ord_in_Ord Ord_linear2 \<gg>_in_\<beta> \<mu>_in_\<beta> \<open>Ord \<beta>\<close> le leD less_asym subsetD)
             ultimately show "\<mu> m < \<mu> n"
               by (meson Ord_in_Ord Ord_linear_lt \<mu>_in_\<beta> \<open>Ord \<beta>\<close>)
           next
             assume "\<mu> m < \<mu> n"
             then have "\<AA> n (\<gg> n m (\<mu> m)) \<lless> \<AA> n (\<mu> n)"
               by (metis "12" \<gg>_in_\<beta> \<mu>_in_\<beta> eq le less_V_def strict_mono_sets_def)
             then show "\<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)"
               by (meson *[OF less] less_sets_weaken1)
           qed
         next
           case equal
           with 15 show ?thesis by auto
         next
           case greater
           show ?thesis
           proof (intro iffI)
             assume "\<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)"
             moreover
             have "\<not> \<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)" if "\<mu> n = \<mu> m"
               by (metis "*" "15" disjnt_iff eq greater in_mono less_sets_imp_disjnt that)
             moreover
             have "\<not> \<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)" if "\<mu> n < \<mu> m"
               using that 12 15 * [OF greater]
               apply (clarsimp simp: less_sets_def strict_mono_sets_def)
               by (meson \<gg>_in_\<beta> \<mu>_in_\<beta> in_mono less less_asym)
             ultimately show "\<mu> m < \<mu> n"
               by (meson Ord_\<mu> Ord_linear_lt)
           next
             assume "\<mu> m < \<mu> n"
             then have "\<AA> m (\<mu> m) \<lless> (\<AA> m (\<gg> m n (\<mu> n)))"
               by (meson 12 Ord_in_Ord Ord_linear2 \<gg>_in_\<beta> \<mu>_in_\<beta> le leD ord(2) strict_mono_sets_def)
             then show "\<AA> m (\<mu> m) \<lless> \<AA> n (\<mu> n)"
               by (meson "*" greater less_sets_weaken2)
           qed
         qed
         have \<AA>_increasing_\<mu>: "\<AA> n (\<mu> n) \<subseteq> \<AA> m (\<mu> m)" if "m \<le> n" "\<mu> m = \<mu> n" for m n
           by (metis "*" "17" dual_order.order_iff_strict that)
         moreover have INF: "infinite {n. n \<ge> m \<and> \<mu> m = \<mu> n}" for m
         proof -
           have "infinite (range (\<lambda>n. q (\<mu> m, n)))"
             unfolding q_def
             using to_nat_on_infinite [OF co_\<beta>U inf_\<beta>U] finite_image_iff
             by (simp add: finite_image_iff inj_on_def)
           moreover have "(range (\<lambda>n. q (\<mu> m, n))) \<subseteq> {n. \<mu> m = \<mu> n}"
             using 11 [of "\<mu> m"] by auto
           ultimately have "infinite {n. \<mu> m = \<mu> n}"
             using finite_subset by auto
           then have "infinite ({n. \<mu> m = \<mu> n} - {..<m})"
             by simp
           then show ?thesis
             by (auto simp: finite_nat_set_iff_bounded Bex_def not_less)
         qed
         let ?eqv = "\<lambda>m. {n. m \<le> n \<and> \<mu> m = \<mu> n}"
         have sm_x: "strict_mono_on x (?eqv m)" for m
         proof (clarsimp simp: strict_mono_on_def)
           fix n p
           assume "m \<le> n" "\<mu> p = \<mu> n" "\<mu> m = \<mu> n" "n < p"
           with 16 [of n] show "x n < x p"
             by (simp add: less_sets_def) (metis "*" "15" "17" Suc_lessI le_SucI subsetD)
         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 \<equiv> \<lambda>m. ?Z \<inter> \<AA> m (\<mu> 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) \<ge> \<omega>" for m
         proof -
           have "x ` {n. m \<le> n \<and> \<mu> m = \<mu> n} \<subseteq> ZA m"
             unfolding ZA_def using "15" \<AA>_increasing_\<mu> by blast
           then have "infinite (ZA m)"
             using INF [of m] finite_image_iff [OF inj_x] by (meson finite_subset)
           then show ?thesis
             by (simp add: ordertype_infinite_ge_\<omega>)
         qed
         have "\<exists>f \<in> elts \<omega> \<rightarrow> ZA m. strict_mono_on f (elts \<omega>)" for m
         proof -
           obtain Z where "Z \<subseteq> ZA m" "tp Z = \<omega>"
             by (meson 19 Ord_\<omega> le_ordertype_obtains_subset small_ZA)
           moreover have "ZA m \<subseteq> ON"
             using Ord_in_Ord \<AA>_\<alpha>\<beta> \<mu>_in_\<beta> 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 \<phi> where \<phi>: "\<And>m. \<phi> m \<in> elts \<omega> \<rightarrow> ZA m"
           and sm_\<phi>: "\<And>m. strict_mono_on (\<phi> m) (elts \<omega>)"
           by metis
         have "Ex(\<lambda>(m,\<nu>). \<nu> \<in> elts \<beta> \<and> \<gamma> = \<omega> * \<nu> + ord_of_nat m)" if "\<gamma> \<in> elts (\<omega> * \<beta>)" for \<gamma>
           using that by (auto simp: mult [of \<omega> \<beta>] lift_def elts_\<omega>)
         then obtain split where split: "\<And>\<gamma>. \<gamma> \<in> elts (\<omega> * \<beta>) \<Longrightarrow>
              (\<lambda>(m,\<nu>). \<nu> \<in> elts \<beta> \<and> \<gamma> = \<omega> * \<nu> + ord_of_nat m)(split \<gamma>)"
           by meson
         have split_eq [simp]: "split (\<omega> * \<nu> + ord_of_nat m) = (m,\<nu>)" if "\<nu> \<in> elts \<beta>" for \<nu> m
         proof -
           have [simp]: "\<omega> * \<nu> + ord_of_nat m = \<omega> * \<xi> + ord_of_nat n \<longleftrightarrow> \<xi> = \<nu> \<and> n = m" if "\<xi> \<in> elts \<beta>" for \<xi> n
             by (metis Ord_\<omega> that Ord_mem_iff_less_TC mult_cancellation_lemma ord_of_nat_\<omega> ord_of_nat_inject)
           show ?thesis
             using split [of "\<omega>*\<nu> + m"] that by (auto simp: mult [of \<omega> \<beta>] lift_def cong: conj_cong)
         qed
         define \<pi> where "\<pi> \<equiv> \<lambda>\<gamma>. (\<lambda>(m,\<nu>). \<phi> (q(\<nu>,0)) m)(split \<gamma>)"
         have \<pi>_Pi: "\<pi> \<in> elts (\<omega> * \<beta>) \<rightarrow> (\<Union>m. ZA m)"
           using \<phi> by (fastforce simp: \<pi>_def mult [of \<omega> \<beta>] lift_def elts_\<omega>)
         moreover have "(\<Union>m. ZA m) \<subseteq> ON"
           unfolding ZA_def using \<AA>_\<alpha>\<beta> \<mu>_in_\<beta> elts_subset_ON by blast
         ultimately have Ord_\<pi>_Pi: "\<pi> \<in> elts (\<omega> * \<beta>) \<rightarrow> ON"
           by fastforce
         show "tp ?Z \<ge> \<omega> * \<beta>"
         proof -
           have \<dagger>: "(\<Union>m. ZA m) = ?Z"
             using "15" by (force simp: ZA_def)
           moreover
           have "tp (elts (\<omega> * \<beta>)) \<le> tp (\<Union>m. ZA m)"
           proof (rule ordertype_inc_le)
             show "\<pi> ` elts (\<omega> * \<beta>) \<subseteq> (\<Union>m. ZA m)"
               using \<pi>_Pi by blast
           next
             fix u v
             assume x: "u \<in> elts (\<omega> * \<beta>)" and y: "v \<in> elts (\<omega> * \<beta>)" and "(u,v) \<in> VWF"
             then have "u<v"
               by (meson Ord_\<omega> Ord_in_Ord Ord_mult VWF_iff_Ord_less ord(2))
             moreover
             obtain m \<nu> n \<xi> where ueq: "u = \<omega> * \<nu> + ord_of_nat m" and \<nu>: "\<nu> \<in> elts \<beta>"
               and veq: "v = \<omega> * \<xi> + ord_of_nat n" and \<xi>: "\<xi> \<in> elts \<beta>"
               using x y by (auto simp:  mult [of \<omega> \<beta>] lift_def elts_\<omega>)
             ultimately have "\<nu> \<le> \<xi>"
               by (meson Ord_\<omega> Ord_in_Ord Ord_linear2 \<open>Ord \<beta>\<close> add_mult_less_add_mult less_asym ord_of_nat_\<omega>)
             consider (eq) "\<nu> = \<xi>" | (lt) "\<nu> < \<xi>"
               using \<open>\<nu> \<le> \<xi>\<close> le_neq_trans by blast
             then have "\<pi> u < \<pi> v"
             proof cases
               case eq
               then have "m < n"
                 using ueq veq \<open>u<v\<close> by simp
               then have "\<phi> (q (\<xi>, 0)) m < \<phi> (q (\<xi>, 0)) n"
                 using sm_\<phi> strict_mono_onD by blast
               then show ?thesis
                 using eq ueq veq \<nu> \<open>m < n\<close> by (simp add: \<pi>_def)
             next
               case lt
               have "\<phi> (q(\<nu>,0)) m \<in> \<AA> (q(\<nu>,0)) (\<mu>(q(\<nu>,0)))" "\<phi> (q (\<xi>,0)) n \<in> \<AA> (q(\<xi>,0)) (\<mu>(q(\<xi>,0)))"
                 using \<phi> unfolding ZA_def by blast+
               then show ?thesis
                 using lt ueq veq \<nu> \<xi> 18 [of "q(\<nu>,0)" "q(\<xi>,0)"]
                 by (simp add: \<pi>_def less_sets_def)
             qed
             then show "(\<pi> u, \<pi> v) \<in> VWF"
               using \<pi>_Pi
               by (metis Ord_\<pi>_Pi PiE VWF_iff_Ord_less x y mem_Collect_eq)
           qed (use \<dagger> in auto)
           ultimately show ?thesis by simp
         qed
       qed
       then obtain Z where "Z \<subseteq> ?Z" "tp Z = \<omega> * \<beta>"
         by (meson Ord_\<omega> Ord_mult ord Z_sub down le_ordertype_obtains_subset)
       ultimately show False
         using iii [of Z] by (meson dual_order.trans image_mono nsets_mono)
     qed
     have False
       if 0: "\<forall>H. tp H = ord_of_nat (2*k) \<longrightarrow> H \<subseteq> elts (\<alpha>*\<beta>) \<longrightarrow> \<not> f ` [H]\<^bsup>2\<^esup> \<subseteq> {0}"
         and 1: "\<forall>H. tp H = min \<gamma> (\<omega> * \<beta>) \<longrightarrow> H \<subseteq> elts (\<alpha>*\<beta>) \<longrightarrow> \<not> f ` [H]\<^bsup>2\<^esup> \<subseteq> {1}"
     proof (cases "\<omega>*\<beta> \<le> \<gamma>")
       case True
       then have \<dagger>: "\<exists>H'\<subseteq>H. tp H' = \<omega> * \<beta>" if "tp H = \<gamma>" "small H" for H
         by (metis Ord_\<omega> Ord_\<omega>1 Ord_in_Ord Ord_mult \<beta> le_ordertype_obtains_subset that)
       have [simp]: "min \<gamma> (\<omega>*\<beta>) = \<omega>*\<beta>"
         by (simp add: min_absorb2 that True)
       then show ?thesis
         using * [OF 0] 1 True
         by simp (meson \<dagger> down image_mono nsets_mono subset_trans)
     next
       case False
       then have \<dagger>: "\<exists>H'\<subseteq>H. tp H' = \<gamma>" if "tp H = \<omega> * \<beta>" "small H" for H
         by (metis Ord_linear_le Ord_ordertype \<open>Ord \<gamma>\<close> le_ordertype_obtains_subset that)
       then have "\<gamma> \<le> \<omega>*\<beta>"
         by (meson Ord_\<omega> Ord_\<omega>1 Ord_in_Ord Ord_linear_le Ord_mult \<beta> \<open>Ord \<gamma>\<close> False)
       then have [simp]: "min \<gamma> (\<omega>*\<beta>) = \<gamma>"
         by (simp add: min_absorb1)
       then show ?thesis
         using * [OF 0] 1 False
         by simp (meson \<dagger> down image_mono nsets_mono subset_trans)
     qed
     then show "\<exists>i<Suc (Suc 0). \<exists>H\<subseteq>elts (\<alpha>*\<beta>). tp H = [ord_of_nat (2*k), min \<gamma> (\<omega>*\<beta>)] ! i \<and> f ` [H]\<^bsup>2\<^esup> \<subseteq> {i}"
       by force
   qed
 qed
 
 
 theorem Erdos_Milner:
   assumes \<nu>: "\<nu> \<in> elts \<omega>1"
   shows "partn_lst_VWF (\<omega>\<up>(1 + \<nu> * n)) [ord_of_nat (2^n), \<omega>\<up>(1+\<nu>)] 2"
 proof (induction n)
   case 0
   then show ?case
     using partn_lst_VWF_degenerate [of 1 2] by simp
 next
   case (Suc n)
   have "Ord \<nu>"
     using Ord_\<omega>1 Ord_in_Ord assms by blast
   have "1+\<nu> \<le> \<nu>+1"
     by (simp add: \<open>Ord \<nu>\<close> one_V_def plus_Ord_le)
   then have [simp]: "min (\<omega> \<up> (1 + \<nu>)) (\<omega> * \<omega> \<up> \<nu>) = \<omega> \<up> (1+\<nu>)"
     by (simp add: \<open>Ord \<nu>\<close> oexp_add min_def)
   have ind: "indecomposable (\<omega> \<up> (1 + \<nu> * ord_of_nat n))"
     by (simp add: \<open>Ord \<nu>\<close> indecomposable_\<omega>_power)
   show ?case
   proof (cases "n = 0")
     case True
     then show ?thesis
       using partn_lst_VWF_\<omega>_2 \<open>Ord \<nu>\<close> one_V_def by auto
   next
     case False
     then have "Suc 0 < 2 ^ n"
       using less_2_cases not_less_eq by fastforce
     then have "partn_lst_VWF (\<omega> \<up> (1 + \<nu> * n) * \<omega> \<up> \<nu>) [ord_of_nat (2 * 2 ^ n), \<omega> \<up> (1 + \<nu>)] 2"
       using Erdos_Milner_aux [OF Suc ind, where \<beta> = "\<omega>\<up>\<nu>"] \<open>Ord \<nu>\<close> \<nu>
       by (auto simp: countable_oexp)
     then show ?thesis
       using \<open>Ord \<nu>\<close> by (simp add: mult_succ mult.assoc oexp_add)
   qed
 qed
 
 
 corollary remark_3: "partn_lst_VWF (\<omega>\<up>(Suc(4*k))) [4, \<omega>\<up>(Suc(2*k))] 2"
   using Erdos_Milner [of "2*k" 2]
   apply (simp flip: ord_of_nat_mult ord_of_nat.simps)
   by (simp add: one_V_def)
 
 
 text \<open>Theorem 3.2 of Jean A. Larson, ibid.\<close>
 corollary Theorem_3_2:
   fixes k n::nat
   shows "partn_lst_VWF (\<omega>\<up>(n*k)) [\<omega>\<up>n, ord_of_nat k] 2"
 proof (cases "n=0 \<or> k=0")
   case True
   then show ?thesis
     by (auto intro: partn_lst_triv0 [where i=1] partn_lst_triv1 [where i=0])
 next
   case False
   then have "n > 0" "k > 0"
     by auto
   have PV: "partn_lst_VWF (\<omega> \<up> (1 + ord_of_nat (n-1) * ord_of_nat (k-1))) [ord_of_nat (2 ^ (k-1)), \<omega> \<up> (1 + ord_of_nat (n-1))] 2"
     using Erdos_Milner [of "ord_of_nat (n-1)" "k-1"] Ord_\<omega>1 Ord_mem_iff_lt less_imp_le by blast
   have "k+n \<le> Suc (Suc(k-1) * Suc(n-1))"
     by simp
   also have "\<dots> \<le> Suc (k * n)"
     using False by auto
   finally have "1 + (n - 1) * (k - 1) \<le> n*k"
     using False by (auto simp: algebra_simps)
   then have "(1 + ord_of_nat (n - 1) * ord_of_nat (k - 1)) \<le> ord_of_nat(n*k)"
     by (metis (mono_tags, lifting) One_nat_def one_V_def ord_of_nat.simps ord_of_nat_add ord_of_nat_mono_iff ord_of_nat_mult)
   then have x: "\<omega> \<up> (1 + ord_of_nat (n - 1) * ord_of_nat (k - 1)) \<le> \<omega>\<up>(n*k)"
     by (simp add: oexp_mono_le)
   then have "partn_lst_VWF (\<omega>\<up>(n*k)) [\<omega> \<up> (1 + ord_of_nat (n-1)), ord_of_nat (2 ^ (k-1))] 2"
     by (metis PV partn_lst_two_swap Partitions.partn_lst_greater_resource less_eq_V_def)
   then have "partn_lst_VWF (\<omega>\<up>(n*k)) [\<omega> \<up> n, ord_of_nat (2 ^ (k-1))] 2"
     using ord_of_minus_1 [OF \<open>n > 0\<close>] by (simp add: one_V_def)
   then show ?thesis
     using power_gt_expt [of 2 "k-1"]
     by (force simp: less_Suc_eq intro: partn_lst_less)
 qed
 
 end
diff --git a/thys/ZFC_in_HOL/Ordinal_Exp.thy b/thys/ZFC_in_HOL/Ordinal_Exp.thy
--- a/thys/ZFC_in_HOL/Ordinal_Exp.thy
+++ b/thys/ZFC_in_HOL/Ordinal_Exp.thy
@@ -1,589 +1,589 @@
 section \<open>Exponentiation of ordinals\<close>
 
 theory Ordinal_Exp
   imports Kirby
 
 begin
 
 text \<open>Source: Schlöder, Julian.  Ordinal Arithmetic; available online at
     \url{http://www.math.uni-bonn.de/ag/logik/teaching/2012WS/Set%20theory/oa.pdf}\<close>
 
 definition oexp :: "[V,V] \<Rightarrow> V" (infixr "\<up>" 80)
   where "oexp a b \<equiv> transrec (\<lambda>f x. if x=0 then 1
                                     else if Limit x then if a=0 then 0 else SUP \<xi> \<in> elts x. f \<xi>
-                                    else f (\<Squnion>(elts x)) * a) b"
+                                    else f (\<Squnion>(elts x)) * a)  b"
 
 text \<open>@{term "0\<up>\<omega> = 1"} if we don't make a special case for Limit ordinals and zero\<close>
 
 
 lemma oexp_0_right [simp]: "\<alpha>\<up>0 = 1"
   by (simp add: def_transrec [OF oexp_def])
 
 lemma oexp_succ [simp]: "Ord \<beta> \<Longrightarrow> \<alpha>\<up>(succ \<beta>) = \<alpha>\<up>\<beta> * \<alpha>"
   by (simp add: def_transrec [OF oexp_def])
 
 lemma oexp_Limit: "Limit \<beta> \<Longrightarrow> \<alpha>\<up>\<beta> = (if \<alpha>=0 then 0 else SUP \<xi> \<in> elts \<beta>. \<alpha>\<up>\<xi>)"
   by (auto simp: def_transrec [OF oexp_def, of _ \<beta>])
 
 lemma oexp_1_right [simp]: "\<alpha>\<up>1 = \<alpha>"
   using one_V_def oexp_succ by fastforce
 
 lemma oexp_1 [simp]: "Ord \<alpha> \<Longrightarrow> 1\<up>\<alpha> = 1"
   by (induction rule: Ord_induct3) (use Limit_def oexp_Limit in auto)
 
 lemma oexp_0 [simp]: "Ord \<alpha> \<Longrightarrow> 0\<up>\<alpha> = (if \<alpha> = 0 then 1 else 0)"
   by (induction rule: Ord_induct3) (use Limit_def oexp_Limit in auto)
 
 lemma oexp_eq_0_iff [simp]:
   assumes "Ord \<beta>" shows "\<alpha>\<up>\<beta> = 0 \<longleftrightarrow> \<alpha>=0 \<and> \<beta>\<noteq>0"
   using \<open>Ord \<beta>\<close>
 proof (induction rule: Ord_induct3)
   case (Limit \<mu>)
   then show ?case
     using Limit_def oexp_Limit by auto
 qed auto
 
 lemma oexp_gt_0_iff [simp]:
   assumes "Ord \<beta>" shows "\<alpha>\<up>\<beta> > 0 \<longleftrightarrow> \<alpha>>0 \<or> \<beta>=0"
   by (simp add: assms less_V_def)
 
 lemma ord_of_nat_oexp: "ord_of_nat (m^n) = ord_of_nat m\<up>ord_of_nat n"
 proof (induction n)
   case (Suc n)
   then show ?case
     by (simp add: mult.commute [of m]) (simp add: ord_of_nat_mult)
 qed auto
 
 lemma omega_closed_oexp [intro]:
   assumes "\<alpha> \<in> elts \<omega>" "\<beta> \<in> elts \<omega>" shows "\<alpha>\<up>\<beta> \<in> elts \<omega>"
 proof -
   obtain m n where "\<alpha> = ord_of_nat m" "\<beta> = ord_of_nat n"
     using assms elts_\<omega> by auto
   then have "\<alpha>\<up>\<beta> = ord_of_nat (m^n)"
     by (simp add: ord_of_nat_oexp)
   then show ?thesis
     by (simp add: \<omega>_def)
 qed
 
 
 lemma Ord_oexp [simp]:
   assumes "Ord \<alpha>" "Ord \<beta>" shows "Ord (\<alpha>\<up>\<beta>)"
   using \<open>Ord \<beta>\<close>
 proof (induction rule: Ord_induct3)
   case (Limit \<alpha>)
   then show ?case
     by (auto simp: oexp_Limit image_iff intro: Ord_Sup)
 qed (auto intro: Ord_mult assms)
 
 text \<open>Lemma 3.19\<close>
 lemma le_oexp:
   assumes "Ord \<alpha>" "Ord \<beta>" "\<beta> \<noteq> 0" shows "\<alpha> \<le> \<alpha>\<up>\<beta>"
   using \<open>Ord \<beta>\<close> \<open>\<beta> \<noteq> 0\<close>
 proof (induction rule: Ord_induct3)
   case (succ \<beta>)
   then show ?case
     by simp (metis \<open>Ord \<alpha>\<close> le_0 le_mult mult.left_neutral oexp_0_right order_refl order_trans)
 next
   case (Limit \<mu>)
   then show ?case
     by (metis Limit_def Limit_eq_Sup_self ZFC_in_HOL.Sup_upper eq_iff image_eqI image_ident oexp_1_right oexp_Limit replacement small_elts one_V_def)
 qed auto
 
 
 text \<open>Lemma 3.20\<close>
 lemma le_oexp':
   assumes "Ord \<alpha>" "1 < \<alpha>" "Ord \<beta>" shows "\<beta> \<le> \<alpha>\<up>\<beta>"
 proof (cases "\<beta> = 0")
   case True
   then show ?thesis
     by auto
 next
   case False
   show ?thesis
     using \<open>Ord \<beta>\<close>
   proof (induction rule: Ord_induct3)
     case 0
     then show ?case
       by auto
   next
     case (succ \<gamma>)
     then have "\<alpha>\<up>\<gamma> * 1 < \<alpha>\<up>\<gamma> * \<alpha>"
       using \<open>Ord \<alpha>\<close> \<open>1 < \<alpha>\<close>
       by (metis le_mult less_V_def mult.right_neutral mult_cancellation not_less_0 oexp_eq_0_iff succ.hyps)
     then have " \<gamma> < \<alpha>\<up>succ \<gamma>"
       using succ.IH succ.hyps by auto
     then show ?case
       using False \<open>Ord \<alpha>\<close> \<open>1 < \<alpha>\<close> succ
       by (metis Ord_mem_iff_lt Ord_oexp Ord_succ elts_succ insert_subset less_eq_V_def less_imp_le)
   next
     case (Limit \<mu>)
     with False \<open>1 < \<alpha>\<close> show ?case
       by (force simp: Limit_def oexp_Limit intro: elts_succ)
   qed
 qed
 
 
 lemma oexp_Limit_le:
   assumes "\<beta> < \<gamma>" "Limit \<gamma>" "Ord \<beta>" "\<alpha> > 0" shows "\<alpha>\<up>\<beta> \<le> \<alpha>\<up>\<gamma>"
 proof -
   have "Ord \<gamma>"
     using Limit_def assms(2) by blast
   with assms show ?thesis
     using Ord_mem_iff_lt ZFC_in_HOL.Sup_upper oexp_Limit by auto
 qed
 
 proposition oexp_less:
   assumes \<beta>: "\<beta> \<in> elts \<gamma>" and "Ord \<gamma>" and \<alpha>: "\<alpha> > 1" "Ord \<alpha>" shows "\<alpha>\<up>\<beta> < \<alpha>\<up>\<gamma>"
 proof -
   obtain "\<beta> < \<gamma>" "Ord \<beta>"
     using Ord_in_Ord OrdmemD assms by auto
   have gt0: "\<alpha>\<up>\<beta> > 0"
     using \<open>Ord \<beta>\<close> \<alpha> dual_order.order_iff_strict by auto
   show ?thesis
     using \<open>Ord \<gamma>\<close> \<beta>
   proof (induction rule: Ord_induct3)
     case 0
     then show ?case
       by auto
   next
     case (succ \<delta>)
     then consider "\<beta> = \<delta>" | "\<beta> < \<delta>"
       using OrdmemD elts_succ by blast
     then show ?case
     proof cases
       case 1
       then have "(\<alpha>\<up>\<beta>) * 1 < (\<alpha>\<up>\<delta>) * \<alpha>"
         using Ord_1 Ord_oexp \<alpha> gt0 mult_cancel_less_iff succ.hyps by metis
       then show ?thesis
         by (simp add: succ.hyps)
     next
       case 2
       then have "(\<alpha>\<up>\<delta>) * 1 < (\<alpha>\<up>\<delta>) * \<alpha>"
         by (meson Ord_1 Ord_mem_iff_lt Ord_oexp \<open>Ord \<beta>\<close> \<alpha> gt0 less_trans mult_cancel_less_iff succ)
       with 2 show ?thesis
         using Ord_mem_iff_lt \<open>Ord \<beta>\<close> succ by auto
     qed
   next
     case (Limit \<gamma>)
     then obtain "Ord \<gamma>" "succ \<beta> < \<gamma>"
       using Limit_def Ord_in_Ord OrdmemD assms by auto
     have "\<alpha>\<up>\<beta> = (\<alpha>\<up>\<beta>) * 1"
       by simp
     also have "\<dots> < (\<alpha>\<up>\<beta>) * \<alpha>"
       using Ord_oexp \<open>Ord \<beta>\<close> assms gt0 mult_cancel_less_iff by blast
     also have "\<dots> = \<alpha>\<up>succ \<beta>"
       by (simp add: \<open>Ord \<beta>\<close>)
     also have "\<dots> \<le> (SUP \<xi> \<in> elts \<gamma>. \<alpha>\<up>\<xi>)"
     proof -
       have "succ \<beta> \<in> elts \<gamma>"
         using Limit.hyps Limit.prems Limit_def by auto
       then show ?thesis
         by (simp add: ZFC_in_HOL.Sup_upper)
     qed
     finally
     have "\<alpha>\<up>\<beta> < (SUP \<xi> \<in> elts \<gamma>. \<alpha>\<up>\<xi>)" .
     then show ?case
       using Limit.hyps oexp_Limit \<open>\<alpha> > 1\<close> by auto
   qed
 qed
 
 corollary oexp_less_iff:
   assumes "\<alpha> > 0" "Ord \<alpha>" "Ord \<beta>" "Ord \<gamma>" shows "\<alpha>\<up>\<beta> < \<alpha>\<up>\<gamma> \<longleftrightarrow> \<beta> \<in> elts \<gamma> \<and> \<alpha> > 1"
 proof safe
   show "\<beta> \<in> elts \<gamma>" "1 < \<alpha>"
     if "\<alpha>\<up>\<beta> < \<alpha>\<up>\<gamma>"
   proof -
     show "\<alpha> > 1"
     proof (rule ccontr)
       assume "\<not> \<alpha> > 1"
       then consider "\<alpha>=0" | "\<alpha>=1"
         using \<open>Ord \<alpha>\<close> less_V_def mem_0_Ord by fastforce
       then show False
         by cases (use that \<open>\<alpha> > 0\<close> \<open>Ord \<beta>\<close> \<open>Ord \<gamma>\<close> in \<open>auto split: if_split_asm\<close>)
     qed
     show \<beta>: "\<beta> \<in> elts \<gamma>"
     proof (rule ccontr)
       assume "\<beta> \<notin> elts \<gamma>"
       then have "\<gamma> \<le> \<beta>"
         by (meson Ord_linear_le Ord_mem_iff_lt assms less_le_not_le)
       then consider "\<gamma> = \<beta>" | "\<gamma> < \<beta>"
         using less_V_def by blast
       then show False
       proof cases
         case 1
         then show ?thesis
           using that by blast
       next
         case 2
         with \<open>\<alpha> > 1\<close> have "\<alpha>\<up>\<gamma> < \<alpha>\<up>\<beta>"
           by (simp add: Ord_mem_iff_lt assms oexp_less)
         with that show ?thesis
           by auto
       qed
     qed
   qed
   show "\<alpha>\<up>\<beta> < \<alpha>\<up>\<gamma>" if "\<beta> \<in> elts \<gamma>" "1 < \<alpha>"
     using that by (simp add: assms oexp_less)
 qed
 
 lemma \<omega>_oexp_iff [simp]: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> \<omega>\<up>\<alpha> = \<omega>\<up>\<beta> \<longleftrightarrow> \<alpha>=\<beta>"
   by (metis Ord_\<omega> Ord_linear \<omega>_gt1 less_irrefl oexp_less)
 
 lemma Limit_oexp:
   assumes "Limit \<gamma>" "Ord \<alpha>" "\<alpha> > 1" shows "Limit (\<alpha>\<up>\<gamma>)"
   unfolding Limit_def
 proof safe
   show O\<alpha>\<gamma>: "Ord (\<alpha>\<up>\<gamma>)"
     using Limit_def Ord_oexp \<open>Limit \<gamma>\<close> assms(2) by blast
   show 0: "0 \<in> elts (\<alpha>\<up>\<gamma>)"
     using Limit_def oexp_Limit \<open>Limit \<gamma>\<close> \<open>\<alpha> > 1\<close> by fastforce
   have "Ord \<gamma>"
     using Limit_def \<open>Limit \<gamma>\<close> by blast
   fix x
   assume x: "x \<in> elts (\<alpha>\<up>\<gamma>)"
   with \<open>Limit \<gamma>\<close> \<open>\<alpha> > 1\<close>
   obtain \<beta> where "\<beta> < \<gamma>" "Ord \<beta>" "Ord x" and x\<beta>: "x \<in> elts (\<alpha>\<up>\<beta>)"
     apply (simp add: oexp_Limit split: if_split_asm)
     using Ord_in_Ord OrdmemD \<open>Ord \<gamma>\<close> O\<alpha>\<gamma> x by blast
   then have O\<alpha>\<beta>: "Ord (\<alpha>\<up>\<beta>)"
     using Ord_oexp assms(2) by blast
   have "\<beta> \<in> elts \<gamma>"
     by (simp add: Ord_mem_iff_lt \<open>Ord \<beta>\<close> \<open>Ord \<gamma>\<close> \<open>\<beta> < \<gamma>\<close>)
   moreover have "\<alpha> \<noteq> 0"
     using \<open>\<alpha> > 1\<close> by blast
   ultimately have \<alpha>\<beta>\<gamma>: "\<alpha>\<up>\<beta> \<le> \<alpha>\<up>\<gamma>"
     by (simp add: Sup_upper oexp_Limit \<open>Limit \<gamma>\<close>)
   have "succ x \<le> \<alpha>\<up>\<beta>"
     by (simp add: OrdmemD O\<alpha>\<beta> \<open>Ord x\<close> succ_le_iff x\<beta>)
   then consider "succ x < \<alpha>\<up>\<beta>" | "succ x = \<alpha>\<up>\<beta>"
     using le_neq_trans by blast
   then show "succ x \<in> elts (\<alpha>\<up>\<gamma>)"
   proof cases
     case 1
     with \<alpha>\<beta>\<gamma> show ?thesis
       using O\<alpha>\<beta> Ord_mem_iff_lt \<open>Ord x\<close> by blast
   next
     case 2
     then have "succ \<beta> < \<gamma>"
       using Limit_def OrdmemD \<open>\<beta> \<in> elts \<gamma>\<close> assms(1) by auto
     have ge1: "1 \<le> \<alpha>\<up>\<beta>"
       by (metis "2" Ord_0 \<open>Ord x\<close> le_0 le_succ_iff one_V_def)
     have "succ x < succ (\<alpha>\<up>\<beta>)"
       using "2" O\<alpha>\<beta> succ_le_iff by auto
     also have "\<dots> \<le> (\<alpha>\<up>\<beta>) + (\<alpha>\<up>\<beta>)"
       using ge1 by (simp add: succ_eq_add1)
     also have "\<dots> = (\<alpha>\<up>\<beta>) * succ (succ 0)"
       by (simp add: mult_succ)
     also have "\<dots> \<le> (\<alpha>\<up>\<beta>) * \<alpha>"
       using O\<alpha>\<beta> Ord_succ assms(2) assms(3) one_V_def succ_le_iff by auto
     also have "\<dots> = \<alpha>\<up>succ \<beta>"
       by (simp add: \<open>Ord \<beta>\<close>)
     also have "\<dots> \<le> \<alpha>\<up>\<gamma>"
       by (meson Limit_def \<open>\<beta> \<in> elts \<gamma>\<close> assms dual_order.order_iff_strict oexp_less)
   finally show ?thesis
     by (simp add: "2" O\<alpha>\<beta> O\<alpha>\<gamma> Ord_mem_iff_lt)
   qed
 qed
 
 
 
 lemma oexp_mono:
   assumes \<alpha>: "Ord \<alpha>" "\<alpha> \<noteq> 0" and \<beta>: "Ord \<beta>" "\<gamma> \<sqsubseteq> \<beta>" shows "\<alpha>\<up>\<gamma> \<le> \<alpha>\<up>\<beta>"
   using \<beta>
 proof (induction rule: Ord_induct3)
   case 0
   then show ?case
     by simp
 next
   case (succ \<beta>)
   with \<alpha> le_mult show ?case
     by (auto simp: le_TC_succ)
 next
   case (Limit \<mu>)
   then have "\<alpha>\<up>\<gamma> \<le> \<Squnion> ((\<up>) \<alpha> ` elts \<mu>)"
     using Limit.hyps Ord_less_TC_mem \<open>\<alpha> \<noteq> 0\<close> le_TC_def by (auto simp: oexp_Limit Limit_def)
   then show ?case
     using \<alpha> by (simp add: oexp_Limit Limit.hyps)
 qed
 
 lemma oexp_mono_le:
   assumes "\<gamma> \<le> \<beta>" "\<alpha> \<noteq> 0" "Ord \<alpha>" "Ord \<beta>" "Ord \<gamma>" shows "\<alpha>\<up>\<gamma> \<le> \<alpha>\<up>\<beta>"
   by (simp add: assms oexp_mono vle2 vle_iff_le_Ord)
 
 lemma oexp_sup:
   assumes "\<alpha> \<noteq> 0" "Ord \<alpha>" "Ord \<beta>" "Ord \<gamma>" shows "\<alpha>\<up>(\<beta> \<squnion> \<gamma>) = \<alpha>\<up>\<beta> \<squnion> \<alpha>\<up>\<gamma>"
   by (metis Ord_linear_le assms oexp_mono_le sup.absorb2 sup.orderE)
 
 lemma oexp_Sup:
   assumes \<alpha>: "\<alpha> \<noteq> 0" "Ord \<alpha>" and X: "X \<subseteq> ON" "small X" "X \<noteq> {}" shows "\<alpha>\<up>\<Squnion> X = \<Squnion> ((\<up>) \<alpha> ` X)"
 proof (rule order_antisym)
   show "\<Squnion> ((\<up>) \<alpha> ` X) \<le> \<alpha>\<up>\<Squnion> X"
     by (metis ON_imp_Ord Ord_Sup ZFC_in_HOL.Sup_upper assms cSUP_least oexp_mono_le)
 next
   have "Ord (Sup X)"
     using Ord_Sup X by auto
   then show "\<alpha>\<up>\<Squnion> X \<le> \<Squnion> ((\<up>) \<alpha> ` X)"
   proof (cases rule: Ord_cases)
     case 0
     then show ?thesis
       using X dual_order.antisym by fastforce
   next
     case (succ \<beta>)
     then show ?thesis
       using ZFC_in_HOL.Sup_upper X succ_in_Sup_Ord by auto
   next
     case limit
     show ?thesis
     proof (clarsimp simp: assms oexp_Limit limit)
       fix x y z
       assume x: "x \<in> elts (\<alpha> \<up> y)" and "z \<in> X" "y \<in> elts z"
       then have "\<alpha> \<up> y \<le> \<alpha> \<up> z"
         by (meson ON_imp_Ord Ord_in_Ord OrdmemD \<alpha> \<open>X \<subseteq> ON\<close> le_less oexp_mono_le)
       with x have "x \<in> elts (\<alpha> \<up> z)" by blast
       then show "\<exists>u\<in>X. x \<in> elts (\<alpha> \<up> u)"
         using \<open>z \<in> X\<close> by blast
     qed
   qed
 qed
 
 
 lemma omega_le_Limit:
   assumes "Limit \<mu>" shows "\<omega> \<le> \<mu>"
 proof
   fix \<rho>
   assume "\<rho> \<in> elts \<omega>"
   then obtain n where "\<rho> = ord_of_nat n"
     using elts_\<omega> by auto
   have "ord_of_nat n \<in> elts \<mu>"
     by (induction n) (use Limit_def assms in auto)
   then show "\<rho> \<in> elts \<mu>"
     using \<open>\<rho> = ord_of_nat n\<close> by auto
 qed
 
 lemma finite_omega_power [simp]:
   assumes "1 < n" "n \<in> elts \<omega>" shows "n\<up>\<omega> = \<omega>"
 proof (rule order_antisym)
   have "\<Squnion> ((\<up>) (ord_of_nat k) ` elts \<omega>) \<le> \<omega>" for k
   proof (induction k)
     case 0
     then show ?case
       by auto
   next
     case (Suc k)
     then show ?case
       by (metis Ord_\<omega> OrdmemD Sup_eq_0_iff ZFC_in_HOL.SUP_le_iff le_0 le_less omega_closed_oexp ord_of_nat_\<omega>)
   qed
   then show "n\<up>\<omega> \<le> \<omega>"
     using assms
     by (simp add: elts_\<omega> oexp_Limit) metis
   show "\<omega> \<le> n\<up>\<omega>"
     using Ord_in_Ord assms le_oexp' by blast
 qed
 
 
 proposition oexp_add:
   assumes "Ord \<alpha>" "Ord \<beta>" "Ord \<gamma>" shows "\<alpha>\<up>(\<beta> + \<gamma>) = \<alpha>\<up>\<beta> * \<alpha>\<up>\<gamma>"
 proof (cases \<open>\<alpha> = 0\<close>)
   case True
   then show ?thesis
     using assms by simp
 next
   case False
   show ?thesis
     using \<open>Ord \<gamma>\<close>
   proof (induction rule: Ord_induct3)
     case 0
     then show ?case
       by auto
   next
     case (succ \<xi>)
     then show ?case
       using \<open>Ord \<beta>\<close> by (auto simp: plus_V_succ_right mult.assoc)
   next
     case (Limit \<mu>)
     have "\<alpha>\<up>(\<beta> + (SUP \<xi>\<in>elts \<mu>. \<xi>)) = (SUP \<xi>\<in>elts (\<beta> + \<mu>). \<alpha>\<up>\<xi>)"
       by (simp add: Limit.hyps oexp_Limit assms False)
     also have "\<dots> = (SUP \<xi> \<in> {\<xi>. Ord \<xi> \<and> \<beta> + \<xi> < \<beta> + \<mu>}. \<alpha>\<up>(\<beta> + \<xi>))"
     proof (rule Sup_eq_Sup)
       show "(\<lambda>\<xi>. \<alpha>\<up>(\<beta> + \<xi>)) ` {\<xi>. Ord \<xi> \<and> \<beta> + \<xi> < \<beta> + \<mu>} \<subseteq> (\<up>) \<alpha> ` elts (\<beta> + \<mu>)"
         using Limit.hyps Limit_def Ord_mem_iff_lt imageI by blast
       fix x
       assume "x \<in> (\<up>) \<alpha> ` elts (\<beta> + \<mu>)"
       then obtain \<xi> where \<xi>: "\<xi> \<in> elts (\<beta> + \<mu>)" and x: "x = \<alpha>\<up>\<xi>"
         by auto
       have "\<exists>\<gamma>. Ord \<gamma> \<and> \<gamma> < \<mu> \<and> \<alpha>\<up>\<xi> \<le> \<alpha>\<up>(\<beta> + \<gamma>)"
       proof (rule mem_plus_V_E [OF \<xi>])
         assume "\<xi> \<in> elts \<beta>"
         then have "\<alpha>\<up>\<xi> \<le> \<alpha>\<up>\<beta>"
           by (meson arg_subset_TC assms False le_TC_def less_TC_def oexp_mono vsubsetD)
         with zero_less_Limit [OF \<open>Limit \<mu>\<close>]
         show "\<exists>\<gamma>. Ord \<gamma> \<and> \<gamma> < \<mu> \<and> \<alpha>\<up>\<xi> \<le> \<alpha>\<up>(\<beta> + \<gamma>)"
           by force
       next
         fix \<delta>
         assume "\<delta> \<in> elts \<mu>" and "\<xi> = \<beta> + \<delta>"
         have "Ord \<delta>"
           using Limit.hyps Limit_def Ord_in_Ord \<open>\<delta> \<in> elts \<mu>\<close> by blast
         moreover have "\<delta> < \<mu>"
           using Limit.hyps Limit_def OrdmemD \<open>\<delta> \<in> elts \<mu>\<close> by auto
         ultimately show "\<exists>\<gamma>. Ord \<gamma> \<and> \<gamma> < \<mu> \<and> \<alpha>\<up>\<xi> \<le> \<alpha>\<up>(\<beta> + \<gamma>)"
           using \<open>\<xi> = \<beta> + \<delta>\<close> by blast
       qed
       then show "\<exists>y\<in>(\<lambda>\<xi>. \<alpha>\<up>(\<beta> + \<xi>)) ` {\<xi>. Ord \<xi> \<and> \<beta> + \<xi> < \<beta> + \<mu>}. x \<le> y"
         using x by auto
     qed auto
     also have "\<dots> = (SUP \<xi>\<in>elts \<mu>. \<alpha>\<up>(\<beta> + \<xi>))"
       using \<open>Limit \<mu>\<close>
       by (simp add: Ord_Collect_lt Limit_def)
     also have "\<dots> = (SUP \<xi>\<in>elts \<mu>. \<alpha>\<up>\<beta> * \<alpha>\<up>\<xi>)"
       using Limit.IH by auto
     also have "\<dots> = \<alpha>\<up>\<beta> * \<alpha>\<up>(SUP \<xi>\<in>elts \<mu>. \<xi>)"
       using \<open>\<alpha> \<noteq> 0\<close> Limit.hyps
       by (simp add: image_image oexp_Limit mult_Sup_distrib)
     finally show ?case .
   qed
 qed
 
 proposition oexp_mult:
   assumes "Ord \<alpha>" "Ord \<beta>" "Ord \<gamma>" shows "\<alpha>\<up>(\<beta> * \<gamma>) = (\<alpha>\<up>\<beta>)\<up>\<gamma>"
 proof (cases "\<alpha> = 0 \<or> \<beta> = 0")
   case True
   then show ?thesis
     by (auto simp: \<open>Ord \<beta>\<close> \<open>Ord \<gamma>\<close>)
 next
   case False
   show ?thesis
     using \<open>Ord \<gamma>\<close>
   proof (induction rule: Ord_induct3)
     case 0
     then show ?case
       by auto
   next
     case succ
     then show ?case
       using assms by (auto simp: mult_succ oexp_add)
   next
     case (Limit \<mu>)
     have Lim: "Limit (\<Squnion> ((*) \<beta> ` elts \<mu>))"
       unfolding Limit_def
     proof (intro conjI allI impI)
       show "Ord (\<Squnion> ((*) \<beta> ` elts \<mu>))"
         using Limit.hyps Limit_def Ord_in_Ord \<open>Ord \<beta>\<close> by (auto intro: Ord_Sup)
       have "succ 0 \<in> elts \<mu>"
         using Limit.hyps Limit_def by blast
       then show "0 \<in> elts (\<Squnion> ((*) \<beta> ` elts \<mu>))"
         using False \<open>Ord \<beta>\<close> mem_0_Ord by force
       show "succ y \<in> elts (\<Squnion> ((*) \<beta> ` elts \<mu>))"
         if "y \<in> elts (\<Squnion> ((*) \<beta> ` elts \<mu>))" for y
         using that False Limit.hyps
         apply (clarsimp simp: Limit_def)
         by (metis Ord_in_Ord Ord_linear Ord_mem_iff_lt Ord_mult Ord_succ assms(2) less_V_def mult_cancellation mult_succ not_add_mem_right succ_le_iff succ_ne_self)
     qed
     have "\<alpha>\<up>(\<beta> * (SUP \<xi>\<in>elts \<mu>. \<xi>)) = \<alpha>\<up>\<Squnion> ((*) \<beta> ` elts \<mu>)"
       by (simp add: mult_Sup_distrib)
     also have "\<dots> = \<Squnion> (\<Union>x\<in>elts \<mu>. (\<up>) \<alpha> ` elts (\<beta> * x))"
       using False Lim oexp_Limit by fastforce
     also have "\<dots> = (SUP x\<in>elts \<mu>. \<alpha>\<up>(\<beta> * x))"
     proof (rule Sup_eq_Sup)
       show "(\<lambda>x. \<alpha>\<up>(\<beta> * x)) ` elts \<mu> \<subseteq> (\<Union>x\<in>elts \<mu>. (\<up>) \<alpha> ` elts (\<beta> * x))"
         using \<open>Ord \<alpha>\<close> \<open>Ord \<beta>\<close> False Limit
         apply clarsimp
         by (metis Limit_def elts_succ imageI insertI1 mem_0_Ord mult_add_mem_0)
       show "\<exists>y\<in>(\<lambda>x. \<alpha>\<up>(\<beta> * x)) ` elts \<mu>. x \<le> y"
         if "x \<in> (\<Union>x\<in>elts \<mu>. (\<up>) \<alpha> ` elts (\<beta> * x))" for x
         using that \<open>Ord \<alpha>\<close> \<open>Ord \<beta>\<close> False Limit
         by clarsimp (metis Limit_def Ord_in_Ord Ord_mult VWO_TC_le mem_imp_VWO oexp_mono)
     qed auto
     also have "\<dots> = \<Squnion> ((\<up>) (\<alpha>\<up>\<beta>) ` elts (SUP \<xi>\<in>elts \<mu>. \<xi>))"
       using Limit.IH Limit.hyps by auto
     also have "\<dots> = (\<alpha>\<up>\<beta>)\<up>(SUP \<xi>\<in>elts \<mu>. \<xi>)"
       using False Limit.hyps oexp_Limit \<open>Ord \<beta>\<close> by auto
     finally show ?case .
   qed
 qed
 
 lemma Limit_omega_oexp:
   assumes "Ord \<delta>" "\<delta> \<noteq> 0"
   shows "Limit (\<omega>\<up>\<delta>)"
   using assms
 proof (cases \<delta> rule: Ord_cases)
   case 0
   then show ?thesis
     using assms(2) by blast
 next
   case (succ l)
   have *: "succ \<beta> \<in> elts (\<omega>\<up>l * n + \<omega>\<up>l)"
     if n: "n \<in> elts \<omega>" and \<beta>: "\<beta> \<in> elts (\<omega>\<up>l * n)" for n \<beta>
   proof -
     obtain "Ord n" "Ord \<beta>"
       by (meson Ord_\<omega> Ord_in_Ord Ord_mult Ord_oexp \<beta> n succ(1))
     obtain oo: "Ord (\<omega>\<up>l)" "Ord (\<omega>\<up>l * n)"
       by (simp add: \<open>Ord n\<close> succ(1))
     moreover have f4: "\<beta> < \<omega>\<up>l * n"
       using oo Ord_mem_iff_lt \<open>Ord \<beta>\<close> \<open>\<beta> \<in> elts (\<omega>\<up>l * n)\<close> by blast
     moreover have f5: "Ord (succ \<beta>)"
       using \<open>Ord \<beta>\<close> by blast
     moreover have "\<omega>\<up>l \<noteq> 0"
       using oexp_eq_0_iff omega_nonzero succ(1) by blast
     ultimately show ?thesis
       by (metis add_less_cancel_left Ord_\<omega> Ord_add Ord_mem_iff_lt OrdmemD \<open>Ord \<beta>\<close> add.right_neutral dual_order.strict_trans2 oexp_gt_0_iff succ(1) succ_le_iff zero_in_omega)
   qed
   show ?thesis
     using succ
     apply (clarsimp simp: Limit_def mem_0_Ord)
     apply (simp add: mult_Limit)
     by (metis * mult_succ succ_in_omega)
 next
   case limit
   then show ?thesis
     by (metis Limit_oexp Ord_\<omega> OrdmemD one_V_def succ_in_omega zero_in_omega)
 qed
 
 lemma oexp_mult_commute:
   fixes j::nat
   assumes "Ord \<alpha>"
   shows "(\<alpha> \<up> j) * \<alpha> = \<alpha> * (\<alpha> \<up> j)"
 proof -
   have "(\<alpha> \<up> j) * \<alpha> = \<alpha> \<up> (1 + ord_of_nat j)"
     by (simp add: one_V_def)
   also have "... = \<alpha> * (\<alpha> \<up> j)"
     by (simp add: assms oexp_add)
   finally show ?thesis .
 qed
 
 lemma oexp_\<omega>_Limit: "Limit \<beta> \<Longrightarrow> \<omega>\<up>\<beta> = (SUP \<xi> \<in> elts \<beta>. \<omega>\<up>\<xi>)"
   by (simp add: oexp_Limit)
 
 lemma \<omega>_power_succ_gtr: "Ord \<alpha> \<Longrightarrow> \<omega> \<up> \<alpha> * ord_of_nat n < \<omega> \<up> succ \<alpha>"
   by (simp add: OrdmemD)
 
 lemma countable_oexp:
   assumes \<nu>: "\<alpha> \<in> elts \<omega>1" 
   shows "\<omega> \<up> \<alpha> \<in> elts \<omega>1"
 proof -
   have "Ord \<alpha>"
     using Ord_\<omega>1 Ord_in_Ord assms by blast
   then show ?thesis
     using assms
   proof (induction rule: Ord_induct3)
     case 0
     then show ?case
       by (simp add: Ord_mem_iff_lt)
   next
     case (succ \<alpha>)
     then have "countable (elts (\<omega> \<up> \<alpha> * \<omega>))"
       by (simp add: succ_in_Limit_iff countable_mult less_\<omega>1_imp_countable)
     then show ?case
       using Ord_mem_iff_lt countable_iff_less_\<omega>1 succ.hyps by auto
   next
     case (Limit \<alpha>)
     with Ord_\<omega>1 have "countable (\<Union>\<beta>\<in>elts \<alpha>. elts (\<omega> \<up> \<beta>))" "Ord (\<omega> \<up> \<Squnion> (elts \<alpha>))"
       by (force simp: Limit_def intro: Ord_trans less_\<omega>1_imp_countable)+
     then have "\<omega> \<up> \<Squnion> (elts \<alpha>) < \<omega>1"
       using Limit.hyps countable_iff_less_\<omega>1 oexp_Limit by fastforce
     then show ?case
       using Limit.hyps Limit_def Ord_mem_iff_lt by auto
   qed
 qed
 
 end
diff --git a/thys/ZFC_in_HOL/ZFC_Cardinals.thy b/thys/ZFC_in_HOL/ZFC_Cardinals.thy
--- a/thys/ZFC_in_HOL/ZFC_Cardinals.thy
+++ b/thys/ZFC_in_HOL/ZFC_Cardinals.thy
@@ -1,2526 +1,2541 @@
 section \<open>Cartesian products, Disjoint Sums, Ranks, Cardinals\<close>
 
 theory ZFC_Cardinals
   imports ZFC_in_HOL
 
 begin
 
 declare [[coercion_enabled]]
 declare [[coercion "ord_of_nat :: nat \<Rightarrow> V"]]
 
 subsection \<open>Ordered Pairs\<close>
 
 lemma singleton_eq_iff [iff]: "set {a} = set {b} \<longleftrightarrow> a=b"
   by simp
 
 lemma doubleton_eq_iff: "set {a,b} = set {c,d} \<longleftrightarrow> (a=c \<and> b=d) \<or> (a=d \<and> b=c)"
   by (simp add: Set.doubleton_eq_iff)
 
 definition vpair :: "V \<Rightarrow> V \<Rightarrow> V"
   where "vpair a b = set {set {a},set {a,b}}"
 
 definition vfst :: "V \<Rightarrow> V"
   where "vfst p \<equiv> THE x. \<exists>y. p = vpair x y"
 
 definition vsnd :: "V \<Rightarrow> V"
   where "vsnd p \<equiv> THE y. \<exists>x. p = vpair x y"
 
 definition vsplit :: "[[V, V] \<Rightarrow> 'a, V] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
   where "vsplit c \<equiv> \<lambda>p. c (vfst p) (vsnd p)"
 
 nonterminal Vs
 syntax (ASCII)
   "_Tuple"    :: "[V, Vs] \<Rightarrow> V"              ("<(_,/ _)>")
   "_hpattern" :: "[pttrn, patterns] \<Rightarrow> pttrn"   ("<_,/ _>")
 syntax
   ""          :: "V \<Rightarrow> Vs"                    ("_")
   "_Enum"     :: "[V, Vs] \<Rightarrow> Vs"             ("_,/ _")
   "_Tuple"    :: "[V, Vs] \<Rightarrow> V"              ("\<langle>(_,/ _)\<rangle>")
   "_hpattern" :: "[pttrn, patterns] \<Rightarrow> pttrn"   ("\<langle>_,/ _\<rangle>")
 translations
   "<x, y, z>"    \<rightleftharpoons> "<x, <y, z>>"
   "<x, y>"       \<rightleftharpoons> "CONST vpair x y"
   "<x, y, z>"    \<rightleftharpoons> "<x, <y, z>>"
   "\<lambda><x,y,zs>. b" \<rightleftharpoons> "CONST vsplit(\<lambda>x <y,zs>. b)"
   "\<lambda><x,y>. b"    \<rightleftharpoons> "CONST vsplit(\<lambda>x y. b)"
 
 
 lemma vpair_def': "vpair a b = set {set {a,a},set {a,b}}"
   by (simp add: vpair_def)
 
 lemma vpair_iff [simp]: "vpair a b = vpair a' b' \<longleftrightarrow> a=a' \<and> b=b'"
   unfolding vpair_def' doubleton_eq_iff by auto
 
 lemmas vpair_inject = vpair_iff [THEN iffD1, THEN conjE, elim!]
 
 lemma vfst_conv [simp]: "vfst \<langle>a,b\<rangle> = a"
   by (simp add: vfst_def)
 
 lemma vsnd_conv [simp]: "vsnd \<langle>a,b\<rangle> = b"
   by (simp add: vsnd_def)
 
 lemma vsplit [simp]: "vsplit c \<langle>a,b\<rangle> = c a b"
   by (simp add: vsplit_def)
 
 lemma vpair_neq_fst: "\<langle>a,b\<rangle> \<noteq> a"
   by (metis elts_of_set insertI1 mem_not_sym small_upair vpair_def')
 
 lemma vpair_neq_snd: "\<langle>a,b\<rangle> \<noteq> b"
   by (metis elts_of_set insertI1 mem_not_sym small_upair subsetD subset_insertI vpair_def')
 
 lemma vpair_nonzero [simp]: "\<langle>x,y\<rangle> \<noteq> 0"
   by (metis elts_0 elts_of_set empty_not_insert small_upair vpair_def)
 
 lemma zero_notin_vpair: "0 \<notin> elts \<langle>x,y\<rangle>"
   by (auto simp: vpair_def)
 
 lemma inj_on_vpair [simp]: "inj_on (\<lambda>(x, y). \<langle>x, y\<rangle>) A"
   by (auto simp: inj_on_def)
 
 
 subsection \<open>Generalized Cartesian product\<close>
 
 definition VSigma :: "V \<Rightarrow> (V \<Rightarrow> V) \<Rightarrow> V"
   where "VSigma A B \<equiv> set(\<Union>x \<in> elts A. \<Union>y \<in> elts (B x). {\<langle>x,y\<rangle>})"
 
 abbreviation vtimes where "vtimes A B \<equiv> VSigma A (\<lambda>x. B)"
 
 definition pairs :: "V \<Rightarrow> (V * V)set"
   where "pairs r \<equiv> {(x,y). \<langle>x,y\<rangle> \<in> elts r} "
 
 lemma pairs_iff_elts: "(x,y) \<in> pairs z \<longleftrightarrow> \<langle>x,y\<rangle> \<in> elts z"
   by (simp add: pairs_def)
 
 lemma VSigma_iff [simp]: "\<langle>a,b\<rangle> \<in> elts (VSigma A B) \<longleftrightarrow> a \<in> elts A \<and> b \<in> elts (B a)"
   by (auto simp: VSigma_def UNION_singleton_eq_range)
 
 lemma VSigmaI [intro!]: "\<lbrakk> a \<in> elts A;  b \<in> elts (B a)\<rbrakk>  \<Longrightarrow> \<langle>a,b\<rangle> \<in> elts (VSigma A B)"
   by simp
 
 lemmas VSigmaD1 = VSigma_iff [THEN iffD1, THEN conjunct1]
 lemmas VSigmaD2 = VSigma_iff [THEN iffD1, THEN conjunct2]
 
 text \<open>The general elimination rule\<close>
 lemma VSigmaE [elim!]:
   assumes "c \<in> elts (VSigma A B)"
   obtains x y where "x \<in> elts A" "y \<in> elts (B x)" "c=\<langle>x,y\<rangle>"
   using assms by (auto simp: VSigma_def split: if_split_asm)
 
 lemma VSigmaE2 [elim!]:
   assumes "\<langle>a,b\<rangle> \<in> elts (VSigma A B)" obtains "a \<in> elts A" and "b \<in> elts (B a)"
   using assms  by auto
 
 lemma VSigma_empty1 [simp]: "VSigma 0 B = 0"
   by auto
 
 lemma times_iff [simp]: "\<langle>a,b\<rangle> \<in> elts (vtimes A B) \<longleftrightarrow> a \<in> elts A \<and> b \<in> elts B"
   by simp
 
 lemma timesI [intro!]: "\<lbrakk>a \<in> elts A;  b \<in> elts B\<rbrakk>  \<Longrightarrow> \<langle>a,b\<rangle> \<in> elts (vtimes A B)"
   by simp
 
 lemma times_empty2 [simp]: "vtimes A 0 = 0"
   using elts_0 by blast
 
 lemma times_empty_iff: "VSigma A B = 0 \<longleftrightarrow> A=0 \<or> (\<forall>x \<in> elts A. B x = 0)"
   by (metis VSigmaE VSigmaI elts_0 empty_iff trad_foundation)
 
 lemma elts_VSigma: "elts (VSigma a b) = (\<lambda>(x,y). vpair x y) ` Sigma (elts a) (\<lambda>x. elts (b x))"
   by auto
 
 lemma small_Times [simp]:
   assumes "small A" "small B" 
   shows "small (A \<times> B)"
 proof -
   obtain f a g b where "inj_on f A" "inj_on g B" and f: "f ` A = elts a" and g: "g ` B = elts b"
     using assms by (auto simp: small_def)
   define h where "h \<equiv> \<lambda>(x,y). \<langle>f x, g y\<rangle>"
   show ?thesis
     unfolding small_def
   proof (intro exI conjI)
     show "inj_on h (A \<times> B)"
       using \<open>inj_on f A\<close> \<open>inj_on g B\<close> by (simp add: h_def inj_on_def)
     have "h ` (A \<times> B) = elts (vtimes a b)"
       using f g by (fastforce simp: h_def image_iff split: prod.split)
     then show "h ` (A \<times> B) \<in> range elts"
       by blast
   qed
 qed
 
 
 subsection \<open>Disjoint Sum\<close>
 
 definition vsum :: "V \<Rightarrow> V \<Rightarrow> V" (infixl "\<Uplus>" 65) where
  "A \<Uplus> B \<equiv> (VSigma (set {0}) (\<lambda>x. A)) \<squnion> (VSigma (set {1}) (\<lambda>x. B))"
 
 definition Inl :: "V\<Rightarrow>V" where
      "Inl a \<equiv> \<langle>0,a\<rangle>"
 
 definition Inr :: "V\<Rightarrow>V" where
      "Inr b \<equiv> \<langle>1,b\<rangle>"
 
 lemmas sum_defs = vsum_def Inl_def Inr_def
 
 lemma Inl_nonzero [simp]:"Inl x \<noteq> 0"
   by (metis Inl_def vpair_nonzero)
 
 lemma Inr_nonzero [simp]:"Inr x \<noteq> 0"
   by (metis Inr_def vpair_nonzero)
 
 subsubsection\<open>Equivalences for the injections and an elimination rule\<close>
 
 lemma Inl_in_sum_iff [iff]: "Inl a \<in> elts (A \<Uplus> B) \<longleftrightarrow> a \<in> elts A"
   by (auto simp: sum_defs)
 
 lemma Inr_in_sum_iff [iff]: "Inr b \<in> elts (A \<Uplus> B) \<longleftrightarrow> b \<in> elts B"
   by (auto simp: sum_defs)
 
 lemma sumE [elim!]:
   assumes u: "u \<in> elts (A \<Uplus> B)"
   obtains x where "x \<in> elts A" "u=Inl x" | y where "y \<in> elts B" "u=Inr y" using u
   by (auto simp: sum_defs)
 
 subsubsection \<open>Injection and freeness equivalences, for rewriting\<close>
 
 lemma Inl_iff [iff]: "Inl a=Inl b \<longleftrightarrow> a=b"
   by (simp add: sum_defs)
 
 lemma Inr_iff [iff]: "Inr a=Inr b \<longleftrightarrow> a=b"
   by (simp add: sum_defs)
 
 lemma inj_on_Inl [simp]: "inj_on Inl A"
   by (simp add: inj_on_def)
 
 lemma inj_on_Inr [simp]: "inj_on Inr A"
   by (simp add: inj_on_def)
 
 lemma Inl_Inr_iff [iff]: "Inl a=Inr b \<longleftrightarrow> False"
   by (simp add: sum_defs)
 
 lemma Inr_Inl_iff [iff]: "Inr b=Inl a \<longleftrightarrow> False"
   by (simp add: sum_defs)
 
 lemma sum_empty [simp]: "0 \<Uplus> 0 = 0"
   by auto
 
 lemma elts_vsum: "elts (a \<Uplus> b) = Inl ` (elts a) \<union> Inr ` (elts b)"
   by auto
 
 lemma sum_iff: "u \<in> elts (A \<Uplus> B) \<longleftrightarrow> (\<exists>x. x \<in> elts A \<and> u=Inl x) \<or> (\<exists>y. y \<in> elts B \<and> u=Inr y)"
   by blast
 
 lemma sum_subset_iff: "A\<Uplus>B \<le> C\<Uplus>D \<longleftrightarrow> A\<le>C \<and> B\<le>D"
   by (auto simp: less_eq_V_def)
 
 lemma sum_equal_iff:
   fixes A :: V shows "A\<Uplus>B = C\<Uplus>D \<longleftrightarrow> A=C \<and> B=D"
   by (simp add: eq_iff sum_subset_iff)
 
 definition is_sum :: "V \<Rightarrow> bool"
   where "is_sum z = (\<exists>x. z = Inl x \<or> z = Inr x)"
 
 definition sum_case  :: "(V \<Rightarrow> 'a) \<Rightarrow> (V \<Rightarrow> 'a) \<Rightarrow> V \<Rightarrow> 'a"
   where
   "sum_case f g a \<equiv>
     THE z. (\<forall>x. a = Inl x \<longrightarrow> z = f x) \<and> (\<forall>y. a = Inr y \<longrightarrow> z = g y) \<and> (\<not> is_sum a \<longrightarrow> z = undefined)"
 
 lemma sum_case_Inl [simp]: "sum_case f g (Inl x) = f x"
   by (simp add: sum_case_def is_sum_def)
 
 lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"
   by (simp add: sum_case_def is_sum_def)
 
 lemma sum_case_non [simp]: "\<not> is_sum a \<Longrightarrow> sum_case f g a = undefined"
   by (simp add: sum_case_def is_sum_def)
 
 lemma is_sum_cases: "(\<exists>x. z = Inl x \<or> z = Inr x) \<or> \<not> is_sum z"
   by (auto simp: is_sum_def)
 
 lemma sum_case_split:
   "P (sum_case f g a) \<longleftrightarrow> (\<forall>x. a = Inl x \<longrightarrow> P(f x)) \<and> (\<forall>y. a = Inr y \<longrightarrow> P(g y)) \<and> (\<not> is_sum a \<longrightarrow> P undefined)"
   by (cases "is_sum a") (auto simp: is_sum_def)
 
 lemma sum_case_split_asm:
   "P (sum_case f g a) \<longleftrightarrow> \<not> ((\<exists>x. a = Inl x \<and> \<not> P(f x)) \<or> (\<exists>y. a = Inr y \<and> \<not> P(g y)) \<or> (\<not> is_sum a \<and> \<not> P undefined))"
   by (auto simp: sum_case_split)
 
 subsubsection \<open>Applications of disjoint sums and pairs: general union theorems for small sets\<close>
 
 lemma small_Un:
   assumes X: "small X" and Y: "small Y"
   shows "small (X \<union> Y)"
 proof -
   obtain f g :: "'a\<Rightarrow>V" where f: "inj_on f X" and g: "inj_on g Y" 
     by (meson assms small_def)
   define h where "h \<equiv> \<lambda>z. if z \<in> X then Inl (f z) else Inr (g z)"
   show ?thesis
     unfolding small_def
   proof (intro exI conjI)
     show "inj_on h (X \<union> Y)"
       using f g by (auto simp add: inj_on_def h_def)
     show "h ` (X \<union> Y) \<in> range elts"
       by (metis X Y image_Un replacement small_iff_range small_sup_iff)
   qed
 qed
 
 lemma small_UN [simp,intro]:
   assumes X: "small X" and B: "\<And>x. x \<in> X \<Longrightarrow> small (B x)"
   shows "small (\<Union>x\<in>X. B x)"
 proof -
   obtain f :: "'a\<Rightarrow>V" where f: "inj_on f X" 
     by (meson assms small_def)
   have "\<exists>g. inj_on g (B x) \<and> g ` (B x) \<in> range elts" if "x \<in> X" for x
     using B small_def that by auto
   then obtain g::"'a \<Rightarrow> 'b \<Rightarrow> V" where g: "\<And>x. x \<in> X \<Longrightarrow> inj_on (g x) (B x)" 
     by metis
   define \<phi> where "\<phi> \<equiv> \<lambda>y. @x. x \<in> X \<and> y \<in> B x"
   have \<phi>: "\<phi> y \<in> X \<and> y \<in> B (\<phi> y)" if "y \<in> (\<Union>x\<in>X. B x)" for y
     unfolding \<phi>_def by (metis (mono_tags, lifting) UN_E someI that)
   define h where "h \<equiv> \<lambda>y. \<langle>f (\<phi> y), g (\<phi> y) y\<rangle>"
   show ?thesis
     unfolding small_def
   proof (intro exI conjI)
     show "inj_on h (\<Union> (B ` X))"
       using f g \<phi> unfolding h_def inj_on_def by (metis vpair_inject)
   have "small (h ` \<Union> (B ` X))"
     by (simp add: B X image_UN)
   then show "h ` \<Union> (B ` X) \<in> range elts"
     using small_iff_range by blast
   qed
 qed
 
 lemma small_Union [simp,intro]:
   assumes "\<A> \<subseteq> Collect small" "small \<A>"
   shows "small (\<Union> \<A>)"
   using small_UN [of \<A> "\<lambda>x. x"] assms by (simp add: subset_iff)
 
 subsection\<open>Generalised function space and lambda\<close>
 
 definition VLambda :: "V \<Rightarrow> (V \<Rightarrow> V) \<Rightarrow> V"
   where "VLambda A b \<equiv> set ((\<lambda>x. \<langle>x,b x\<rangle>) ` elts A)"
 
 definition app :: "[V,V] \<Rightarrow> V"
   where "app f x \<equiv> THE y. \<langle>x,y\<rangle> \<in> elts f"
 
 lemma beta [simp]:
   assumes "x \<in> elts A"
   shows "app (VLambda A b) x = b x"
   using assms by (auto simp: VLambda_def app_def)
 
 definition VPi :: "V \<Rightarrow> (V \<Rightarrow> V) \<Rightarrow> V"
   where "VPi A B \<equiv> set {f \<in> elts (VPow(VSigma A B)). elts A \<le> Domain (pairs f) \<and> single_valued (pairs f)}"
 
 lemma VPi_I:
   assumes "\<And>x. x \<in> elts A \<Longrightarrow> b x \<in> elts (B x)"
   shows "VLambda A b \<in> elts (VPi A B)"
   proof (clarsimp simp: VPi_def, intro conjI impI)
   show "VLambda A b \<le> VSigma A B"
     by (auto simp: assms VLambda_def split: if_split_asm)
   show "elts A \<subseteq> Domain (pairs (VLambda A b))"
     by (force simp: VLambda_def pairs_iff_elts)
   show "single_valued (pairs (VLambda A b))"
     by (auto simp: VLambda_def single_valued_def pairs_iff_elts)
   show "small {f. f \<le> VSigma A B \<and> elts A \<subseteq> Domain (pairs f) \<and> single_valued (pairs f)}"
     by (metis (mono_tags, lifting) down VPow_iff mem_Collect_eq subsetI)
 qed
 
 lemma apply_pair:
   assumes f: "f \<in> elts (VPi A B)" and x: "x \<in> elts A"
   shows "\<langle>x, app f x\<rangle> \<in> elts f"
 proof -
   have "x \<in> Domain (pairs f)"
     by (metis (no_types, lifting) VPi_def assms elts_of_set empty_iff mem_Collect_eq subsetD)
   then obtain y where y: "\<langle>x,y\<rangle> \<in> elts f"
     using pairs_iff_elts by auto
   show ?thesis
     unfolding app_def
   proof (rule theI)
     show "\<langle>x, y\<rangle> \<in> elts f"
       by (rule y)
     show "z = y" if "\<langle>x, z\<rangle> \<in> elts f" for z
       using f unfolding VPi_def
       by (metis (mono_tags, lifting) that elts_of_set empty_iff mem_Collect_eq pairs_iff_elts single_valued_def y)
   qed
 qed
 
 lemma VPi_D:
   assumes f: "f \<in> elts (VPi A B)" and x: "x \<in> elts A"
   shows "app f x \<in> elts (B x)"
 proof -
   have "f \<le> VSigma A B"
     by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq)
   then show ?thesis
     using apply_pair [OF assms] by blast
 qed
 
 lemma VPi_memberD:
   assumes f: "f \<in> elts (VPi A B)" and p: "p \<in> elts f"
   obtains x where "x \<in> elts A" "p = \<langle>x, app f x\<rangle>"
 proof -
   have "f \<le> VSigma A B"
     by (metis (no_types, lifting) VPi_def elts_of_set empty_iff f VPow_iff mem_Collect_eq)
   then obtain x y where "p = \<langle>x,y\<rangle>" "x \<in> elts A"
     using p by blast
   then have "y = app f x"
     by (metis (no_types, lifting) VPi_def apply_pair elts_of_set equals0D f mem_Collect_eq p pairs_iff_elts single_valuedD)
   then show thesis
     using \<open>p = \<langle>x, y\<rangle>\<close> \<open>x \<in> elts A\<close> that by blast
 qed
 
 lemma fun_ext:
   assumes "f \<in> elts (VPi A B)" "g \<in> elts (VPi A B)" "\<And>x. x \<in> elts A \<Longrightarrow> app f x = app g x"
   shows "f = g"
   by (metis VPi_memberD V_equalityI apply_pair assms)
 
 lemma eta[simp]:
   assumes "f \<in> elts (VPi A B)"
   shows "VLambda A ((app)f) = f"
   proof (rule fun_ext [OF _ assms])
   show "VLambda A (app f) \<in> elts (VPi A B)"
     using VPi_D VPi_I assms by auto
 qed auto
 
 
 lemma fst_pairs_VLambda: "fst ` pairs (VLambda A f) = elts A"
   by (force simp: VLambda_def pairs_def)
 
 lemma snd_pairs_VLambda: "snd ` pairs (VLambda A f) = f ` elts A"
   by (force simp: VLambda_def pairs_def)
 
 lemma VLambda_eq_D1: "VLambda A f = VLambda B g \<Longrightarrow> A = B"
   by (metis ZFC_in_HOL.ext fst_pairs_VLambda)
 
 lemma VLambda_eq_D2: "\<lbrakk>VLambda A f = VLambda A g; x \<in> elts A\<rbrakk> \<Longrightarrow> f x = g x"
   by (metis beta)
 
 
 subsection\<open>Transitive closure of a set\<close>
 
 definition TC :: "V\<Rightarrow>V"
   where "TC \<equiv> transrec (\<lambda>f x. x \<squnion> \<Squnion> (f ` elts x))"
 
 lemma TC: "TC a = a \<squnion> \<Squnion> (TC ` elts a)"
   by (metis (no_types, lifting) SUP_cong TC_def restrict_apply' transrec)
 
 lemma TC_0 [simp]: "TC 0 = 0"
   by (metis TC ZFC_in_HOL.Sup_empty elts_0 image_is_empty sup_V_0_left)
 
 lemma arg_subset_TC: "a \<le> TC a"
   by (metis (no_types) TC sup_ge1)
 
 lemma Transset_TC: "Transset(TC a)"
 proof (induction a rule: eps_induct)
   case (step x)
   have 1: "v \<in> elts (TC x)" if "v \<in> elts u" "u \<in> elts x" for u v
     using that unfolding TC [of x]
     using arg_subset_TC by fastforce
   have 2: "v \<in> elts (TC x)" if "v \<in> elts u" "\<exists>x\<in>elts x. u \<in> elts (TC x)" for u v
     using that step unfolding TC [of x] Transset_def by auto
   show ?case
     unfolding Transset_def
     by (subst TC) (force intro: 1 2)
 qed
 
 lemma TC_least: "\<lbrakk>Transset x;  a\<le>x\<rbrakk> \<Longrightarrow> TC a \<le> x"
 proof (induction a rule: eps_induct)
   case (step y)
   show ?case
   proof (cases "y=0")
     case True
     then show ?thesis
       by auto
   next
     case False
     have "\<Squnion> (TC ` elts y) \<le> x"
     proof (rule cSup_least)
       show "TC ` elts y \<noteq> {}"
         using False by auto
       show "z \<le> x" if "z \<in> TC ` elts y" for z
         using that by (metis Transset_def image_iff step.IH step.prems vsubsetD)
     qed
     then show ?thesis
       by (simp add: step TC [of y])
   qed
 qed
 
 definition less_TC (infix "\<sqsubset>" 50)
   where "x \<sqsubset> y \<equiv> x \<in> elts (TC y)"
 
 definition le_TC (infix "\<sqsubseteq>" 50)
   where "x \<sqsubseteq> y \<equiv> x \<sqsubset> y \<or> x=y"
 
 lemma less_TC_imp_not_le: "x \<sqsubset> a \<Longrightarrow> \<not> a \<le> x"
 proof (induction a arbitrary: x rule: eps_induct)
   case (step a)
   then show ?case
     unfolding TC[of a] less_TC_def
     using Transset_TC Transset_def by force
 qed
 
 lemma non_TC_less_0 [iff]: "\<not> (x \<sqsubset> 0)"
   using less_TC_imp_not_le by blast
 
 lemma less_TC_iff: "x \<sqsubset> y \<longleftrightarrow> (\<exists>z \<in> elts y. x \<sqsubseteq> z)"
   by (auto simp: less_TC_def le_TC_def TC [of y])
 
 lemma nonzero_less_TC: "x \<noteq> 0 \<Longrightarrow> 0 \<sqsubset> x"
   by (metis eps_induct le_TC_def less_TC_iff trad_foundation)
 
 lemma less_irrefl_TC [simp]: "\<not> x \<sqsubset> x"
   using less_TC_imp_not_le by blast
 
 lemma less_asym_TC: "\<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> False"
   by (metis TC_least Transset_TC Transset_def antisym_conv less_TC_def less_TC_imp_not_le order_refl)
 
 lemma le_antisym_TC: "\<lbrakk>x \<sqsubset> y; y \<sqsubset> x\<rbrakk> \<Longrightarrow> x = y"
   using less_asym_TC by blast
 
 lemma less_imp_le_TC [iff]: "x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y"
   by (simp add: le_TC_def)
 
 lemma le_TC_refl [iff]: "x \<sqsubseteq> x"
   by (simp add: le_TC_def)
 
 lemma less_TC_trans [trans]: "\<lbrakk>x \<sqsubset> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z"
   by (meson TC_least Transset_TC Transset_def less_TC_def less_eq_V_def subsetD)
 
 lemma less_le_TC_trans [trans]: "\<lbrakk>x \<sqsubset> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z"
   using le_TC_def less_TC_trans by blast
 
 lemma le_less_TC_trans [trans]: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubset> z\<rbrakk> \<Longrightarrow> x \<sqsubset> z"
   using le_TC_def less_TC_trans by blast
 
 lemma le_TC_trans [trans]: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
   using le_TC_def le_less_TC_trans by blast
 
 lemma TC_sup_distrib: "TC (x \<squnion> y) = TC x \<squnion> TC y"
   by (simp add: Sup_Un_distrib TC [of "x \<squnion> y"] TC [of x] TC [of y] image_Un sup.assoc sup_left_commute)
 
 lemma TC_Sup_distrib:
   assumes "small X" shows "TC (\<Squnion>X) = \<Squnion>(TC ` X)"
 proof -
   have "\<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x) \<le> \<Squnion> (TC ` X)"
     using assms
     apply (auto simp: Sup_le_iff)
     using arg_subset_TC apply blast
     by (metis TC_least Transset_TC Transset_def arg_subset_TC vsubsetD)
   moreover have "\<Squnion> (TC ` X) \<le> \<Squnion> X \<squnion> \<Squnion> (\<Union>x\<in>X. TC ` elts x)"
   proof (clarsimp simp add: Sup_le_iff assms)
     show "\<exists>x\<in>X. y \<in> elts x"
       if "x \<in> X" "y \<in> elts (TC x)" "\<forall>x\<in>X. \<forall>u\<in>elts x. y \<notin> elts (TC u)" for x y
       using that by (auto simp: TC [of x])
   qed
   ultimately show ?thesis
     using Sup_Un_distrib TC [of "\<Squnion>X"] image_Union assms
     by (simp add: image_Union inf_sup_aci(5) sup.absorb_iff2)
 qed
 
 lemma TC': "TC x = x \<squnion> TC (\<Squnion> (elts x))"
   by (simp add: TC [of x] TC_Sup_distrib)
 
 lemma TC_eq_0_iff [simp]: "TC x = 0 \<longleftrightarrow> x=0"
   using arg_subset_TC by fastforce
 
 text\<open>A distinctive induction principle\<close>
 lemma TC_induct_down_lemma:
   assumes ab: "a \<sqsubset> b" and base: "b \<le> d"
       and step: "\<And>y z. \<lbrakk>y \<sqsubset> b; y \<in> elts d; z \<in> elts y\<rbrakk> \<Longrightarrow> z \<in> elts d"
     shows "a \<in> elts d"
 proof -
   have "Transset (TC b \<sqinter> d)"
     using Transset_TC
     unfolding Transset_def
     by (metis inf.bounded_iff less_TC_def less_eq_V_def local.step subsetI vsubsetD) 
   moreover have "b \<le> TC b \<sqinter> d"
     by (simp add: arg_subset_TC base)
   ultimately show ?thesis
     using TC_least [THEN vsubsetD] ab unfolding less_TC_def
     by (meson TC_least le_inf_iff vsubsetD)
 qed
 
 lemma TC_induct_down [consumes 1, case_names base step small]:
   assumes "a \<sqsubset> b"
     and "\<And>y. y \<in> elts b \<Longrightarrow> P y"
     and "\<And>y z. \<lbrakk>y \<sqsubset> b; P y; z \<in> elts y\<rbrakk> \<Longrightarrow> P z"
     and "small (Collect P)"
   shows "P a"
   using TC_induct_down_lemma [of a b "set (Collect P)"] assms
   by (metis elts_of_set mem_Collect_eq vsubsetI)
 
 subsection\<open>Rank of a set\<close>
 
 definition rank :: "V\<Rightarrow>V"
   where "rank a \<equiv> transrec (\<lambda>f x. set (\<Union>y\<in>elts x. elts (succ(f y)))) a"
 
 lemma rank: "rank a = set(\<Union>y \<in> elts a. elts (succ(rank y)))"
   by (subst rank_def [THEN def_transrec], simp)
 
 lemma rank_Sup: "rank a = \<Squnion>((\<lambda>y. succ(rank y)) ` elts a)"
   by (metis elts_Sup image_image rank replacement set_of_elts small_elts)
 
 lemma Ord_rank [simp]: "Ord(rank a)"
 proof (induction a rule: eps_induct)
   case (step x)
   then show ?case
     unfolding rank_Sup [of x]
     by (metis (mono_tags, lifting) Ord_Sup Ord_succ imageE)
 qed
 
 lemma rank_of_Ord: "Ord i \<Longrightarrow> rank i = i"
   apply (induction rule: Ord_induct)
   by (metis (no_types, lifting) Ord_equality SUP_cong rank_Sup)
 
 lemma Ord_iff_rank: "Ord x \<longleftrightarrow> rank x = x"
   using Ord_rank [of x] rank_of_Ord by fastforce
 
 lemma rank_lt: "a \<in> elts b \<Longrightarrow> rank a < rank b"
   apply (subst rank [of b])
   by (metis (no_types, lifting) Ord_mem_iff_lt Ord_rank small_UN UN_iff elts_of_set elts_succ insert_iff rank small_elts)
 
 lemma rank_0 [simp]: "rank 0 = 0"
   unfolding rank_def
   using transrec by fastforce
 
 lemma rank_succ [simp]: "rank(succ x) = succ(rank x)"
 proof (rule order_antisym)
   show "rank (succ x) \<le> succ (rank x)"
     apply (subst rank [of "succ x"])
     apply (metis (no_types, lifting) Sup_insert elts_of_set elts_succ equals0D image_insert rank small_sup_iff subset_insertI sup.orderE vsubsetI)
     done
   show "succ (rank x) \<le> rank (succ x)"
     by (metis (mono_tags, lifting) ZFC_in_HOL.Sup_upper elts_succ image_insert insertI1 rank_Sup replacement small_elts)
 qed
 
 lemma rank_mono: "a \<le> b \<Longrightarrow> rank a \<le> rank b"
   apply (rule vsubsetI)
   using rank [of a] rank [of b] small_UN by auto
 
 lemma VsetI: "rank b \<sqsubset> i \<Longrightarrow> b \<in> elts (Vset i)"
 proof (induction i arbitrary: b rule: eps_induct)
   case (step x)
   then consider "rank b \<in> elts x" | "(\<exists>y\<in>elts x. rank b \<in> elts (TC y))"
     using le_TC_def less_TC_def less_TC_iff by fastforce
   then have "\<exists>y\<in>elts x. b \<le> Vset y"
   proof cases
     case 1
     then have "b \<le> Vset (rank b)"
       unfolding less_eq_V_def subset_iff
       by (meson Ord_mem_iff_lt Ord_rank le_TC_refl less_TC_iff rank_lt step.IH)
     then show ?thesis
       using "1" by blast
   next
     case 2
     then show ?thesis
       using step.IH
       unfolding less_eq_V_def subset_iff less_TC_def
       by (meson Ord_mem_iff_lt Ord_rank Transset_TC Transset_def rank_lt vsubsetD)
   qed
   then show ?case
     by (simp add: Vset [of x])
 qed
 
 lemma Ord_VsetI: "\<lbrakk>Ord i; rank b < i\<rbrakk> \<Longrightarrow> b \<in> elts (Vset i)"
   by (meson Ord_mem_iff_lt Ord_rank VsetI arg_subset_TC less_TC_def vsubsetD)
 
 lemma arg_le_Vset_rank: "a \<le> Vset(rank a)"
   by (simp add: Ord_VsetI rank_lt vsubsetI)
 
 lemma two_in_Vset:
   obtains \<alpha> where  "x \<in> elts (Vset \<alpha>)" "y \<in> elts (Vset \<alpha>)"
   by (metis Ord_rank Ord_VsetI elts_of_set insert_iff rank_lt small_elts small_insert_iff)
 
 lemma rank_eq_0_iff [simp]: "rank x = 0 \<longleftrightarrow> x=0"
   using arg_le_Vset_rank by fastforce
 
 lemma small_ranks_imp_small:
   assumes "small (rank ` A)" shows "small A"
 proof -
   define i where "i \<equiv> set (\<Union>(elts ` (rank ` A)))"
   have "Ord i"
     unfolding i_def using Ord_Union Ord_rank assms imageE by blast
   have *: "Vset (rank x) \<le> (Vset i)" if "x \<in> A" for x
     unfolding i_def by (metis Ord_rank Sup_V_def ZFC_in_HOL.Sup_upper Vfrom_mono assms imageI le_less that)
   have "A \<subseteq> elts (VPow (Vset i))"
     by (meson "*" VPow_iff arg_le_Vset_rank order.trans subsetI)
   then show ?thesis
     using down by blast
 qed
 
 lemma rank_Union: "rank(\<Squnion> A) = \<Squnion> (rank ` A)"
 proof (rule order_antisym)
   have "elts (SUP y\<in>elts (\<Squnion> A). succ (rank y)) \<subseteq> elts (\<Squnion> (rank ` A))"
     apply auto(*SLOW*)
     using Ord_mem_iff_lt Ord_rank rank_lt apply blast
     by (meson less_le_not_le rank_lt vsubsetD)
   then show "rank (\<Squnion> A) \<le> \<Squnion> (rank ` A)"
     by (metis less_eq_V_def rank_Sup)
   show "\<Squnion> (rank ` A) \<le> rank (\<Squnion> A)"
   proof (cases "small A")
     case True
     then show ?thesis
       by (metis (mono_tags, lifting) ZFC_in_HOL.Sup_least ZFC_in_HOL.Sup_upper image_iff rank_mono)
   next
     case False
     then have "\<not> small (rank ` A)"
       using small_ranks_imp_small by blast
     then show ?thesis
       by blast
   qed
 qed
 
 lemma small_bounded_rank:  "small {x. rank x \<in> elts a}"
 proof -
   have "{x. rank x \<in> elts a} \<subseteq> {x. rank x \<sqsubset> a}"
     using less_TC_iff by auto
   also have "\<dots> \<subseteq> elts (Vset a)"
     using VsetI by blast
   finally show ?thesis
     using down by simp
 qed
 
 lemma small_bounded_rank_le:  "small {x. rank x \<le> a}"
   using small_bounded_rank [of "VPow a"] VPow_iff [of _ a]  by simp
 
 lemma TC_rank_lt: "a \<sqsubset> b \<Longrightarrow> rank a < rank b"
 proof (induction rule: TC_induct_down)
   case (base y)
   then show ?case
     by (simp add: rank_lt)
 next
   case (step y z)
   then show ?case
     using less_trans rank_lt by blast
 next
   case small
   show ?case
     apply (rule smaller_than_small [OF small_bounded_rank_le [of "rank b"]])
     by (simp add: Collect_mono less_V_def)
 qed
 
 lemma TC_rank_mem: "x \<sqsubset> y \<Longrightarrow> rank x \<in> elts (rank y)"
   by (simp add: Ord_mem_iff_lt TC_rank_lt)
 
 lemma wf_TC_less: "wf {(x,y). x \<sqsubset> y}"
   proof (rule wf_subset [OF wf_inv_image [OF foundation, of rank]])
     show "{(x, y). x \<sqsubset> y} \<subseteq> inv_image {(x, y). x \<in> elts y} rank"
       by (auto simp: TC_rank_mem inv_image_def)
 qed
 
 lemma less_TC_minimal:
   assumes "P a"
   obtains x where "P x" "x \<sqsubseteq> a" "\<And>y. y \<sqsubset> x \<Longrightarrow> \<not> P y"
   using wfE_min' [OF wf_TC_less, of "{x. P x \<and> x \<sqsubseteq> a}"]
   by simp (metis le_TC_def less_le_TC_trans assms)
 
 lemma Vfrom_rank_eq: "Vfrom A (rank(x)) = Vfrom A x"
 proof (rule order_antisym)
   show "Vfrom A (rank x) \<le> Vfrom A x"
   proof (induction x rule: eps_induct)
     case (step x)
     have "(SUP j\<in>elts (rank x). VPow (Vfrom A j)) \<le> (SUP j\<in>elts x. VPow (Vfrom A j))"
       apply (rule Sup_least, clarify)
       apply (simp add: rank [of x])
       using step.IH
       by (metis Ord_rank OrdmemD Vfrom_mono2 dual_order.trans inf_sup_aci(5) less_V_def sup.orderE)
     then show ?case
       by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
 qed
   show "Vfrom A x \<le> Vfrom A (rank x)"
   proof (induction x rule: eps_induct)
     case (step x)
     have "(SUP j\<in>elts x. VPow (Vfrom A j)) \<le> (SUP j\<in>elts (rank x). VPow (Vfrom A j))"
       using step.IH TC_rank_mem less_TC_iff by force
     then show ?case
       by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
   qed
 qed
 
 lemma Vfrom_succ: "Vfrom A (succ(i)) = A \<squnion> VPow(Vfrom A i)"
   by (metis Ord_rank Vfrom_rank_eq Vfrom_succ_Ord rank_succ)
 
 lemma Vset_succ_TC:
   assumes "x \<in> elts (Vset (ZFC_in_HOL.succ k))" "u \<sqsubset> x"
   shows "u \<in> elts (Vset k)"
   using assms
   apply (simp add: Vfrom_succ)
   using TC_least Transset_Vfrom less_TC_def by auto
 
 subsection\<open>Cardinal Numbers\<close>
 
 text\<open>We extend the membership relation to a wellordering\<close>
 definition VWO :: "(V \<times> V) set"
   where "VWO \<equiv> @r. {(x,y). x \<in> elts y} \<subseteq> r \<and> Well_order r \<and> Field r = UNIV"
 
 lemma VWO: "{(x,y). x \<in> elts y} \<subseteq> VWO \<and> Well_order VWO \<and> Field VWO = UNIV"
   unfolding VWO_def
   by (metis (mono_tags, lifting) VWO_def foundation someI_ex total_well_order_extension)
 
 lemma wf_VWO: "wf(VWO - Id)"
   using VWO well_order_on_def by blast
 
 lemma wf_Ord_less: "wf {(x, y). Ord y \<and> x < y}"
   by (metis (no_types, lifting) Ord_mem_iff_lt eps_induct wfPUNIVI wfP_def)
 
 lemma refl_VWO: "refl VWO"
   using VWO order_on_defs by fastforce
 
 lemma trans_VWO: "trans VWO"
   using VWO by (simp add: VWO wo_rel.TRANS wo_rel_def)
 
 lemma antisym_VWO: "antisym VWO"
   using VWO by (simp add: VWO wo_rel.ANTISYM wo_rel_def)
 
 lemma total_VWO: "total VWO"
     using VWO by (metis wo_rel.TOTAL wo_rel.intro)
 
 lemma total_VWOId: "total (VWO-Id)"
   by (simp add: total_VWO)
 
 lemma Linear_order_VWO: "Linear_order VWO"
   using VWO well_order_on_def by blast
 
 lemma wo_rel_VWO: "wo_rel VWO"
   using VWO wo_rel_def by blast
 
 subsubsection \<open>Transitive Closure and VWO\<close>
 
 lemma mem_imp_VWO: "x \<in> elts y \<Longrightarrow> (x,y) \<in> VWO"
   using VWO by blast
 
 lemma less_TC_imp_VWO: "x \<sqsubset> y \<Longrightarrow> (x,y) \<in> VWO"
   unfolding less_TC_def
 proof (induction y arbitrary: x rule: eps_induct)
   case (step y' u)
   then consider "u \<in> elts y'" | v where "v \<in> elts y'" "u \<in> elts (TC v)"
     by (auto simp: TC [of y'])
   then show ?case
   proof cases
     case 2
     then show ?thesis
       by (meson mem_imp_VWO step.IH transD trans_VWO)
   qed (use mem_imp_VWO in blast)
 qed
 
 lemma le_TC_imp_VWO: "x \<sqsubseteq> y \<Longrightarrow> (x,y) \<in> VWO"
   apply (auto simp: le_TC_def less_TC_imp_VWO)
   by (metis Diff_iff Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO)
 
 lemma le_TC_0_iff [simp]: "x \<sqsubseteq> 0 \<longleftrightarrow> x = 0"
   by (simp add: le_TC_def)
 
 lemma less_TC_succ: " x \<sqsubset> succ \<beta> \<longleftrightarrow> x \<sqsubset> \<beta> \<or> x = \<beta>"
   by (metis elts_succ insert_iff le_TC_def less_TC_iff)
 
 lemma le_TC_succ: "x \<sqsubseteq> succ \<beta> \<longleftrightarrow> x \<sqsubseteq> \<beta> \<or> x = succ \<beta>"
   by (simp add: le_TC_def less_TC_succ)
 
 lemma Transset_TC_eq [simp]: "Transset x \<Longrightarrow> TC x = x"
   by (simp add: TC_least arg_subset_TC eq_iff)
 
 lemma Ord_TC_less_iff: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> \<beta> \<sqsubset> \<alpha> \<longleftrightarrow> \<beta> < \<alpha>"
   by (metis Ord_def Ord_mem_iff_lt Transset_TC_eq less_TC_def)
 
 lemma Ord_mem_iff_less_TC: "Ord l \<Longrightarrow> k \<in> elts l \<longleftrightarrow> k \<sqsubset> l"
   by (simp add: Ord_def less_TC_def)
 
 lemma le_TC_Ord: "\<lbrakk>\<beta> \<sqsubseteq> \<alpha>; Ord \<alpha>\<rbrakk> \<Longrightarrow> Ord \<beta>"
   by (metis Ord_def Ord_in_Ord Transset_TC_eq le_TC_def less_TC_def)
 
 lemma Ord_less_TC_mem:
   assumes "Ord \<alpha>" "\<beta> \<sqsubset> \<alpha>" shows "\<beta> \<in> elts \<alpha>"
   using Ord_def assms less_TC_def by auto
 
 lemma VWO_TC_le: "\<lbrakk>Ord \<alpha>; Ord \<beta>; (\<beta>, \<alpha>) \<in> VWO\<rbrakk> \<Longrightarrow> \<beta> \<sqsubseteq> \<alpha>"
 proof (induct \<alpha> arbitrary: \<beta> rule: Ord_induct)
   case (step \<alpha>)
   then show ?case
     by (metis Diff_iff Linear_order_VWO Linear_order_in_diff_Id Ord_TC_less_iff Ord_linear2 UNIV_I VWO le_TC_def le_less less_TC_imp_VWO pair_in_Id_conv)
 qed
 
 lemma VWO_iff_Ord_le [simp]: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> (\<beta>, \<alpha>) \<in> VWO \<longleftrightarrow> \<beta> \<le> \<alpha>"
   by (metis VWO_TC_le Ord_TC_less_iff le_TC_def le_TC_imp_VWO le_less)
 
 lemma zero_TC_le [iff]: "0 \<sqsubseteq> y"
   using le_TC_def nonzero_less_TC by auto
 
 lemma succ_le_TC_iff: "Ord j \<Longrightarrow> succ i \<sqsubseteq> j \<longleftrightarrow> i \<sqsubset> j"
   by (metis Ord_in_Ord Ord_linear Ord_mem_iff_less_TC Ord_succ le_TC_def less_TC_succ less_asym_TC)
 
 lemma VWO_0_iff [simp]: "(x,0) \<in> VWO \<longleftrightarrow> x=0"
 proof
   show "x = 0" if "(x, 0) \<in> VWO"
     using zero_TC_le [of x] le_TC_imp_VWO that
     by (metis DiffI Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO pair_in_Id_conv)
 qed auto
 
 lemma VWO_antisym:
   assumes "(x,y) \<in> VWO" "(y,x) \<in> VWO" shows "x=y"
   by (metis Diff_iff IdD Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO assms)
 
 subsubsection \<open>Relation VWF\<close>
 
 definition VWF where "VWF \<equiv> VWO - Id"
 
 lemma wf_VWF [iff]: "wf VWF"
   by (simp add: VWF_def wf_VWO)
 
 lemma trans_VWF [iff]: "trans VWF"
   by (simp add: VWF_def antisym_VWO trans_VWO trans_diff_Id)
 
 lemma asym_VWF [iff]: "asym VWF"
   by (metis VWF_def asym.intros irrefl_diff_Id wf_VWF wf_not_sym)
 
 lemma total_VWF [iff]: "total VWF"
   using VWF_def total_VWOId by auto
 
 lemma total_on_VWF [iff]: "total_on A VWF"
   by (meson UNIV_I total_VWF total_on_def)
 
 lemma VWF_asym:
   assumes "(x,y) \<in> VWF" "(y,x) \<in> VWF" shows False
   using VWF_def assms wf_VWO wf_not_sym by fastforce
 
 lemma VWF_non_refl [iff]: "(x,x) \<notin> VWF"
   by simp
 
 lemma VWF_iff_Ord_less [simp]: "\<lbrakk>Ord \<alpha>; Ord \<beta>\<rbrakk> \<Longrightarrow> (\<alpha>,\<beta>) \<in> VWF \<longleftrightarrow> \<alpha> < \<beta>"
   by (simp add: VWF_def less_V_def)
 
 lemma mem_imp_VWF: "x \<in> elts y \<Longrightarrow> (x,y) \<in> VWF"
   using VWF_def mem_imp_VWO by fastforce
 
 
 subsection\<open>Order types\<close>
 
 definition ordermap :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> V"
   where "ordermap A r \<equiv> wfrec r (\<lambda>f x. set (f ` {y \<in> A. (y,x) \<in> r}))"
 
 definition ordertype :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> V"
   where "ordertype A r \<equiv> set (ordermap A r ` A)"
 
 lemma ordermap_type:
     "small A \<Longrightarrow> ordermap A r \<in> A \<rightarrow> elts (ordertype A r)"
   by (simp add: ordertype_def)
 
 lemma ordermap_in_ordertype [intro]: "\<lbrakk>a \<in> A; small A\<rbrakk> \<Longrightarrow> ordermap A r a \<in> elts (ordertype A r)"
   by (simp add: ordertype_def)
 
 lemma ordermap: "wf r \<Longrightarrow> ordermap A r a = set (ordermap A r ` {y \<in> A. (y,a) \<in> r})"
   unfolding ordermap_def
   by (auto simp: wfrec_fixpoint adm_wf_def)
 
 lemma wf_Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)"
   using \<open>wf r\<close>
 proof (induction x rule: wf_induct_rule)
   case (less u)
   have "Transset (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))"
   proof (clarsimp simp add: Transset_def)
     show "x \<in> ordermap A r ` {y \<in> A. (y, u) \<in> r}"
       if "small (ordermap A r ` {y \<in> A. (y, u) \<in> r})"
         and x: "x \<in> elts (ordermap A r y)" and "y \<in> A" "(y, u) \<in> r" for x y
     proof -
       have "ordermap A r y = ZFC_in_HOL.set (ordermap A r ` {a \<in> A. (a, y) \<in> r})"
         using ordermap assms(1) by force
       then have "x \<in> ordermap A r ` {z \<in> A. (z, y) \<in> r}"
         by (metis (no_types, lifting) elts_of_set empty_iff x)
       then have "\<exists>v. v \<in> A \<and> (v, u) \<in> r \<and> x = ordermap A r v"
         using that transD [OF \<open>trans r\<close>] by blast
       then show ?thesis
         by blast
     qed
   qed
   moreover have "Ord x"
     if "x \<in> elts (set (ordermap A r ` {y \<in> A. (y, u) \<in> r}))" for x
     using that less by (auto simp: split: if_split_asm)
   ultimately show ?case
     by (metis (full_types) Ord_def ordermap assms(1))
 qed
 
 lemma wf_Ord_ordertype: assumes "wf r" "trans r" shows "Ord(ordertype A r)"
 proof -
   have "y \<le> set (ordermap A r ` A)"
     if "y = ordermap A r x" "x \<in> A" "small (ordermap A r ` A)" for x y
     using that by (auto simp: less_eq_V_def ordermap [OF \<open>wf r\<close>, of A x])
   moreover have "z \<le> y" if "y \<in> ordermap A r ` A" "z \<in> elts y" for y z
     by (metis wf_Ord_ordermap OrdmemD assms imageE order.strict_implies_order that)
   ultimately show ?thesis
     unfolding ordertype_def Ord_def Transset_def by simp
 qed
 
 lemma Ord_ordertype [simp]: "Ord(ordertype A VWF)"
   using wf_Ord_ordertype by blast
 
 lemma Ord_ordermap [simp]: "Ord (ordermap A VWF x)"
   by blast
 
 lemma ordertype_singleton [simp]:
   assumes "wf r" 
   shows "ordertype {x} r = 1"
 proof -
   have \<dagger>: "{y. y = x \<and> (y, x) \<in> r} = {}"
     using assms by auto
   show ?thesis
     by (auto simp add: ordertype_def assms \<dagger> ordermap [where a=x])
 qed
 
 
 subsubsection\<open>@{term ordermap} preserves the orderings in both directions\<close>
 
 lemma ordermap_mono:
   assumes wx: "(w, x) \<in> r" and "wf r" "w \<in> A" "small A"
     shows "ordermap A r w \<in> elts (ordermap A r x)"
 proof -
   have "small {a \<in> A. (a, x) \<in> r} \<and> w \<in> A \<and> (w, x) \<in> r"
     by (simp add: assms)
   then show ?thesis
     using assms ordermap [of r A]
     by (metis (no_types, lifting) elts_of_set image_eqI mem_Collect_eq replacement)
 qed
 
 lemma converse_ordermap_mono:
   assumes "ordermap A r y \<in> elts (ordermap A r x)" "wf r" "total_on A r" "x \<in> A" "y \<in> A" "small A"
   shows "(y, x) \<in> r"
 proof (cases "x = y")
   case True
   then show ?thesis
     using assms(1) mem_not_refl by blast
 next
   case False
   then consider "(x,y) \<in> r" | "(y,x) \<in> r"
     using \<open>total_on A r\<close> assms by (meson UNIV_I total_on_def)
   then show ?thesis
     by (meson ordermap_mono assms mem_not_sym)
 qed
 
+lemma converse_ordermap_mono_iff:
+  assumes "wf r" "total_on A r" "x \<in> A" "y \<in> A" "small A"
+  shows "ordermap A r y \<in> elts (ordermap A r x) \<longleftrightarrow> (y, x) \<in> r"
+  by (metis assms converse_ordermap_mono ordermap_mono)
+
 lemma ordermap_surj: "elts (ordertype A r) \<subseteq> ordermap A r ` A"
   unfolding ordertype_def by simp
 
 lemma ordermap_bij:
   assumes "wf r" "total_on A r" "small A"
   shows "bij_betw (ordermap A r) A (elts (ordertype A r))"
   unfolding bij_betw_def
   proof (intro conjI)
     show "inj_on (ordermap A r) A"
     unfolding inj_on_def by (metis assms mem_not_refl ordermap_mono total_on_def)
   show "ordermap A r ` A = elts (ordertype A r)"
     by (metis ordertype_def \<open>small A\<close> elts_of_set replacement)
 qed
 
 lemma ordermap_eq_iff [simp]: 
   "\<lbrakk>x \<in> A; y \<in> A; wf r; total_on A r; small A\<rbrakk> \<Longrightarrow> ordermap A r x = ordermap A r y \<longleftrightarrow> x = y"
   by (metis bij_betw_iff_bijections ordermap_bij)
 
 lemma inv_into_ordermap: "\<alpha> \<in> elts (ordertype A r) \<Longrightarrow> inv_into A (ordermap A r) \<alpha> \<in> A"
   by (meson in_mono inv_into_into ordermap_surj)
 
 lemma ordertype_nat_imp_finite:
   assumes "ordertype A r = ord_of_nat m" "small A" "wf r" "total_on A r"
   shows "finite A"
 proof -
   have "A \<approx> elts m"
     using eqpoll_def assms ordermap_bij by fastforce 
   then show ?thesis
     using eqpoll_finite_iff finite_Ord_omega by blast
 qed
 
 lemma wf_ordertype_eqpoll:
   assumes "wf r" "total_on A r" "small A"
   shows "elts (ordertype A r) \<approx> A"
   using assms eqpoll_def eqpoll_sym ordermap_bij by blast
 
 lemma ordertype_eqpoll:
   assumes "small A"
   shows "elts (ordertype A VWF) \<approx> A"
   using assms wf_ordertype_eqpoll total_VWF wf_VWF
   by (simp add: wf_ordertype_eqpoll total_on_def)
 
 subsection \<open>More advanced @{term ordertype} and @{term ordermap} results\<close>
 
 lemma ordermap_VWF_0 [simp]: "ordermap A VWF 0 = 0"
   by (simp add: ordermap wf_VWO VWF_def)
 
 lemma ordertype_empty [simp]: "ordertype {} r = 0"
   by (simp add: ordertype_def)
 
 lemma ordertype_eq_0_iff [simp]: "\<lbrakk>small X; wf r\<rbrakk> \<Longrightarrow> ordertype X r = 0 \<longleftrightarrow> X = {}"
   by (metis ordertype_def elts_of_set replacement image_is_empty zero_V_def)
 
 lemma ordermap_mono_less:
   assumes "(w, x) \<in> r"
       and "wf r" "trans r"
       and "w \<in> A" "x \<in> A"
       and "small A"
     shows "ordermap A r w < ordermap A r x"
   by (simp add: OrdmemD assms ordermap_mono)
 
 lemma ordermap_mono_le:
   assumes "(w, x) \<in> r \<or> w=x"
       and "wf r" "trans r"
       and "w \<in> A" "x \<in> A"
       and "small A"
     shows "ordermap A r w \<le> ordermap A r x"
   by (metis assms dual_order.strict_implies_order eq_refl ordermap_mono_less)
 
 lemma converse_ordermap_le_mono:
   assumes "ordermap A r y \<le> ordermap A r x" "wf r" "total r"  "x \<in> A" "small A"
   shows "(y, x) \<in> r \<or> y=x"
   by (meson UNIV_I assms mem_not_refl ordermap_mono total_on_def vsubsetD)
 
 lemma ordertype_mono:
   assumes "X \<subseteq> Y" and r: "wf r" "trans r" and "small Y"
   shows "ordertype X r \<le> ordertype Y r"
 proof -
   have "small X"
     using assms smaller_than_small by fastforce 
   have *: "ordermap X r x \<le> ordermap Y r x" for x
     using \<open>wf r\<close>
   proof (induction x rule: wf_induct_rule)
     case (less x)
     have "ordermap X r z < ordermap Y r x" if "z \<in> X" and zx: "(z,x) \<in> r" for z
       using less [OF zx] assms
       by (meson Ord_linear2 OrdmemD wf_Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx)
     then show ?case
       by (auto simp add: ordermap [of _ X x] \<open>small X\<close> Ord_mem_iff_lt set_image_le_iff less_eq_V_def r)
   qed
   show ?thesis
   proof -
     have "ordermap Y r ` Y = elts (ordertype Y r)"
       by (metis ordertype_def \<open>small Y\<close> elts_of_set replacement)
     then have "ordertype Y r \<notin> ordermap X r ` X"
       using "*" \<open>X \<subseteq> Y\<close> by fastforce
     then show ?thesis
       by (metis Ord_linear2 Ord_mem_iff_lt ordertype_def wf_Ord_ordertype \<open>small X\<close> elts_of_set replacement r)
   qed
 qed
 
 corollary ordertype_VWF_mono:
   assumes "X \<subseteq> Y" "small Y"
   shows "ordertype X VWF \<le> ordertype Y VWF"
   using assms by (simp add: ordertype_mono)
 
 lemma ordertype_UNION_ge:
   assumes "A \<in> \<A>" "wf r" "trans r" "\<A> \<subseteq> Collect small" "small \<A>"
   shows "ordertype A r \<le> ordertype (\<Union>\<A>) r" 
   by (rule ordertype_mono) (use assms in auto)
 
 lemma inv_ordermap_mono_less:
   assumes "(inv_into M (ordermap M r) \<alpha>, inv_into M (ordermap M r) \<beta>) \<in> r" 
     and "small M" and \<alpha>: "\<alpha> \<in> elts (ordertype M r)" and \<beta>: "\<beta> \<in> elts (ordertype M r)"
     and "wf r" "trans r"
   shows "\<alpha> < \<beta>"
 proof -
   have "\<alpha> = ordermap M r (inv_into M (ordermap M r) \<alpha>)"
     by (metis \<alpha> f_inv_into_f ordermap_surj subset_eq)
   also have "\<dots> < ordermap M r (inv_into M (ordermap M r) \<beta>)"
     by (meson \<alpha> \<beta> assms in_mono inv_into_into ordermap_mono_less ordermap_surj)
   also have "\<dots> = \<beta>"
     by (meson \<beta> f_inv_into_f in_mono ordermap_surj)
   finally show ?thesis .
 qed
 
 lemma inv_ordermap_mono_eq:
   assumes "inv_into M (ordermap M r) \<alpha> = inv_into M (ordermap M r) \<beta>" 
     and "\<alpha> \<in> elts (ordertype M r)" "\<beta> \<in> elts (ordertype M r)"
   shows "\<alpha> = \<beta>"
   by (metis assms f_inv_into_f ordermap_surj subsetD)
 
 lemma inv_ordermap_VWF_mono_le:
   assumes "inv_into M (ordermap M VWF) \<alpha> \<le> inv_into M (ordermap M VWF) \<beta>" 
     and "M \<subseteq> ON" "small M" and \<alpha>: "\<alpha> \<in> elts (ordertype M VWF)" and \<beta>: "\<beta> \<in> elts (ordertype M VWF)"
   shows "\<alpha> \<le> \<beta>"
 proof -
   have "\<alpha> = ordermap M VWF (inv_into M (ordermap M VWF) \<alpha>)"
     by (metis \<alpha> f_inv_into_f ordermap_surj subset_eq)
   also have "\<dots> \<le> ordermap M VWF (inv_into M (ordermap M VWF) \<beta>)"
     by (metis ON_imp_Ord VWF_iff_Ord_less assms dual_order.strict_implies_order elts_of_set eq_refl inv_into_into order.not_eq_order_implies_strict ordermap_mono_less ordertype_def replacement trans_VWF wf_VWF)
   also have "\<dots> = \<beta>"
     by (meson \<beta> f_inv_into_f in_mono ordermap_surj)
   finally show ?thesis .
 qed
 
+lemma inv_ordermap_VWF_mono_iff:
+  assumes "M \<subseteq> ON" "small M" and "\<alpha> \<in> elts (ordertype M VWF)" and "\<beta> \<in> elts (ordertype M VWF)"
+  shows "inv_into M (ordermap M VWF) \<alpha> \<le> inv_into M (ordermap M VWF) \<beta> \<longleftrightarrow> \<alpha> \<le> \<beta>"
+  by (metis ON_imp_Ord Ord_linear_le assms dual_order.eq_iff inv_into_ordermap inv_ordermap_VWF_mono_le)
+
+lemma inv_ordermap_VWF_strict_mono_iff:
+  assumes "M \<subseteq> ON" "small M" and "\<alpha> \<in> elts (ordertype M VWF)" and "\<beta> \<in> elts (ordertype M VWF)"
+  shows "inv_into M (ordermap M VWF) \<alpha> < inv_into M (ordermap M VWF) \<beta> \<longleftrightarrow> \<alpha> < \<beta>"
+  by (simp add: assms inv_ordermap_VWF_mono_iff less_le_not_le)
+
 lemma strict_mono_on_ordertype:
   assumes "M \<subseteq> ON" "small M"
   obtains f where "f \<in> elts (ordertype M VWF) \<rightarrow> M" "strict_mono_on f (elts (ordertype M VWF))"
 proof 
   show "inv_into M (ordermap M VWF) \<in> elts (ordertype M VWF) \<rightarrow> M"
     by (meson Pi_I' in_mono inv_into_into ordermap_surj)
   show "strict_mono_on (inv_into M (ordermap M VWF)) (elts (ordertype M VWF))"
   proof (clarsimp simp: strict_mono_on_def)
     fix x y
     assume "x \<in> elts (ordertype M VWF)" "y \<in> elts (ordertype M VWF)" "x < y"
     then show "inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y"
       using assms by (meson ON_imp_Ord Ord_linear2 inv_into_into inv_ordermap_VWF_mono_le leD ordermap_surj subsetD)
   qed
 qed
 
 lemma ordermap_inc_eq:
   assumes "x \<in> A" "small A"
     and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> s"
     and r: "wf r" "total_on A r" and "wf s" 
   shows "ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x"
   using \<open>wf r\<close> \<open>x \<in> A\<close>
 proof (induction x rule: wf_induct_rule)
   case (less x)
   then have 1: "{y \<in> A. (y, x) \<in> r} = A \<inter> {y. (y, x) \<in> r}"
     using r by auto
   have 2: "{y \<in> \<pi> ` A. (y, \<pi> x) \<in> s} = \<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}"
     by auto
   have inv\<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (\<pi> x, \<pi> y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r"
     by (metis \<pi> \<open>wf s\<close> \<open>total_on A r\<close> total_on_def wf_not_sym)
   have eq: "f ` (\<pi> ` A \<inter> {y. (y, \<pi> x) \<in> s}) = (f \<circ> \<pi>) ` (A \<inter> {y. (y, x) \<in> r})" for f :: "'b \<Rightarrow> V"
     using less by (auto simp: image_subset_iff inv\<pi> \<pi>)
   show ?case
     using less
     by (simp add: ordermap [OF \<open>wf r\<close>, of _ x] ordermap [OF \<open>wf s\<close>, of _ "\<pi> x"] 1 2 eq)
 qed
 
 lemma ordertype_inc_eq:
   assumes "small A"
     and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> s"
     and r: "wf r" "total_on A r" and "wf s" 
   shows "ordertype (\<pi> ` A) s = ordertype A r"
 proof -
   have "ordermap (\<pi> ` A) s (\<pi> x) = ordermap A r x" if "x \<in> A" for x
     using assms that by (auto simp: ordermap_inc_eq)
   then show ?thesis
     unfolding ordertype_def
     by (metis (no_types, lifting) image_cong image_image)
 qed
 
 lemma ordertype_inc_le:
   assumes "small A" "small B"
     and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> s"
     and r: "wf r" "total_on A r" and "wf s" "trans s"
     and "\<pi> ` A \<subseteq> B"
   shows "ordertype A r \<le> ordertype B s"
   by (metis assms ordertype_inc_eq ordertype_mono)
 
 corollary ordertype_VWF_inc_eq:
   assumes "A \<subseteq> ON" "\<pi> ` A \<subseteq> ON" "small A" and "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; x<y\<rbrakk> \<Longrightarrow> \<pi> x < \<pi> y"
   shows "ordertype (\<pi> ` A) VWF = ordertype A VWF"
 proof (rule ordertype_inc_eq)
   show "(\<pi> x, \<pi> y) \<in> VWF"
     if "x \<in> A" "y \<in> A" "(x, y) \<in> VWF" for x y
     using that ON_imp_Ord assms by auto
   show "total_on A VWF"
     by (meson UNIV_I total_VWF total_on_def)
 qed (use assms in auto)
 
 lemma ordertype_image_ordermap:
   assumes "small A" "X \<subseteq> A" "wf r" "trans r" "total_on X r"
   shows "ordertype (ordermap A r ` X) VWF = ordertype X r"
 proof (rule ordertype_inc_eq)
   show "small X"
     by (meson assms smaller_than_small)
   show "(ordermap A r x, ordermap A r y) \<in> VWF"
     if "x \<in> X" "y \<in> X" "(x, y) \<in> r" for x y
     by (meson that wf_Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD)
 qed (use assms in auto)
     
 lemma ordertype_map_image:
   assumes "B \<subseteq> A" "small A"
   shows "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (A - B) VWF"
 proof -
   have "ordermap A VWF ` A - ordermap A VWF ` B = ordermap A VWF ` (A - B)"
     using assms by auto
   then have "ordertype (ordermap A VWF ` A - ordermap A VWF ` B) VWF = ordertype (ordermap A VWF ` (A - B)) VWF"
     by simp
   also have "\<dots> = ordertype (A - B) VWF"
     using \<open>small A\<close> ordertype_image_ordermap by fastforce
   finally show ?thesis .
 qed
 
 proposition ordertype_le_ordertype:
   assumes r: "wf r" "total_on A r" and "small A"
   assumes s: "wf s" "total_on B s" "trans s" and "small B"
   shows "ordertype A r \<le> ordertype B s \<longleftrightarrow>
          (\<exists>f \<in> A \<rightarrow> B. inj_on f A \<and> (\<forall>x \<in> A. \<forall>y \<in> A. ((x,y) \<in> r \<longrightarrow> (f x, f y) \<in> s)))"
     (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   define f where "f \<equiv> inv_into B (ordermap B s) \<circ> ordermap A r"
   show ?rhs
   proof (intro bexI conjI ballI impI)
     have AB: "elts (ordertype A r) \<subseteq> ordermap B s ` B"
       by (metis L assms(7) ordertype_def replacement set_of_elts small_elts subset_iff_less_eq_V)
     have bijA: "bij_betw (ordermap A r) A (elts (ordertype A r))"
       using ordermap_bij \<open>small A\<close> r by blast
     have "inv_into B (ordermap B s) (ordermap A r i) \<in> B" if "i \<in> A" for i
       by (meson L \<open>small A\<close> inv_into_into ordermap_in_ordertype ordermap_surj subsetD that vsubsetD)
     then show "f \<in> A \<rightarrow> B"
       by (auto simp: Pi_iff f_def)
     show "inj_on f A"
     proof (clarsimp simp add: f_def inj_on_def)
       fix x y
       assume "x \<in> A" "y \<in> A"
         and "inv_into B (ordermap B s) (ordermap A r x) = inv_into B (ordermap B s) (ordermap A r y)"
       then have "ordermap A r x = ordermap A r y"
         by (meson AB \<open>small A\<close> inv_into_injective ordermap_in_ordertype subsetD)
       then show "x = y"
         by (metis \<open>x \<in> A\<close> \<open>y \<in> A\<close> bijA bij_betw_inv_into_left)
     qed
   next
     fix x y
     assume "x \<in> A" "y \<in> A" and "(x, y) \<in> r"
     have \<ddagger>: "ordermap A r y \<in> ordermap B s ` B"
       by (meson L \<open>y \<in> A\<close> \<open>small A\<close> in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
     moreover have \<dagger>: "\<And>x. inv_into B (ordermap B s) (ordermap A r x) = f x"
       by (simp add: f_def)
     then have *: "ordermap B s (f y) = ordermap A r y"
       using \<ddagger> by (metis f_inv_into_f)
     moreover have "ordermap A r x \<in> ordermap B s ` B"
       by (meson L \<open>x \<in> A\<close> \<open>small A\<close> in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
     moreover have "ordermap A r x < ordermap A r y"
       using * r s by (metis (no_types) wf_Ord_ordermap OrdmemD \<open>(x, y) \<in> r\<close> \<open>x \<in> A\<close> \<open>small A\<close> ordermap_mono)
     ultimately show "(f x, f y) \<in> s"
       using \<dagger> s by (metis assms(7) f_inv_into_f inv_into_into less_asym ordermap_mono_less total_on_def)
   qed
 next
   assume R: ?rhs
   then obtain f where f: "f\<in>A \<rightarrow> B" "inj_on f A" "\<forall>x\<in>A. \<forall>y\<in>A. (x, y) \<in> r \<longrightarrow> (f x, f y) \<in> s"
     by blast
   show ?lhs
     by (rule ordertype_inc_le [where \<pi>=f]) (use f assms in auto)
 qed
 
 lemma iso_imp_ordertype_eq_ordertype:
   assumes iso: "iso r r' f"
     and "wf r"
     and "Total r"
     and sm: "small (Field r)"
   shows "ordertype (Field r) r = ordertype (Field r') r'"
   by (metis (no_types, lifting) iso_forward iso_wf assms iso_Field ordertype_inc_eq sm)
 
 lemma ordertype_infinite_ge_\<omega>:
   assumes "infinite A" "small A"
   shows "ordertype A VWF \<ge> \<omega>"
 proof -
   have "inj_on (ordermap A VWF) A"
     by (meson ordermap_bij \<open>small A\<close> bij_betw_def total_on_VWF wf_VWF)
   then have "infinite (ordermap A VWF ` A)"
     using \<open>infinite A\<close> finite_image_iff by blast
   then show ?thesis
     using Ord_ordertype \<open>small A\<close> infinite_Ord_omega by (auto simp: ordertype_def)
 qed
 
 lemma ordertype_eqI:
   assumes "wf r" "total_on A r" "small A" "wf s" 
           "bij_betw f A B" "(\<forall>x \<in> A. \<forall>y \<in> A. (f x, f y) \<in> s \<longleftrightarrow> (x,y) \<in> r)"
   shows "ordertype A r = ordertype B s"
   by (metis assms bij_betw_imp_surj_on ordertype_inc_eq)
 
 lemma ordermap_eq_self:
   assumes "Ord \<alpha>" and x: "x \<in> elts \<alpha>" 
   shows "ordermap (elts \<alpha>) VWF x = x" 
   using Ord_in_Ord [OF assms] x 
 proof (induction x rule: Ord_induct)
   case (step x)
   have 1: "{y \<in> elts \<alpha>. (y, x) \<in> VWF} = elts x" (is "?A = _")
   proof
     show "?A \<subseteq> elts x"
       using \<open>Ord \<alpha>\<close> by clarify (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less step.hyps)
     show "elts x \<subseteq> ?A"
       using \<open>Ord \<alpha>\<close> by clarify (meson Ord_in_Ord Ord_trans OrdmemD VWF_iff_Ord_less step.prems)
   qed
   show ?case
     using step
     by (simp add: ordermap [OF wf_VWF, of _ x] 1 Ord_trans [of _ _ \<alpha>] step.prems \<open>Ord \<alpha>\<close> cong: image_cong)
 qed
 
 lemma ordertype_eq_Ord [simp]:
   assumes "Ord \<alpha>" 
   shows "ordertype (elts \<alpha>) VWF = \<alpha>"
   using assms ordermap_eq_self [OF assms] by (simp add: ordertype_def)
 
 
 proposition ordertype_eq_iff:
   assumes \<alpha>: "Ord \<alpha>" and r: "wf r" and "small A" "total_on A r" "trans r"
   shows "ordertype A r = \<alpha> \<longleftrightarrow>
          (\<exists>f. bij_betw f A (elts \<alpha>) \<and> (\<forall>x \<in> A. \<forall>y \<in> A. f x < f y \<longleftrightarrow> (x,y) \<in> r))"
     (is "?lhs = ?rhs")
 proof safe
   assume eq: "\<alpha> = ordertype A r"
   show "\<exists>f. bij_betw f A (elts (ordertype A r)) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. f x < f y \<longleftrightarrow> ((x, y) \<in> r))"
   proof (intro exI conjI ballI)
     show "bij_betw (ordermap A r) A (elts (ordertype A r))"
       by (simp add: assms ordermap_bij)
     then show "ordermap A r x < ordermap A r y \<longleftrightarrow> (x, y) \<in> r"
       if "x \<in> A" "y \<in> A" for x y
       using that assms
       by (metis order.asym ordermap_mono_less total_on_def)
   qed
 next
   fix f 
   assume f: "bij_betw f A (elts \<alpha>)" "\<forall>x\<in>A. \<forall>y\<in>A. f x < f y \<longleftrightarrow> (x, y) \<in> r"
   have "ordertype A r = ordertype (elts \<alpha>) VWF"
   proof (rule ordertype_eqI)
     show "\<forall>x\<in>A. \<forall>y\<in>A. ((f x, f y) \<in> VWF) = ((x, y) \<in> r)"
       by (meson Ord_in_Ord VWF_iff_Ord_less \<alpha> bij_betwE f)
   qed (use assms f in auto)
   then show ?lhs
     by (simp add: \<alpha>)
 qed
 
 corollary ordertype_VWF_eq_iff:
   assumes "Ord \<alpha>" "small A"
   shows "ordertype A VWF = \<alpha> \<longleftrightarrow>
          (\<exists>f. bij_betw f A (elts \<alpha>) \<and> (\<forall>x \<in> A. \<forall>y \<in> A. f x < f y \<longleftrightarrow> (x,y) \<in> VWF))"
   by (metis UNIV_I assms ordertype_eq_iff total_VWF total_on_def trans_VWF wf_VWF)
 
 
 lemma ordertype_le_Ord:
   assumes "Ord \<alpha>" "X \<subseteq> elts \<alpha>"
   shows "ordertype X VWF \<le> \<alpha>"
   by (metis assms ordertype_VWF_mono ordertype_eq_Ord small_elts)
 
 lemma ordertype_inc_le_Ord:
   assumes "small A" "Ord \<alpha>"
     and \<pi>: "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> \<pi> x < \<pi> y"
     and "wf r" "total_on A r" 
     and sub: "\<pi> ` A \<subseteq> elts \<alpha>"
   shows "ordertype A r \<le> \<alpha>"
 proof -
   have "\<And>x y. \<lbrakk>x\<in>A; y\<in>A; (x,y) \<in> r\<rbrakk> \<Longrightarrow> (\<pi> x, \<pi> y) \<in> VWF"
     by (meson Ord_in_Ord VWF_iff_Ord_less \<pi> \<open>Ord \<alpha>\<close> sub image_subset_iff)
   with assms show ?thesis
     by (metis ordertype_inc_eq ordertype_le_Ord wf_VWF)
 qed
 
 lemma le_ordertype_obtains_subset:
   assumes \<alpha>: "\<beta> \<le> \<alpha>" "ordertype H VWF = \<alpha>" and "small H" "Ord \<beta>"
   obtains G where "G \<subseteq> H" "ordertype G VWF = \<beta>" 
 proof (intro exI conjI that)
   let ?f = "ordermap H VWF"
   show \<ddagger>: "inv_into H ?f ` elts \<beta> \<subseteq> H"
     unfolding image_subset_iff
     by (metis \<alpha> inv_into_into ordermap_surj subsetD vsubsetD)
   have "\<exists>f. bij_betw f (inv_into H ?f ` elts \<beta>) (elts \<beta>) \<and> (\<forall>x\<in>inv_into H ?f ` elts \<beta>. \<forall>y\<in>inv_into H ?f ` elts \<beta>. (f x < f y) = ((x, y) \<in> VWF))"
   proof (intro exI conjI ballI iffI)
     show "bij_betw ?f (inv_into H ?f ` elts \<beta>) (elts \<beta>)"
       using ordermap_bij [OF wf_VWF total_on_VWF \<open>small H\<close>] \<alpha> 
       by (metis bij_betw_inv_into_RIGHT bij_betw_subset less_eq_V_def \<ddagger>)
   next
     fix x y
     assume x: "x \<in> inv_into H ?f ` elts \<beta>"
         and y: "y \<in> inv_into H ?f ` elts \<beta>"
     show "?f x < ?f y" if "(x,y) \<in> VWF"
       using that \<ddagger> \<open>small H\<close> in_mono ordermap_mono_less x y by fastforce
     show "(x,y) \<in> VWF" if "?f x < ?f y"
       using that \<ddagger> \<open>small H\<close> in_mono ordermap_mono_less [OF _ wf_VWF trans_VWF] x y
       by (metis UNIV_I less_imp_not_less total_VWF total_on_def)
   qed
   then show "ordertype (inv_into H ?f ` elts \<beta>) VWF = \<beta>"
     by (subst ordertype_eq_iff) (use assms in auto)
 qed
 
 lemma ordertype_infinite_\<omega>:
   assumes "A \<subseteq> elts \<omega>" "infinite A"
   shows "ordertype A VWF = \<omega>"
 proof (rule antisym)
   show "ordertype A VWF \<le> \<omega>"
     by (simp add: assms ordertype_le_Ord)
   show "\<omega> \<le> ordertype A VWF"
     using assms down ordertype_infinite_ge_\<omega> by auto
 qed
 
 text \<open>For infinite sets of natural numbers\<close>
 lemma ordertype_nat_\<omega>:
   assumes "infinite N" shows "ordertype N less_than = \<omega>"
 proof -
   have "small N"
     by (meson inj_on_def ord_of_nat_inject small_def small_iff_range small_image_nat_V)
   have "ordertype (ord_of_nat ` N) VWF = \<omega>"
     by (force simp: assms finite_image_iff inj_on_def intro: ordertype_infinite_\<omega>)
   moreover have "ordertype (ord_of_nat ` N) VWF = ordertype N less_than"
     by (auto intro: ordertype_inc_eq \<open>small N\<close>)
   ultimately show ?thesis
     by simp
 qed
 
 proposition ordertype_eq_ordertype:
   assumes r: "wf r" "total_on A r" "trans r" and "small A"
   assumes s: "wf s" "total_on B s" "trans s" and "small B"
   shows "ordertype A r = ordertype B s \<longleftrightarrow>
          (\<exists>f. bij_betw f A B \<and> (\<forall>x \<in> A. \<forall>y \<in> A. (f x, f y) \<in> s \<longleftrightarrow> (x,y) \<in> r))"
     (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   define \<gamma> where "\<gamma> = ordertype A r"
   have A: "bij_betw (ordermap A r) A (ordermap A r ` A)"
     by (meson ordermap_bij assms(4) bij_betw_def r)
   have B: "bij_betw (ordermap B s) B (ordermap B s ` B)"
     by (meson ordermap_bij assms(8) bij_betw_def s)
   define f where "f \<equiv> inv_into B (ordermap B s) o ordermap A r"
   show ?rhs
   proof (intro exI conjI)
     have bijA: "bij_betw (ordermap A r) A (elts \<gamma>)"
       unfolding \<gamma>_def using ordermap_bij \<open>small A\<close> r by blast
     moreover have bijB: "bij_betw (ordermap B s) B (elts \<gamma>)"
       by (simp add: L \<gamma>_def ordermap_bij \<open>small B\<close> s)
     ultimately show bij: "bij_betw f A B"
       unfolding f_def using bij_betw_comp_iff bij_betw_inv_into by blast
     have invB: "\<And>\<alpha>. \<alpha> \<in> elts \<gamma> \<Longrightarrow> ordermap B s (inv_into B (ordermap B s) \<alpha>) = \<alpha>"
       by (meson bijB bij_betw_inv_into_right)
     have ordermap_A_\<gamma>: "\<And>a. a \<in> A \<Longrightarrow> ordermap A r a \<in> elts \<gamma>"
       using bijA bij_betwE by auto
     have f_in_B: "\<And>a. a \<in> A \<Longrightarrow> f a \<in> B"
       using bij bij_betwE by fastforce
     show "\<forall>x\<in>A. \<forall>y\<in>A. (f x, f y) \<in> s \<longleftrightarrow> (x, y) \<in> r"
     proof (intro iffI ballI)
       fix x y
       assume "x \<in> A" "y \<in> A" and ins: "(f x, f y) \<in> s"
       then have "ordermap A r x < ordermap A r y"
         unfolding o_def 
         by (metis (mono_tags, lifting) f_def \<open>small B\<close> comp_apply f_in_B invB ordermap_A_\<gamma> ordermap_mono_less s(1) s(3))
       then show "(x, y) \<in> r"
         by (metis \<open>x \<in> A\<close> \<open>y \<in> A\<close> \<open>small A\<close> order.asym ordermap_mono_less r total_on_def)
     next
       fix x y
       assume "x \<in> A" "y \<in> A" and "(x, y) \<in> r"
       then have "ordermap A r x < ordermap A r y"
         by (simp add: \<open>small A\<close> ordermap_mono_less r)
       then have "(f y, f x) \<notin> s"
         by (metis (mono_tags, lifting) \<open>x \<in> A\<close> \<open>y \<in> A\<close> \<open>small B\<close> comp_apply f_def f_in_B invB order.asym ordermap_A_\<gamma> ordermap_mono_less s(1) s(3))
       moreover have "f y \<noteq> f x"
         by (metis \<open>(x, y) \<in> r\<close> \<open>x \<in> A\<close> \<open>y \<in> A\<close> bij bij_betw_inv_into_left r(1) wf_not_sym)
       ultimately show "(f x, f y) \<in> s"
         by (meson \<open>x \<in> A\<close> \<open>y \<in> A\<close> f_in_B s(2) total_on_def)
     qed
   qed
 next
   assume ?rhs
   then show ?lhs
     using assms ordertype_eqI  by blast
 qed
 
 corollary ordertype_eq_ordertype_iso:
   assumes r: "wf r" "total_on A r" "trans r" and "small A" and FA: "Field r = A"
   assumes s: "wf s" "total_on B s" "trans s" and "small B" and FB: "Field s = B"
   shows "ordertype A r = ordertype B s \<longleftrightarrow> (\<exists>f. iso r s f)"
     (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   then obtain f where "bij_betw f A B" "\<forall>x \<in> A. \<forall>y \<in> A. (f x, f y) \<in> s \<longleftrightarrow> (x,y) \<in> r"
     using assms ordertype_eq_ordertype by blast
   then show ?rhs
     using FA FB iso_iff2 by blast
 next
   assume ?rhs
   then show ?lhs
     using FA FB \<open>small A\<close> iso_imp_ordertype_eq_ordertype r by blast
 qed
 
 lemma Limit_ordertype_imp_Field_Restr:
   assumes Lim: "Limit (ordertype A r)" and r: "wf r" "total_on A r" and "small A"
   shows "Field (Restr r A) = A"
 proof -
   have "\<exists>y\<in>A. (x,y) \<in> r" if "x \<in> A" for x
   proof -
     let ?oy = "succ (ordermap A r x)"
     have \<section>: "?oy \<in> elts (ordertype A r)"
       by (simp add: Lim \<open>small A\<close> ordermap_in_ordertype succ_in_Limit_iff that)
     then have A: "inv_into A (ordermap A r) ?oy \<in> A"
       by (simp add: inv_into_ordermap)
     moreover have "(x, inv_into A (ordermap A r) ?oy) \<in> r"
     proof -
       have "ordermap A r x \<in> elts (ordermap A r (inv_into A (ordermap A r) ?oy))"
         by (metis "\<section>" elts_succ f_inv_into_f insert_iff ordermap_surj subsetD)
       then show ?thesis
         by (metis \<open>small A\<close> A converse_ordermap_mono r that)
     qed
     ultimately show ?thesis ..
   qed
   then have "A \<subseteq> Field (Restr r A)"
     by (auto simp: Field_def)
   then show ?thesis
     by (simp add: Field_Restr_subset subset_antisym)
 qed
 
 lemma ordertype_Field_Restr:
   assumes "wf r" "total_on A r" "trans r" "small A" "Field (Restr r A) = A"
   shows "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r"
   using assms by (force simp: ordertype_eq_ordertype wf_Restr total_on_def trans_Restr)
 
 proposition ordertype_eq_ordertype_iso_Restr:
   assumes r: "wf r" "total_on A r" "trans r" and "small A" and FA: "Field (Restr r A) = A"
   assumes s: "wf s" "total_on B s" "trans s" and "small B" and FB: "Field (Restr s B) = B"
   shows "ordertype A r = ordertype B s \<longleftrightarrow> (\<exists>f. iso (Restr r A) (Restr s B) f)"
     (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   then obtain f where "bij_betw f A B" "\<forall>x \<in> A. \<forall>y \<in> A. (f x, f y) \<in> s \<longleftrightarrow> (x,y) \<in> r"
     using assms ordertype_eq_ordertype by blast
   then show ?rhs
     using FA FB bij_betwE unfolding iso_iff2 by fastforce
 next
   assume ?rhs
   moreover
   have "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r"
     using FA \<open>small A\<close> ordertype_Field_Restr r by blast
   moreover
   have "ordertype (Field (Restr s B)) (Restr s B) = ordertype B s"
     using FB \<open>small B\<close> ordertype_Field_Restr s by blast
   ultimately show ?lhs
     using iso_imp_ordertype_eq_ordertype FA FB \<open>small A\<close> r
     by (fastforce intro: total_on_imp_Total_Restr trans_Restr wf_Int1)
 qed
 
 lemma ordermap_insert:
   assumes "Ord \<alpha>" and y: "Ord y" "y \<le> \<alpha>" and U: "U \<subseteq> elts \<alpha>"
   shows "ordermap (insert \<alpha> U) VWF y = ordermap U VWF y"
   using y
 proof (induction rule: Ord_induct)
   case (step y)
   then have 1: "{u \<in> U. (u, y) \<in> VWF} = elts y \<inter> U"
     apply (simp add: set_eq_iff)
     by (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less assms subsetD)
   have 2: "{u \<in> insert \<alpha> U. (u, y) \<in> VWF} = elts y \<inter> U"
     apply (simp add: set_eq_iff)
     by (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less assms leD step.hyps step.prems subsetD)
   show ?case
     using step
     apply (simp only: ordermap [OF wf_VWF, of _ y] 1 2)
     by (meson Int_lower1 Ord_is_Transset Sup.SUP_cong Transset_def assms(1) in_mono vsubsetD)
 qed
 
 lemma ordertype_insert:
   assumes "Ord \<alpha>" and U: "U \<subseteq> elts \<alpha>"
   shows "ordertype (insert \<alpha> U) VWF = succ (ordertype U VWF)"
 proof -
   have \<dagger>: "{y \<in> insert \<alpha> U. (y, \<alpha>) \<in> VWF} = U" "{y \<in> U. (y, \<alpha>) \<in> VWF} = U"
     using Ord_in_Ord OrdmemD assms by auto
   have eq: "\<And>x. x \<in> U \<Longrightarrow> ordermap (insert \<alpha> U) VWF x = ordermap U VWF x"
     by (meson Ord_in_Ord Ord_is_Transset Transset_def U assms(1) in_mono ordermap_insert)
   have "ordertype (insert \<alpha> U) VWF =
         ZFC_in_HOL.set (insert (ordermap U VWF \<alpha>) (ordermap U VWF ` U))"
     by (simp add: ordertype_def ordermap_insert assms eq)
   also have "\<dots> = succ (ZFC_in_HOL.set (ordermap U VWF ` U))"
     using "\<dagger>" U by (simp add: ordermap [OF wf_VWF, of _ \<alpha>] down succ_def vinsert_def)
   also have "\<dots> = succ (ordertype U VWF)"
     by (simp add: ordertype_def)
   finally show ?thesis .
 qed
 
 lemma finite_ordertype_le_card:
   assumes "finite A" "wf r" "trans r" 
   shows "ordertype A r \<le> ord_of_nat (card A)"
 proof -
   have "Ord (ordertype A r)"
     by (simp add: wf_Ord_ordertype assms)
   moreover have "ordermap A r ` A = elts (ordertype A r)"
     by (simp add: ordertype_def finite_imp_small \<open>finite A\<close>)
   moreover have "card (ordermap A r ` A) \<le> card A"
     using \<open>finite A\<close> card_image_le by blast
   ultimately show ?thesis
     by (metis Ord_linear_le Ord_ord_of_nat \<open>finite A\<close> card_ord_of_nat card_seteq finite_imageI less_eq_V_def)
 qed
 
 lemma ordertype_VWF_\<omega>:
   assumes "finite A"
   shows "ordertype A VWF \<in> elts \<omega>"
 proof -
   have "finite (ordermap A VWF ` A)"
     using assms by blast
   then have "ordertype A VWF < \<omega>"
     by (meson Ord_\<omega> OrdmemD trans_VWF wf_VWF assms finite_ordertype_le_card le_less_trans ord_of_nat_\<omega>)
   then show ?thesis
     by (simp add: Ord_mem_iff_lt)
 qed
 
 lemma ordertype_VWF_finite_nat:
   assumes "finite A"
   shows "ordertype A VWF = ord_of_nat (card A)"
   by (metis finite_imp_small ordermap_bij total_on_VWF wf_VWF \<omega>_def assms bij_betw_same_card card_ord_of_nat elts_of_set f_inv_into_f inf ordertype_VWF_\<omega>)
 
 lemma finite_ordertype_eq_card:
   assumes "small A" "wf r" "trans r" "total_on A r"
   shows "ordertype A r = ord_of_nat m \<longleftrightarrow> finite A \<and> card A = m"
   using ordermap_bij [OF \<open>wf r\<close>]
 proof -
   have *: "bij_betw (ordermap A r) A (elts (ordertype A r))"
     by (simp add: assms ordermap_bij)
   moreover have "card (ordermap A r ` A) = card A"
     by (meson bij_betw_def * card_image)
   ultimately show ?thesis
     using assms bij_betw_finite bij_betw_imp_surj_on finite_Ord_omega ordertype_VWF_finite_nat wf_Ord_ordertype by fastforce
 qed
 
 
 lemma ex_bij_betw_strict_mono_card:
   assumes "finite M" "M \<subseteq> ON"
   obtains h where "bij_betw h {..<card M} M" and "strict_mono_on h {..<card M}"
 proof -
   have bij: "bij_betw (ordermap M VWF) M (elts (card M))"
     using Finite_V \<open>finite M\<close> ordermap_bij ordertype_VWF_finite_nat by fastforce
   let ?h = "(inv_into M (ordermap M VWF)) \<circ> ord_of_nat"
   show thesis
   proof
     show bijh: "bij_betw ?h {..<card M} M"
     proof (rule bij_betw_trans)
       show "bij_betw ord_of_nat {..<card M} (elts (card M))"
         by (simp add: bij_betw_def elts_ord_of_nat inj_on_def)
       show "bij_betw (inv_into M (ordermap M VWF)) (elts (card M)) M"
         using Finite_V assms bij_betw_inv_into ordermap_bij ordertype_VWF_finite_nat by fastforce
     qed
     show "strict_mono_on ?h {..<card M}"
     proof -
       have "?h m < ?h n"
         if "m < n" "n < card M" for m n
       proof (rule ccontr)
         obtain mn: "m \<in> elts (ordertype M VWF)" "n \<in> elts (ordertype M VWF)"
           using \<open>m < n\<close> \<open>n < card M\<close> \<open>finite M\<close> ordertype_VWF_finite_nat by auto
         have ord: "Ord (?h m)" "Ord (?h n)"
           using bijh assms(2) bij_betwE that by fastforce+
         moreover
         assume "\<not> ?h m < ?h n"
         ultimately consider "?h m = ?h n" | "?h m > ?h n"
           using Ord_linear_lt by blast
         then show False
         proof cases
           case 1
           then have "m = n"
             by (metis inv_ordermap_mono_eq mn comp_apply ord_of_nat_inject)
           with \<open>m < n\<close> show False by blast 
         next
           case 2
           then have "ord_of_nat n \<le> ord_of_nat m"
             by (metis Finite_V mn assms comp_def inv_ordermap_VWF_mono_le less_imp_le)
           then show ?thesis
             using leD \<open>m < n\<close> by blast
         qed
       qed
       with assms show ?thesis
         by (auto simp: strict_mono_on_def)
     qed
   qed
 qed
 
 lemma ordertype_finite_less_than [simp]: 
   assumes "finite A" shows "ordertype A less_than = card A"
 proof -
   let ?M = "ord_of_nat ` A"
   obtain M: "finite ?M" "?M \<subseteq> ON"
     using Ord_ord_of_nat assms by blast
   have "ordertype A less_than = ordertype ?M VWF"
     by (rule ordertype_inc_eq [symmetric]) (use assms finite_imp_small total_on_def in \<open>force+\<close>)
   also have "\<dots> = card A"
   proof (subst ordertype_eq_iff)
     let ?M = "ord_of_nat ` A"
     obtain h where bijh: "bij_betw h {..<card A} ?M" and smh: "strict_mono_on h {..<card A}"
       by (metis M card_image ex_bij_betw_strict_mono_card inj_on_def ord_of_nat_inject)
     define f where "f \<equiv> ord_of_nat \<circ> inv_into {..<card A} h"
     show "\<exists>f. bij_betw f ?M (elts (card A)) \<and> (\<forall>x\<in>?M. \<forall>y\<in>?M. f x < f y \<longleftrightarrow> ((x, y) \<in> VWF))"
     proof (intro exI conjI ballI)
       have "bij_betw (ord_of_nat \<circ> inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})"
         by (meson UNIV_I bijh bij_betw_def bij_betw_inv_into bij_betw_subset bij_betw_trans inj_ord_of_nat subsetI)
       then show "bij_betw f ?M (elts (card A))"
         by (metis elts_ord_of_nat f_def)
     next
       fix x y
       assume xy: "x \<in> ?M" "y \<in> ?M"
       then obtain m n where "x = ord_of_nat m" "y = ord_of_nat n"
         by auto
       have "(f x < f y) \<longleftrightarrow> ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)"
         unfolding f_def using smh bij_betw_imp_surj_on [OF bijh] 
         apply simp
         by (metis (mono_tags, lifting) inv_into_into not_less_iff_gr_or_eq order.asym strict_mono_onD xy)
       also have "\<dots> = (x < y)"
         using bijh
         by (simp add: bij_betw_inv_into_right xy)
       also have "\<dots> \<longleftrightarrow> ((x, y) \<in> VWF)"
         using M(2) ON_imp_Ord xy by auto
       finally show "(f x < f y) \<longleftrightarrow> ((x, y) \<in> VWF)" . 
     qed 
   qed auto
   finally show ?thesis .
 qed
 
 
 subsection\<open>Cardinality of a set\<close>
 
 definition
   vcard :: "V\<Rightarrow>V"
   where "vcard a \<equiv> (LEAST i. Ord i \<and> elts i \<approx> elts a)"
 
 definition
   Card:: "V\<Rightarrow>bool" where "Card i \<equiv> i = vcard i"
 
 abbreviation CARD where "CARD \<equiv> Collect Card"
 
 lemma cardinal_cong: "elts x \<approx> elts y \<Longrightarrow> vcard x = vcard y"
   unfolding vcard_def by (meson eqpoll_sym eqpoll_trans)
 
 lemma Card_cardinal_eq: "Card \<kappa> \<Longrightarrow> vcard \<kappa> = \<kappa>"
   by (simp add: Card_def)
 
 lemma Card_is_Ord:
   assumes "Card \<kappa>" shows "Ord \<kappa>"
 proof -
   obtain \<alpha> where "Ord \<alpha>" "elts \<alpha> \<approx> elts \<kappa>"
     using Ord_ordertype ordertype_eqpoll by blast
   then have "Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)"
     by (metis Ord_Least)
   then show ?thesis
     using Card_def vcard_def assms by auto
 qed
 
 lemma cardinal_eqpoll: "elts (vcard a) \<approx> elts a"
   unfolding vcard_def
   using ordertype_eqpoll [of "elts a"] Ord_LeastI by (meson Ord_ordertype small_elts)
 
 lemma inj_into_vcard:
   obtains f where "f \<in> elts A \<rightarrow> elts (vcard A)" "inj_on f (elts A)"
   using cardinal_eqpoll [of A] inj_on_the_inv_into the_inv_into_onto
   by (fastforce simp: Pi_iff bij_betw_def eqpoll_def)
 
 lemma cardinal_idem [simp]: "vcard (vcard a) = vcard a"
   using cardinal_cong cardinal_eqpoll by blast
 
 text\<open>every natural number is a (finite) cardinal\<close>
 lemma nat_into_Card:
   assumes "\<alpha> \<in> elts \<omega>" shows "Card(\<alpha>)"
 proof (unfold Card_def vcard_def, rule sym)
   obtain n where n: "\<alpha> = ord_of_nat n"
     by (metis \<omega>_def assms elts_of_set imageE inf)
   have "Ord(\<alpha>)" using assms by auto
   moreover
   { fix \<beta>
     assume "\<beta> < \<alpha>" "Ord \<beta>" "elts \<beta> \<approx> elts \<alpha>"
     with n have "elts \<beta> \<approx> {..<n}"
       by (simp add: ord_of_nat_eq_initial [of n] eqpoll_trans inj_on_def inj_on_image_eqpoll_self)
     hence False using assms n  \<open>Ord \<beta>\<close> \<open>\<beta> < \<alpha>\<close> \<open>Ord(\<alpha>)\<close>
       by (metis \<open>elts \<beta> \<approx> elts \<alpha>\<close> card_seteq eqpoll_finite_iff eqpoll_iff_card finite_lessThan less_eq_V_def less_le_not_le order_refl)
   }
   ultimately
     show "(LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>"
       by (metis (no_types, lifting) Least_equality Ord_linear_le eqpoll_refl less_le_not_le)
   qed
 
 lemma Card_ord_of_nat [simp]: "Card (ord_of_nat n)"
   by (simp add: \<omega>_def nat_into_Card)
 
 lemma Card_0 [iff]: "Card 0"
   by (simp add: nat_into_Card)
 
 lemma CardI: "\<lbrakk>Ord i; \<And>j. \<lbrakk>j < i; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts i\<rbrakk> \<Longrightarrow> Card i"
   unfolding Card_def vcard_def
   by (metis Ord_Least Ord_linear_lt cardinal_eqpoll eqpoll_refl not_less_Ord_Least vcard_def)
 
 lemma vcard_0 [simp]: "vcard 0 = 0"
   using Card_0 Card_def by auto
 
 lemma Ord_cardinal [simp,intro!]: "Ord(vcard a)"
   unfolding vcard_def by (metis Card_def Card_is_Ord cardinal_cong cardinal_eqpoll vcard_def)
 
 text\<open>The cardinals are the initial ordinals.\<close>
 lemma Card_iff_initial: "Card \<kappa> \<longleftrightarrow> Ord \<kappa> \<and> (\<forall>\<alpha>. Ord \<alpha> \<and> \<alpha> < \<kappa> \<longrightarrow> ~ elts \<alpha> \<approx> elts \<kappa>)"
 proof -
   { fix j
     assume \<kappa>: "Card \<kappa>" "elts j \<approx> elts \<kappa>" "Ord j"
     assume "j < \<kappa>"
     also have "\<dots> = (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)" using \<kappa>
       by (simp add: Card_def vcard_def)
     finally have "j < (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)" .
     hence "False" using \<kappa>
       using not_less_Ord_Least by fastforce
   }
   then show ?thesis
     by (blast intro: CardI Card_is_Ord)
 qed
 
 lemma Card_\<omega> [iff]: "Card \<omega>"
 proof -
   have "\<And>\<alpha> f. \<lbrakk>\<alpha> \<in> elts \<omega>; bij_betw f (elts \<alpha>) (elts \<omega>)\<rbrakk> \<Longrightarrow> False"
   using bij_betw_finite finite_Ord_omega infinite_\<omega> by blast
   then show ?thesis
     by (meson CardI Ord_\<omega> Ord_mem_iff_lt eqpoll_def)
 qed
 
 lemma lt_Card_imp_lesspoll: "\<lbrakk>i < a; Card a; Ord i\<rbrakk> \<Longrightarrow> elts i \<prec> elts a"
   by (meson Card_iff_initial less_eq_V_def less_imp_le lesspoll_def subset_imp_lepoll)
 
 lemma lepoll_imp_Card_le:
   assumes "elts a \<lesssim> elts b" shows "vcard a \<le> vcard b"
 using Ord_cardinal [of a] Ord_cardinal [of b]
 proof (cases rule: Ord_linear_le)
   case le thus ?thesis .
 next
   case ge
   have "elts b \<approx> elts (vcard b)"
     by (simp add: cardinal_eqpoll eqpoll_sym)
   also have "\<dots> \<lesssim> elts (vcard a)"
     by (meson ge less_eq_V_def subset_imp_lepoll)
   also have "\<dots> \<approx> elts a"
     by (simp add: cardinal_eqpoll)
   finally have "elts b \<lesssim> elts a"  .
   hence "elts a \<approx> elts b"
     using assms lepoll_antisym by blast
   hence "vcard a = vcard b"
     by (rule cardinal_cong)
   thus ?thesis by simp
 qed
 
 lemma lepoll_cardinal_le: "\<lbrakk>elts A \<lesssim> elts i; Ord i\<rbrakk> \<Longrightarrow> vcard A \<le> i"
   by (metis Ord_Least Ord_linear2 dual_order.trans eqpoll_refl lepoll_imp_Card_le not_less_Ord_Least vcard_def)
 
 lemma cardinal_le_lepoll: "vcard A \<le> \<alpha> \<Longrightarrow> elts A \<lesssim> elts \<alpha>"
   by (meson cardinal_eqpoll eqpoll_sym lepoll_trans1 less_eq_V_def subset_imp_lepoll)
 
 lemma lesspoll_imp_Card_less:
   assumes "elts a \<prec> elts b" shows "vcard a < vcard b"
   by (metis assms cardinal_eqpoll eqpoll_sym eqpoll_trans le_neq_trans lepoll_imp_Card_le lesspoll_def)
 
 
 lemma Card_Union [simp,intro]:
   assumes A: "\<And>x. x \<in> A \<Longrightarrow> Card(x)" shows "Card(\<Squnion>A)"
 proof (rule CardI)
   show "Ord(\<Squnion>A)" using A
     by (simp add: Card_is_Ord Ord_Sup)
 next
   fix j
   assume j: "j < \<Squnion>A" "Ord j"
   hence "\<exists>c\<in>A. j < c \<and> Card(c)" using A
     by (meson Card_is_Ord Ord_linear2 ZFC_in_HOL.Sup_least leD)
   then obtain c where c: "c\<in>A" "j < c" "Card(c)"
     by blast
   hence jls: "elts j \<prec> elts c"
     using j(2) lt_Card_imp_lesspoll by blast
   { assume eqp: "elts j \<approx> elts (\<Squnion>A)"
     have  "elts c \<lesssim> elts (\<Squnion>A)" using c
       using Sup_V_def ZFC_in_HOL.Sup_upper j(1) less_eq_V_def subset_imp_lepoll by fastforce
     also have "... \<approx> elts j"  by (rule eqpoll_sym [OF eqp])
     also have "... \<prec> elts c"  by (rule jls)
     finally have "elts c \<prec> elts c" .
     hence False
       by auto
   } thus "\<not> elts j \<approx> elts (\<Squnion>A)" by blast
 qed
 
 lemma Card_UN: "(\<And>x. x \<in> A \<Longrightarrow> Card(K x)) ==> Card(Sup (K ` A))"
   by blast
 
 subsection\<open>Transfinite recursion for definitions based on the three cases of ordinals\<close>
 
 definition
   transrec3 :: "[V, [V,V]\<Rightarrow>V, [V,V\<Rightarrow>V]\<Rightarrow>V, V] \<Rightarrow> V" where
     "transrec3 a b c \<equiv>
        transrec (\<lambda>r x.
          if x=0 then a
          else if Limit x then c x (\<lambda>y \<in> elts x. r y)
          else b(pred x) (r (pred x)))"
 
 lemma transrec3_0 [simp]: "transrec3 a b c 0 = a"
   by (simp add: transrec transrec3_def)
 
 lemma transrec3_succ [simp]:
      "transrec3 a b c (succ i) = b i (transrec3 a b c i)"
   by (simp add: transrec transrec3_def)
 
 lemma transrec3_Limit [simp]:
      "Limit i \<Longrightarrow>  transrec3 a b c i = c i (\<lambda>j \<in> elts i. transrec3 a b c j)"
   unfolding transrec3_def
   by (subst transrec) auto
 
 
 subsection \<open>Cardinal Addition\<close>
 
 definition cadd :: "[V,V]\<Rightarrow>V"       (infixl \<open>\<oplus>\<close> 65)
   where "\<kappa> \<oplus> \<mu> \<equiv> vcard (\<kappa> \<Uplus> \<mu>)"
 
 subsubsection\<open>Cardinal addition is commutative\<close>
 
 lemma vsum_commute_eqpoll: "elts (a\<Uplus>b) \<approx> elts (b\<Uplus>a)"
 proof -
   have "bij_betw (\<lambda>z \<in> elts (a\<Uplus>b). sum_case Inr Inl z) (elts (a\<Uplus>b)) (elts (b\<Uplus>a))"
     unfolding bij_betw_def
   proof (intro conjI inj_onI)
     show "restrict (sum_case Inr Inl) (elts (a \<Uplus> b)) ` elts (a \<Uplus> b) = elts (b \<Uplus> a)"
      apply auto
      apply (metis (no_types) imageI sum_case_Inr sum_iff)
       by (metis Inl_in_sum_iff imageI sum_case_Inl)
   qed auto
   then show ?thesis
     using eqpoll_def by blast
 qed
 
 lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
   by (simp add: cadd_def cardinal_cong vsum_commute_eqpoll)
 
 subsubsection\<open>Cardinal addition is associative\<close>
 
 lemma sum_assoc_bij:
   "bij_betw (\<lambda>z \<in> elts ((a\<Uplus>b)\<Uplus>c). sum_case(sum_case Inl (\<lambda>y. Inr(Inl y))) (\<lambda>y. Inr(Inr y)) z)
       (elts ((a\<Uplus>b)\<Uplus>c)) (elts (a\<Uplus>(b\<Uplus>c)))"
   by (rule_tac f' = "sum_case (\<lambda>x. Inl (Inl x)) (sum_case (\<lambda>x. Inl (Inr x)) Inr)"
       in bij_betw_byWitness) auto
 
 lemma sum_assoc_eqpoll: "elts ((a\<Uplus>b)\<Uplus>c) \<approx> elts (a\<Uplus>(b\<Uplus>c))"
   unfolding eqpoll_def by (metis sum_assoc_bij)
 
 lemma elts_vcard_vsum_eqpoll: "elts (vcard (i \<Uplus> j)) \<approx> Inl ` elts i \<union> Inr ` elts j"
 proof -
   have "elts (i \<Uplus> j) \<approx> Inl ` elts i \<union> Inr ` elts j"
     by (simp add: elts_vsum)
   then show ?thesis
     using cardinal_eqpoll eqpoll_trans by blast
 qed
 
 lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
 proof (unfold cadd_def, rule cardinal_cong)
   have "elts (vcard(i \<Uplus> j) \<Uplus> k) \<approx> elts ((i \<Uplus> j) \<Uplus> k)"
     by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll intro: Un_eqpoll_cong)
   also have "\<dots>  \<approx> elts (i \<Uplus> (j \<Uplus> k))"
     by (rule sum_assoc_eqpoll)
   also have "\<dots>  \<approx> elts (i \<Uplus> vcard(j \<Uplus> k))"
     by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll [THEN eqpoll_sym] intro: Un_eqpoll_cong)
   finally show "elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))" .
 qed
 
 
 text\<open>0 is the identity for addition\<close>
 lemma vsum_0_eqpoll: "elts (0\<Uplus>a) \<approx> elts a"
   by (simp add: elts_vsum)
 
 lemma cadd_0 [simp]: "Card \<kappa> \<Longrightarrow> 0 \<oplus> \<kappa> = \<kappa>"
   by (metis Card_def cadd_def cardinal_cong vsum_0_eqpoll)
 
 lemma cadd_0_right [simp]: "Card \<kappa> \<Longrightarrow> \<kappa> \<oplus> 0 = \<kappa>"
   by (simp add: cadd_commute)
 
 lemma vsum_lepoll_self: "elts a \<lesssim> elts (a\<Uplus>b)"
   unfolding elts_vsum  by (meson Inl_iff Un_upper1 inj_onI lepoll_def)
 
 lemma cadd_le_self:
   assumes \<kappa>: "Card \<kappa>" shows "\<kappa> \<le> \<kappa> \<oplus> a"
 proof (unfold cadd_def)
   have "\<kappa> \<le> vcard \<kappa>"
     using Card_def \<kappa> by auto
   also have "\<dots> \<le> vcard (\<kappa> \<Uplus> a)"
     by (simp add: lepoll_imp_Card_le vsum_lepoll_self)
   finally show "\<kappa> \<le> vcard (\<kappa> \<Uplus> a)" .
 qed
 
 text\<open>Monotonicity of addition\<close>
 lemma cadd_le_mono: "\<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> \<kappa>' \<oplus> \<mu>' \<le> \<kappa> \<oplus> \<mu>"
   unfolding cadd_def
   by (metis (no_types) lepoll_imp_Card_le less_eq_V_def subset_imp_lepoll sum_subset_iff)
 
 subsection\<open>Cardinal multiplication\<close>
 
 definition cmult :: "[V,V]\<Rightarrow>V"       (infixl \<open>\<otimes>\<close> 70)
   where "\<kappa> \<otimes> \<mu> \<equiv> vcard (VSigma \<kappa> (\<lambda>z. \<mu>))"
 
 subsubsection\<open>Cardinal multiplication is commutative\<close>
 
 lemma prod_bij: "\<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk>
              \<Longrightarrow> bij_betw (\<lambda>(x, y). (f x, g y)) (A \<times> B) (C \<times> D)"
   apply (rule bij_betw_byWitness [where f' = "\<lambda>(x,y). (inv_into A f x, inv_into B g y)"])
      apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betwE)
   using bij_betwE bij_betw_inv_into apply blast+
   done
 
 lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
 proof -
   have "(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)"
     by (simp add: inj_on_vpair times_commute_eqpoll)
   then show ?thesis
     unfolding cmult_def
     using cardinal_cong elts_VSigma by auto
 qed
 
 subsubsection\<open>Cardinal multiplication is associative\<close>
 
 lemma elts_vcard_VSigma_eqpoll: "elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j"
 proof -
   have "elts (vtimes i j) \<approx> elts i \<times> elts j"
     by (simp add: elts_VSigma)
   then show ?thesis
     using cardinal_eqpoll eqpoll_trans by blast
 qed
 
 lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
   unfolding cmult_def
 proof (rule cardinal_cong)
   have "elts (vcard (vtimes i j)) \<times> elts k \<approx> (elts i \<times> elts j) \<times> elts k"
     by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll)
   also have "\<dots>  \<approx> elts i \<times> (elts j \<times> elts k)"
     by (rule times_assoc_eqpoll)
   also have "\<dots>  \<approx> elts i \<times> elts (vcard (vtimes j k))"
     by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll eqpoll_sym)
   finally show "elts (VSigma (vcard (vtimes i j)) (\<lambda>z. k)) \<approx> elts (VSigma i (\<lambda>z. vcard (vtimes j k)))"
     by (simp add: elts_VSigma)
 qed
 
 subsubsection\<open>Cardinal multiplication distributes over addition\<close>
 
 lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
   unfolding cadd_def cmult_def
 proof (rule cardinal_cong)
 have "elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vsum i j)) \<times> elts k"
   using cardinal_eqpoll elts_vcard_VSigma_eqpoll eqpoll_sym eqpoll_trans by blast
   also have "\<dots> \<approx> (Inl ` elts i \<union> Inr ` elts j) \<times> elts k"
     using elts_vcard_vsum_eqpoll times_eqpoll_cong by blast
   also have "\<dots> \<approx> (Inl ` elts i) \<times> elts k \<union> (Inr ` elts j) \<times> elts k"
     by (simp add: Sigma_Un_distrib1)
   also have "\<dots>  \<approx> elts (vtimes i k \<Uplus> vtimes j k)"
     unfolding Plus_def
     by (auto simp: elts_vsum elts_VSigma disjnt_iff intro!: Un_eqpoll_cong times_eqpoll_cong)
   also have "\<dots>  \<approx> elts (vcard (vtimes i k \<Uplus> vtimes j k))"
     by (simp add: cardinal_eqpoll eqpoll_sym)
   also have "\<dots>  \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))"
     by (metis cadd_assoc cadd_def cardinal_cong cardinal_eqpoll vsum_0_eqpoll vsum_commute_eqpoll)
   finally show "elts (VSigma (vcard (i \<Uplus> j)) (\<lambda>z. k))
              \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))" .
 qed
 
 text\<open>Multiplication by 0 yields 0\<close>
 lemma cmult_0 [simp]: "0 \<otimes> i = 0"
   using Card_0 Card_def cmult_def by auto
 
 text\<open>1 is the identity for multiplication\<close>
 lemma cmult_1 [simp]: assumes "Card \<kappa>" shows "1 \<otimes> \<kappa> = \<kappa>"
 proof -
   have "elts (vtimes (set {0}) \<kappa>) \<approx> elts \<kappa>"
     by (auto simp: elts_VSigma intro!: times_singleton_eqpoll)
   then show ?thesis
     by (metis Card_def assms cardinal_cong cmult_def elts_1 set_of_elts)
 qed
 
 subsection\<open>Some inequalities for multiplication\<close>
 
 lemma cmult_square_le: assumes "Card \<kappa>" shows "\<kappa> \<le> \<kappa> \<otimes> \<kappa>"
 proof -
   have "elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)"
     using times_square_lepoll [of "elts \<kappa>"] cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym lepoll_trans2
     by fastforce
   then show ?thesis
     using Card_def assms cmult_def lepoll_cardinal_le by fastforce
 qed
 
 text\<open>Multiplication by a non-empty set\<close>
 lemma cmult_le_self: assumes "Card \<kappa>" "\<alpha> \<noteq> 0" shows "\<kappa> \<le> \<kappa> \<otimes> \<alpha>"
 proof -
   have "\<kappa> = vcard \<kappa>"
     using Card_def \<open>Card \<kappa>\<close> by blast
   also have "\<dots> \<le> vcard (vtimes \<kappa> \<alpha>)"
     apply (rule lepoll_imp_Card_le)
     apply (simp add: elts_VSigma)
     by (metis ZFC_in_HOL.ext \<open>\<alpha> \<noteq> 0\<close> elts_0 lepoll_times1)
   also have "\<dots> = \<kappa> \<otimes> \<alpha>"
     by (simp add: cmult_def)
   finally show ?thesis .
 qed
 
 
 text\<open>Monotonicity of multiplication\<close>
 lemma cmult_le_mono: "\<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> \<kappa>' \<otimes> \<mu>' \<le> \<kappa> \<otimes> \<mu>"
   unfolding cmult_def
   by (auto simp: elts_VSigma intro!: lepoll_imp_Card_le times_lepoll_mono subset_imp_lepoll)
 
 
 subsection\<open>The finite cardinals\<close>
 
 lemma succ_lepoll_succD: "elts (succ(m)) \<lesssim> elts (succ(n)) \<Longrightarrow> elts m \<lesssim> elts n"
   by (simp add: insert_lepoll_insertD)
 
 
 text\<open>Congruence law for @{text succ} under equipollence\<close>
 lemma succ_eqpoll_cong: "elts a \<approx> elts b \<Longrightarrow> elts (succ(a)) \<approx> elts (succ(b))"
   by (simp add: succ_def insert_eqpoll_cong)
 
 lemma sum_succ_eqpoll: "elts (succ a \<Uplus> b) \<approx> elts (succ(a\<Uplus>b))"
   unfolding eqpoll_def
 proof (rule exI)
   let ?f = "\<lambda>z. if z=Inl a then a\<Uplus>b else z"
   let ?g = "\<lambda>z. if z=a\<Uplus>b then Inl a else z"
   show "bij_betw ?f (elts (succ a \<Uplus> b)) (elts (succ (a \<Uplus> b)))"
     apply (rule bij_betw_byWitness [where f' = ?g], auto)
      apply (metis Inl_in_sum_iff mem_not_refl)
     by (metis Inr_in_sum_iff mem_not_refl)
 qed
 
 lemma cadd_succ: "succ m \<oplus> n = vcard (succ(m \<oplus> n))"
 proof (unfold cadd_def)
   have [intro]: "elts (m \<Uplus> n) \<approx> elts (vcard (m \<Uplus> n))"
     using cardinal_eqpoll eqpoll_sym by blast
   have "vcard (succ m \<Uplus> n) = vcard (succ(m \<Uplus> n))"
     by (rule sum_succ_eqpoll [THEN cardinal_cong])
   also have "\<dots> = vcard (succ(vcard (m \<Uplus> n)))"
     by (blast intro: succ_eqpoll_cong cardinal_cong)
   finally show "vcard (succ m \<Uplus> n) = vcard (succ(vcard (m \<Uplus> n)))" .
 qed
 
 lemma nat_cadd_eq_add: "ord_of_nat m \<oplus> ord_of_nat n = ord_of_nat (m + n)"
 proof (induct m)
   case (Suc m) thus ?case
     by (metis Card_def Card_ord_of_nat add_Suc cadd_succ ord_of_nat.simps(2))
 qed auto
 
 lemma vcard_disjoint_sup:
   assumes "x \<sqinter> y = 0" shows "vcard (x \<squnion> y) = vcard x \<oplus> vcard y"
 proof -
   have "elts (x \<squnion> y) \<approx> elts (x \<Uplus> y)"
     unfolding eqpoll_def
   proof (rule exI)
     let ?f = "\<lambda>z. if z \<in> elts x then Inl z else Inr z"
     let ?g = "sum_case id id"
     show "bij_betw ?f (elts (x \<squnion> y)) (elts (x \<Uplus> y))"
       by (rule bij_betw_byWitness [where f' = ?g]) (use assms V_disjoint_iff in auto)
   qed
   then show ?thesis
     by (metis cadd_commute cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll cadd_assoc)
 qed
 
 
 subsection\<open>Infinite cardinals\<close>
 
 definition InfCard :: "V\<Rightarrow>bool"
   where "InfCard \<kappa> \<equiv> Card \<kappa> \<and> \<omega> \<le> \<kappa>"
 
 lemma InfCard_iff: "InfCard \<kappa> \<longleftrightarrow> Card \<kappa> \<and> infinite (elts \<kappa>)"
 proof (cases "\<omega> \<le> \<kappa>")
   case True
   then show ?thesis
     using inj_ord_of_nat lepoll_def less_eq_V_def
     by (auto simp: InfCard_def \<omega>_def infinite_le_lepoll)
 next
   case False
   then show ?thesis
     using Card_iff_initial InfCard_def infinite_Ord_omega by blast
 qed
 
 lemma InfCard_ge_ord_of_nat:
   assumes "InfCard \<kappa>" shows "ord_of_nat n \<le> \<kappa>"
   using InfCard_def assms ord_of_nat_le_omega by blast
 
 lemma InfCard_not_0[iff]: "\<not> InfCard 0"
   by (simp add: InfCard_iff)
 
 definition
   csucc :: "V\<Rightarrow>V"
   where "csucc \<kappa> \<equiv> LEAST \<kappa>'. Ord \<kappa>' \<and> (Card \<kappa>' \<and> \<kappa> < \<kappa>')"
 
 
 lemma less_vcard_VPow: "vcard A < vcard (VPow A)"
 proof (rule lesspoll_imp_Card_less)
   show "elts A \<prec> elts (VPow A)"
     by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self)
 qed
 
 lemma greater_Card:
   assumes "Card \<kappa>" shows "\<kappa> < vcard (VPow \<kappa>)"
 proof -
   have "\<kappa> = vcard \<kappa>"
     using Card_def assms by blast
   also have "\<dots> < vcard (VPow \<kappa>)"
   proof (rule lesspoll_imp_Card_less)
     show "elts \<kappa> \<prec> elts (VPow \<kappa>)"
       by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self)
   qed
   finally show ?thesis .
 qed
 
 lemma
   assumes "Card \<kappa>"
   shows Card_csucc [simp]: "Card (csucc \<kappa>)" and less_csucc [simp]: "\<kappa> < csucc \<kappa>"
 proof -
   have "Card (csucc \<kappa>) \<and> \<kappa> < csucc \<kappa>"
     unfolding csucc_def
   proof (rule Ord_LeastI2)
     show "Card (vcard (VPow \<kappa>)) \<and> \<kappa> < (vcard (VPow \<kappa>))"
       using Card_def assms greater_Card by auto
   qed auto
   then show "Card (csucc \<kappa>)" "\<kappa> < csucc \<kappa>"
     by auto
 qed
 
 lemma le_csucc:
   assumes "Card \<kappa>" shows "\<kappa> \<le> csucc \<kappa>"
   by (simp add: assms less_csucc less_imp_le)
 
 
 lemma csucc_le: "\<lbrakk>Card \<mu>; \<kappa> \<in> elts \<mu>\<rbrakk> \<Longrightarrow> csucc \<kappa> \<le> \<mu>"
   unfolding csucc_def
   by (simp add: Card_is_Ord Ord_Least_le OrdmemD)
 
 lemma finite_csucc: "a \<in> elts \<omega> \<Longrightarrow> csucc a = succ a"
   unfolding csucc_def
   proof (rule Least_equality)
   show "Ord (ZFC_in_HOL.succ a) \<and> Card (ZFC_in_HOL.succ a) \<and> a < ZFC_in_HOL.succ a"
     if "a \<in> elts \<omega>"
     using that by (auto simp: less_V_def less_eq_V_def nat_into_Card)
   show "ZFC_in_HOL.succ a \<le> y"
     if "a \<in> elts \<omega>"
       and "Ord y \<and> Card y \<and> a < y"
     for y :: V
     using that
     using Ord_mem_iff_lt dual_order.strict_implies_order by fastforce
 qed
 
 lemma Finite_imp_cardinal_cons [simp]:
   assumes FA: "finite A" and a: "a \<notin> A"
   shows "vcard (set (insert a A)) = csucc(vcard (set A))"
 proof -
   show ?thesis
     unfolding csucc_def
   proof (rule Least_equality [THEN sym])
     have "small A"
       by (simp add: FA Finite_V)
     then have "\<not> elts (set A) \<approx> elts (set (insert a A))"
       using FA a eqpoll_imp_lepoll eqpoll_sym finite_insert_lepoll by fastforce
     then show "Ord (vcard (set (insert a A))) \<and> Card (vcard (set (insert a A))) \<and> vcard (set A) < vcard (set (insert a A))"
       by (simp add: Card_def lesspoll_imp_Card_less lesspoll_def subset_imp_lepoll subset_insertI)
     show "vcard (set (insert a A)) \<le> i"
       if "Ord i \<and> Card i \<and> vcard (set A) < i" for i
     proof -
       have "elts (vcard (set A)) \<approx> A"
         by (metis FA finite_imp_small cardinal_eqpoll elts_of_set)
       then have less: "A \<prec> elts i"
         using eq_lesspoll_trans eqpoll_sym lt_Card_imp_lesspoll that by blast
       show ?thesis
         using that less by (auto simp: less_imp_insert_lepoll lepoll_cardinal_le)
     qed
   qed
 qed
 
 lemma vcard_finite_set: "finite A \<Longrightarrow> vcard (set A) = ord_of_nat (card A)"
   by (induction A rule: finite_induct) (auto simp: set_empty \<omega>_def finite_csucc)
 
 lemma lt_csucc_iff:
   assumes "Ord \<alpha>" "Card \<kappa>"
   shows "\<alpha> < csucc \<kappa> \<longleftrightarrow> vcard \<alpha> \<le> \<kappa>"
 proof
   show "vcard \<alpha> \<le> \<kappa>" if "\<alpha> < csucc \<kappa>"
   proof -
     have "vcard \<alpha> \<le> csucc \<kappa>"
       by (meson \<open>Ord \<alpha>\<close> dual_order.trans lepoll_cardinal_le lepoll_refl less_le_not_le that)
     then show ?thesis
       by (metis (no_types) Card_def Card_iff_initial Ord_linear2 Ord_mem_iff_lt assms cardinal_eqpoll cardinal_idem csucc_le eq_iff eqpoll_sym that)
   qed
   show "\<alpha> < csucc \<kappa>" if "vcard \<alpha> \<le> \<kappa>"
   proof -
     have "\<not> csucc \<kappa> \<le> \<alpha>"
       using that
       by (metis Card_csucc Card_def assms(2) le_less_trans lepoll_imp_Card_le less_csucc less_eq_V_def less_le_not_le subset_imp_lepoll)
     then show ?thesis
       by (meson Card_csucc Card_is_Ord Ord_linear2 assms)
   qed
 qed
 
 lemma Card_lt_csucc_iff: "\<lbrakk>Card \<kappa>'; Card \<kappa>\<rbrakk> \<Longrightarrow> (\<kappa>' < csucc \<kappa>) = (\<kappa>' \<le> \<kappa>)"
   by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
 
 lemma InfCard_csucc: "InfCard \<kappa> \<Longrightarrow> InfCard (csucc \<kappa>)"
   using InfCard_def le_csucc by auto
 
 
 text\<open>Kunen's Lemma 10.11\<close>
 lemma InfCard_is_Limit:
   assumes "InfCard \<kappa>" shows "Limit \<kappa>"
   proof (rule non_succ_LimitI)
   show "\<kappa> \<noteq> 0"
     using InfCard_def assms mem_not_refl by blast
   show "Ord \<kappa>"
     using Card_is_Ord InfCard_def assms by blast
   show "ZFC_in_HOL.succ y \<noteq> \<kappa>" for y
   proof
     assume "succ y = \<kappa>"
     then have "Card (succ y)"
       using InfCard_def assms by auto
     moreover have "\<omega> \<le> y"
       by (metis InfCard_iff Ord_in_Ord \<open>Ord \<kappa>\<close> \<open>ZFC_in_HOL.succ y = \<kappa>\<close> assms elts_succ finite_insert infinite_Ord_omega insertI1)
     moreover have "elts y \<approx> elts (succ y)"
       using InfCard_iff \<open>ZFC_in_HOL.succ y = \<kappa>\<close> assms eqpoll_sym infinite_insert_eqpoll by fastforce
     ultimately show False
       by (metis Card_iff_initial Ord_in_Ord OrdmemD elts_succ insertI1)
   qed
 qed
 
 
 subsection\<open>Toward's Kunen's Corollary 10.13 (1)\<close>
 
 text\<open>Kunen's Theorem 10.12\<close>
 lemma InfCard_csquare_eq:
   assumes "InfCard(\<kappa>)" shows "\<kappa> \<otimes> \<kappa> = \<kappa>"
   using infinite_times_eqpoll_self [of "elts \<kappa>"] assms
   unfolding InfCard_iff Card_def
   by (metis cardinal_cong cardinal_eqpoll cmult_def elts_vcard_VSigma_eqpoll eqpoll_trans)
 
 lemma InfCard_le_cmult_eq:
   assumes "InfCard \<kappa>" "\<mu> \<le> \<kappa>" "\<mu> \<noteq> 0"
   shows "\<kappa> \<otimes> \<mu> = \<kappa>"
 proof (rule order_antisym)
   have "\<kappa> \<otimes> \<mu> \<le> \<kappa> \<otimes> \<kappa>"
     by (simp add: assms(2) cmult_le_mono)
   also have "\<dots> \<le> \<kappa>"
     by (simp add: InfCard_csquare_eq assms(1))
   finally show "\<kappa> \<otimes> \<mu> \<le> \<kappa>" .
   show "\<kappa> \<le> \<kappa> \<otimes> \<mu>"
     using InfCard_def assms(1) assms(3) cmult_le_self by auto
 qed
 
 text\<open>Kunen's Corollary 10.13 (1), for cardinal multiplication\<close>
 lemma InfCard_cmult_eq: "\<lbrakk>InfCard \<kappa>; InfCard \<mu>\<rbrakk> \<Longrightarrow> \<kappa> \<otimes> \<mu> = \<kappa> \<squnion> \<mu>"
   by (metis Card_is_Ord InfCard_def InfCard_le_cmult_eq Ord_linear_le cmult_commute inf_sup_aci(5) mem_not_refl sup.orderE sup_V_0_right zero_in_omega)
 
 lemma cmult_succ:
   "succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
   unfolding cmult_def cadd_def
 proof (rule cardinal_cong)
   have "elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts n <+> elts m \<times> elts n"
     by (simp add: elts_VSigma prod_insert_eqpoll)
   also have "\<dots> \<approx> elts (n \<Uplus> vcard (vtimes m n))"
     unfolding elts_VSigma elts_vsum Plus_def
   proof (rule Un_eqpoll_cong)
     show "(Sum_Type.Inr ` (elts m \<times> elts n)::(V + V \<times> V) set) \<approx> Inr ` elts (vcard (vtimes m n))"
       by (simp add: elts_vcard_VSigma_eqpoll eqpoll_sym)
   qed (auto simp: disjnt_def)
   finally show "elts (vtimes (ZFC_in_HOL.succ m) n) \<approx> elts (n \<Uplus> vcard (vtimes m n))" .
 qed
 
 lemma cmult_2:
   assumes "Card n" shows "ord_of_nat 2 \<otimes> n = n \<oplus> n"
 proof -
   have "ord_of_nat 2 = succ (succ 0)"
     by force
   then show ?thesis
     by (simp add: cmult_succ assms)
 qed
 
 lemma InfCard_cdouble_eq:
   assumes "InfCard \<kappa>" shows "\<kappa> \<oplus> \<kappa> = \<kappa>"
 proof -
   have "\<kappa> \<oplus> \<kappa> = \<kappa> \<otimes> ord_of_nat 2"
     using InfCard_def assms cmult_2 cmult_commute by auto
   also have "\<dots> = \<kappa>"
     by (simp add: InfCard_le_cmult_eq InfCard_ge_ord_of_nat assms)
   finally show ?thesis .
 qed
 
 text\<open>Corollary 10.13 (1), for cardinal addition\<close>
 lemma InfCard_le_cadd_eq: "\<lbrakk>InfCard \<kappa>; \<mu> \<le> \<kappa>\<rbrakk> \<Longrightarrow> \<kappa> \<oplus> \<mu> = \<kappa>"
   by (metis InfCard_cdouble_eq InfCard_def antisym cadd_le_mono cadd_le_self)
 
 lemma InfCard_cadd_eq: "\<lbrakk>InfCard \<kappa>; InfCard \<mu>\<rbrakk> \<Longrightarrow> \<kappa> \<oplus> \<mu> = \<kappa> \<squnion> \<mu>"
   by (metis Card_iff_initial InfCard_def InfCard_le_cadd_eq Ord_linear_le cadd_commute sup.absorb2 sup.orderE)
 
 
 subsection \<open>The Aleph-seqence\<close>
 
 text \<open>This is the well-known transfinite enumeration of the cardinal numbers.\<close>
 
 definition
   Aleph :: "V \<Rightarrow> V"   (\<open>\<aleph>_\<close> [90] 90) 
   where "Aleph \<equiv> transrec3 \<omega> (\<lambda>x r. csucc(r)) (\<lambda>i r . \<Squnion> (r ` elts i))"
 
 lemma Card_Aleph [simp, intro]:
      "Ord \<alpha> \<Longrightarrow> Card(Aleph \<alpha>)"
 by (induction \<alpha> rule: Ord_induct3) (auto simp: Aleph_def)
 
 lemma Aleph_0 [simp]: "\<aleph>0 = \<omega>"
   by (simp add: Aleph_def)
 
 lemma Aleph_succ [simp]: "\<aleph>(succ x) = csucc (\<aleph> x)"
   by (simp add: Aleph_def)
 
 lemma Aleph_Limit: "Limit \<gamma> \<Longrightarrow> \<aleph> \<gamma> = \<Squnion> (Aleph ` elts \<gamma>)"
   by (simp add: Aleph_def)
 
 lemma mem_Aleph_succ: "Ord \<alpha> \<Longrightarrow> \<aleph>(\<alpha>) \<in> elts (\<aleph>(succ \<alpha>))"
   by (simp add: Card_is_Ord Ord_mem_iff_lt)
 
 lemma Aleph_increasing:
   assumes ab: "\<alpha> < \<beta>" "Ord \<alpha>" "Ord \<beta>" shows "Aleph(\<alpha>) < Aleph(\<beta>)"
 proof -
   { fix x
     have "\<lbrakk>Ord x; x \<in> elts \<beta>\<rbrakk> \<Longrightarrow> Aleph(x) \<in> elts (Aleph \<beta>)"
       using \<open>Ord \<beta>\<close>
     proof (induct \<beta> arbitrary: x rule: Ord_induct3)
       case 0 thus ?case by simp
     next
       case (succ \<beta>)
       then consider "x = \<beta>" |"x \<in> elts \<beta>"
         using OrdmemD by auto
       then show ?case
       proof cases
         case 1
         then show ?thesis
           by (simp add: Card_is_Ord Ord_mem_iff_lt succ.hyps(1))
       next
         case 2
         with succ show ?thesis
           by (metis Aleph_succ Card_Aleph le_csucc vsubsetD)
       qed
     next
       case (Limit \<gamma>)
       hence sc: "succ x \<in> elts \<gamma>"
         by (simp add: Limit_def Ord_mem_iff_lt)
       hence "\<aleph> x \<in> elts (\<Squnion> (Aleph ` elts \<gamma>))" 
         using Limit
         by blast
       thus ?case using Limit
         by (simp add: Aleph_Limit)
     qed
   } thus ?thesis using ab
     by (simp add: Card_is_Ord Ord_mem_iff_lt)
 qed
 
 lemma countable_iff_le_Aleph0: "countable (elts A) \<longleftrightarrow> vcard A \<le> \<aleph>0"
 proof
   show "vcard A \<le> \<aleph>0"
     if "countable (elts A)"
   proof (cases "finite (elts A)")
     case True
     then show ?thesis
       using vcard_finite_set by fastforce
   next
     case False
     then have "elts \<omega> \<approx> elts A"
       using countableE_infinite [OF that]     
       by (simp add: eqpoll_def \<omega>_def) (meson bij_betw_def bij_betw_inv bij_betw_trans inj_ord_of_nat)
     then show ?thesis
       using Card_\<omega> Card_def cardinal_cong vcard_def by auto
   qed
   show "countable (elts A)"
     if "vcard A \<le> \<aleph>0"
   proof -
     have "elts A \<lesssim> elts \<omega>"
       using cardinal_le_lepoll [OF that] by simp
     then show ?thesis
       by (simp add: countable_iff_lepoll \<omega>_def inj_ord_of_nat)
   qed
 qed
 
 subsection \<open>The ordinal @{term "\<omega>1"}\<close>
 
 abbreviation "\<omega>1 \<equiv> Aleph 1"
 
 lemma Ord_\<omega>1 [simp]: "Ord \<omega>1"
   by (simp add: Card_is_Ord)
 
 lemma omega_\<omega>1 [iff]: "\<omega> \<in> elts \<omega>1"
   using mem_Aleph_succ one_V_def by fastforce
 
 lemma ord_of_nat_\<omega>1 [iff]: "ord_of_nat n \<in> elts \<omega>1"
   using Ord_\<omega>1 Ord_trans by blast
 
 lemma countable_iff_less_\<omega>1:
   assumes "Ord \<alpha>"
   shows "countable (elts \<alpha>) \<longleftrightarrow> \<alpha> < \<omega>1"
   by (simp add: assms countable_iff_le_Aleph0 lt_csucc_iff one_V_def)
 
 lemma less_\<omega>1_imp_countable:
   assumes "\<alpha> \<in> elts \<omega>1"
   shows "countable (elts \<alpha>)"
   using Ord_\<omega>1 Ord_in_Ord OrdmemD assms countable_iff_less_\<omega>1 by blast
 
 lemma \<omega>1_gt0 [simp]: "\<omega>1 > 0"
   using Ord_\<omega>1 Ord_trans OrdmemD by blast
 
 lemma \<omega>1_gt1 [simp]: "\<omega>1 > 1"
   using Ord_\<omega>1 OrdmemD \<omega>_gt1 less_trans by blast
 
 lemma Limit_\<omega>1 [simp]: "Limit \<omega>1"
   by (simp add: InfCard_def InfCard_is_Limit le_csucc one_V_def)
 
 end