diff --git a/thys/ZFC_in_HOL/Kirby.thy b/thys/ZFC_in_HOL/Kirby.thy
--- a/thys/ZFC_in_HOL/Kirby.thy
+++ b/thys/ZFC_in_HOL/Kirby.thy
@@ -1,1491 +1,1529 @@
 section \<open>Addition and Multiplication of Sets\<close>
 
 theory Kirby
   imports ZFC_Cardinals
 
 begin
 
 subsection \<open>Generalised Addition\<close>
 
 text \<open>Source: Laurence Kirby, Addition and multiplication of sets
       Math. Log. Quart. 53, No. 1, 52-65 (2007) / DOI 10.1002/malq.200610026
       @{url "http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf"}\<close>
 
 subsubsection \<open>Addition is a monoid\<close>
 
 instantiation V :: plus
 begin
 
 text\<open>This definition is credited to Tarski\<close>
 definition plus_V :: "V \<Rightarrow> V \<Rightarrow> V"
   where "plus_V x \<equiv> transrec (\<lambda>f z. x \<squnion> set (f ` elts z))"
 
 instance ..
 end
 
 definition lift :: "V \<Rightarrow> V \<Rightarrow> V"
   where "lift x y \<equiv> set (plus x ` elts y)"
 
 lemma plus: "x + y = x \<squnion> set ((+)x ` elts y)"
   unfolding plus_V_def  by (subst transrec) auto
 
 lemma plus_eq_lift: "x + y = x \<squnion> lift x y"
   unfolding lift_def  using plus by blast
 
 text\<open>Lemma 3.2\<close>
 lemma lift_sup_distrib: "lift x (a \<squnion> b) = lift x a \<squnion> lift x b"
   by (simp add: image_Un lift_def sup_V_def)
 
 lemma lift_Sup_distrib: "small Y \<Longrightarrow> lift x (\<Squnion> Y) = \<Squnion> (lift x ` Y)"
   by (auto simp: lift_def Sup_V_def image_Union)
 
 lemma add_Sup_distrib:
   fixes x::V shows "y \<noteq> 0 \<Longrightarrow> x + (SUP z\<in>elts y. f z) = (SUP z\<in>elts y. x + f z)"
   by (auto simp: plus_eq_lift SUP_sup_distrib lift_Sup_distrib image_image)
 
 lemma Limit_add_Sup_distrib:
   fixes x::V shows "Limit \<alpha> \<Longrightarrow> x + (SUP z\<in>elts \<alpha>. f z) = (SUP z\<in>elts \<alpha>. x + f z)"
   using add_Sup_distrib by force
 
 text\<open>Proposition 3.3(ii)\<close>
 instantiation V :: monoid_add
 begin
 instance
 proof
   show "a + b + c = a + (b + c)" for a b c :: V
   proof (induction c rule: eps_induct)
     case (step c)
     have "(a+b) + c = a + b \<squnion> set ((+) (a + b) ` elts c)"
       by (metis plus)
     also have "\<dots> = a \<squnion> lift a b \<squnion> set ((\<lambda>u. a + (b+u)) ` elts c)"
       using plus_eq_lift step.IH by auto
     also have "\<dots> = a \<squnion> lift a (b + c)"
     proof -
       have "lift a b \<squnion> set ((\<lambda>u. a + (b + u)) ` elts c) = lift a (b + c)"
         unfolding lift_def
         by (metis elts_of_set image_image lift_def lift_sup_distrib plus_eq_lift replacement small_elts)
       then show ?thesis
         by (simp add: sup_assoc)
     qed
     also have "\<dots> = a + (b + c)"
       using plus_eq_lift by auto
     finally show ?case .
   qed
   show "0 + x = x" for x :: V
   proof (induction rule: eps_induct)
     case (step x)
     then show ?case
       by (subst plus) auto
   qed
   show "x + 0 = x" for x :: V
     by (subst plus) auto
 qed
 end
 
 lemma lift_0 [simp]: "lift 0 x = x"
   by (simp add: lift_def)
 
 lemma lift_by0 [simp]: "lift x 0 = 0"
   by (simp add: lift_def)
 
 lemma lift_by1 [simp]: "lift x 1 = set{x}"
   by (simp add: lift_def)
 
 lemma add_eq_0_iff [simp]:
   fixes x y::V
   shows "x+y = 0 \<longleftrightarrow> x=0 \<and> y=0"
   proof safe
   show "x = 0" if "x + y = 0"
     by (metis that le_imp_less_or_eq not_less_0 plus sup_ge1)
   then show "y = 0" if "x + y = 0"
     using that by auto
 qed auto
 
 lemma plus_vinsert: "x + vinsert z y = vinsert (x+z) (x + y)"
 proof -
   have f1: "elts (x + y) = elts x \<union> (+) x ` elts y"
     by (metis elts_of_set lift_def plus_eq_lift replacement small_Un small_elts sup_V_def)
   moreover have "lift x (vinsert z y) = set ((+) x ` elts (set (insert z (elts y))))"
     using vinsert_def lift_def by presburger
   ultimately show ?thesis
     by (simp add: vinsert_def plus_eq_lift sup_V_def)
 qed
 
 lemma plus_V_succ_right: "x + succ y = succ (x + y)"
   by (metis plus_vinsert succ_def)
 
 lemma succ_eq_add1: "succ x = x + 1"
   by (simp add: plus_V_succ_right one_V_def)
 
 lemma ord_of_nat_add: "ord_of_nat (m+n) = ord_of_nat m + ord_of_nat n"
   by (induction n) (auto simp: plus_V_succ_right)
 
 lemma succ_0_plus_eq [simp]:
   assumes "\<alpha> \<in> elts \<omega>" 
   shows "succ 0 + \<alpha> = succ \<alpha>"
 proof -
   obtain n where "\<alpha> = ord_of_nat n"
     using assms elts_\<omega> by blast
   then show ?thesis
     by (metis One_nat_def ord_of_nat.simps ord_of_nat_add plus_1_eq_Suc)
 qed
 
 lemma omega_closed_add [intro]:
   assumes "\<alpha> \<in> elts \<omega>" "\<beta> \<in> elts \<omega>" shows "\<alpha>+\<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>+\<beta> = ord_of_nat (m+n)"
     using ord_of_nat_add by auto
   then show ?thesis
     by (simp add: \<omega>_def)
 qed
 
 lemma mem_plus_V_E:
   assumes l: "l \<in> elts (x + y)"
   obtains "l \<in> elts x" | z where "z \<in> elts y" "l = x + z"
   using l by (auto simp: plus [of x y] split: if_split_asm)
 
 lemma not_add_less_right: assumes "Ord y" shows "\<not> (x + y < x)"
   using assms
 proof (induction rule: Ord_induct)
   case (step i)
   then show ?case
     by (metis less_le_not_le plus sup_ge1)
 qed
 
 lemma not_add_mem_right: "\<not> (x + y \<in> elts x)"
   by (metis sup_ge1 mem_not_refl plus vsubsetD)
 
 text\<open>Proposition 3.3(iii)\<close>
 lemma add_not_less_TC_self: "\<not> x + y \<sqsubset> x"
 proof (induction y arbitrary: x rule: eps_induct)
   case (step y)
   then show ?case
     using less_TC_imp_not_le plus_eq_lift by fastforce
 qed
 
 lemma TC_sup_lift: "TC x \<sqinter> lift x y = 0"
 proof -
   have "elts (TC x) \<inter> elts (set ((+) x ` elts y)) = {}"
     using add_not_less_TC_self by (auto simp: less_TC_def)
   then have "TC x \<sqinter> set ((+) x ` elts y) = set {}"
     by (metis inf_V_def)
   then show ?thesis
     using lift_def by auto
 qed
 
 lemma lift_lift: "lift x (lift y z) = lift (x+y) z"
   using add.assoc  by (auto simp: lift_def)
 
 lemma lift_self_disjoint: "x \<sqinter> lift x u = 0"
   by (metis TC_sup_lift arg_subset_TC inf.absorb_iff2 inf_assoc inf_sup_aci(3) lift_0)
 
 lemma sup_lift_eq_lift:
   assumes "x \<squnion> lift x u = x \<squnion> lift x v"
   shows "lift x u = lift x v"
   by (metis (no_types) assms inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup_commute sup_inf_absorb)
 
 subsubsection \<open>Deeper properties of addition\<close>
 
 text\<open>Proposition 3.4(i)\<close>
 proposition lift_eq_lift: "lift x y = lift x z \<Longrightarrow> y = z"
 proof (induction y arbitrary: z rule: eps_induct)
   case (step y)
   show ?case
   proof (intro vsubsetI order_antisym)
     show "u \<in> elts z" if "u \<in> elts y" for u
     proof -
       have "x+u \<in> elts (lift x z)"
         using lift_def step.prems that by fastforce
       then obtain v where "v \<in> elts z" "x+u = x+v"
         using lift_def by auto
       then have "lift x u = lift x v"
         using sup_lift_eq_lift by (simp add: plus_eq_lift)
       then have "u=v"
         using step.IH that by blast
       then show ?thesis
         using \<open>v \<in> elts z\<close> by blast
     qed
     show "u \<in> elts y" if "u \<in> elts z" for u
     proof -
       have "x+u \<in> elts (lift x y)"
         using lift_def step.prems that by fastforce
       then obtain v where "v \<in> elts y" "x+u = x+v"
         using lift_def by auto
       then have "lift x u = lift x v"
         using sup_lift_eq_lift by (simp add: plus_eq_lift)
       then have "u=v"
         using step.IH by (metis \<open>v \<in> elts y\<close>)
       then show ?thesis
         using \<open>v \<in> elts y\<close> by auto
     qed
   qed
 qed
 
 corollary inj_lift: "inj_on (lift x) A"
   by (auto simp: inj_on_def dest: lift_eq_lift)
 
 corollary add_right_cancel [iff]:
   fixes x y z::V shows "x+y = x+z \<longleftrightarrow> y=z"
   by (metis lift_eq_lift plus_eq_lift sup_lift_eq_lift)
 
 corollary add_mem_right_cancel [iff]:
   fixes x y z::V shows "x+y \<in> elts (x+z) \<longleftrightarrow> y \<in> elts z"
   apply safe
    apply (metis mem_plus_V_E not_add_mem_right add_right_cancel)
   by (metis ZFC_in_HOL.ext dual_order.antisym elts_vinsert insert_subset order_refl plus_vinsert)
 
 corollary add_le_cancel_left [iff]:
   fixes x y z::V shows "x+y \<le> x+z \<longleftrightarrow> y\<le>z"
   by auto (metis add_mem_right_cancel mem_plus_V_E plus sup_ge1 vsubsetD)
 
 corollary add_less_cancel_left [iff]:
   fixes x y z::V shows "x+y < x+z \<longleftrightarrow> y<z"
   by (simp add: less_le_not_le)
 
 corollary lift_le_self [simp]: "lift x y \<le> x \<longleftrightarrow> y = 0"
   by (auto simp: inf.absorb_iff2 lift_eq_lift lift_self_disjoint)
 
 lemma succ_less_\<omega>_imp: "succ x < \<omega> \<Longrightarrow> x < \<omega>"
   by (metis add_le_cancel_left add.right_neutral le_0 le_less_trans succ_eq_add1)
 
 text\<open>Proposition 3.5\<close>
 lemma card_lift: "vcard (lift x y) = vcard y"
 proof (rule cardinal_cong)
   have "bij_betw ((+)x) (elts y) (elts (lift x y))"
     unfolding bij_betw_def
     by (simp add: inj_on_def lift_def)
   then show "elts (lift x y) \<approx> elts y"
     using eqpoll_def eqpoll_sym by blast
 qed
 
 lemma eqpoll_lift: "elts (lift x y) \<approx> elts y"
   by (metis card_lift cardinal_eqpoll eqpoll_sym eqpoll_trans)
 
 lemma vcard_add: "vcard (x + y) = vcard x \<oplus> vcard y"
   using card_lift [of x y] lift_self_disjoint [of x]
   by (simp add: plus_eq_lift vcard_disjoint_sup)
 
 lemma countable_add:
   assumes "countable (elts A)" "countable (elts B)"
   shows "countable (elts (A+B))"
 proof -
   have "vcard A \<le> \<aleph>0" "vcard B \<le> \<aleph>0"
     using assms countable_iff_le_Aleph0 by blast+
   then have "vcard (A+B) \<le> \<aleph>0"
     unfolding vcard_add
     by (metis Aleph_0 Card_\<omega> InfCard_cdouble_eq InfCard_def cadd_le_mono order_refl)
   then show ?thesis
     by (simp add: countable_iff_le_Aleph0)
 qed
 
 text\<open>Proposition 3.6\<close>
 proposition TC_add: "TC (x + y) = TC x \<squnion> lift x (TC y)"
 proof (induction y rule: eps_induct)
   case (step y)
   have *: "\<Squnion> (TC ` (+) x ` elts y) = TC x \<squnion> (SUP u\<in>elts y. TC (set ((+) x ` elts u)))"
     if "elts y \<noteq> {}"
   proof -
     obtain w where "w \<in> elts y"
       using \<open>elts y \<noteq> {}\<close> by blast
     then have "TC x \<le> TC (x + w)"
       by (simp add: step.IH)
     then have \<dagger>: "TC x \<le> (SUP w\<in>elts y. TC (x + w))"
       using \<open>w \<in> elts y\<close> by blast
     show ?thesis
       using that
       apply (intro conjI ballI impI order_antisym; clarsimp simp add: image_comp \<dagger>)
        apply(metis TC_sup_distrib Un_iff elts_sup_iff plus)
       by (metis TC_least Transset_TC arg_subset_TC le_sup_iff plus vsubsetD)
   qed
   have "TC (x + y) = (x + y) \<squnion> \<Squnion> (TC ` elts (x + y))"
     using TC by blast
   also have "\<dots> = x \<squnion> lift x y \<squnion> \<Squnion> (TC ` elts x) \<squnion> \<Squnion> ((\<lambda>u. TC (x+u)) ` elts y)"
     apply (simp add: plus_eq_lift image_Un Sup_Un_distrib sup.left_commute sup_assoc TC_sup_distrib SUP_sup_distrib)
     apply (simp add: lift_def sup.commute sup_aci *)
     done
   also have "\<dots> = x \<squnion> \<Squnion> (TC ` elts x) \<squnion> lift x y \<squnion> \<Squnion> ((\<lambda>u. TC x \<squnion> lift x (TC u)) ` elts y)"
     by (simp add: sup_aci step.IH)
   also have "\<dots> = TC x \<squnion> lift x y \<squnion> \<Squnion> ((\<lambda>u. lift x (TC u)) ` elts y)"
     by (simp add: sup_aci SUP_sup_distrib flip: TC [of x])
   also have "\<dots> = TC x \<squnion> lift x (y \<squnion> \<Squnion> (TC ` elts y))"
     by (metis (no_types) elts_of_set lift_Sup_distrib image_image lift_sup_distrib replacement small_elts sup_assoc)
   also have "\<dots> = TC x \<squnion> lift x (TC y)"
     by (simp add: TC [of y])
   finally show ?case .
 qed
 
 corollary TC_add': "z \<sqsubset> x + y \<longleftrightarrow> z \<sqsubset> x \<or> (\<exists>v. v \<sqsubset> y \<and> z = x + v)"
   using TC_add by (force simp: less_TC_def lift_def)
 
 text\<open>Corollary 3.7\<close>
 corollary vcard_TC_add: "vcard (TC (x+y)) = vcard (TC x) \<oplus> vcard (TC y)"
   by (simp add: TC_add TC_sup_lift card_lift vcard_disjoint_sup)
 
 text\<open>Corollary 3.8\<close>
 corollary TC_lift:
   assumes "y \<noteq> 0"
   shows "TC (lift x y) = TC x \<squnion> lift x (TC y)"
 proof -
   have "TC (lift x y) = lift x y \<squnion> \<Squnion> ((\<lambda>u. TC(x+u)) ` elts y)"
     unfolding TC [of "lift x y"]  by (simp add: lift_def image_image)
   also have "\<dots> = lift x y \<squnion> (SUP u\<in>elts y. TC x \<squnion> lift x (TC u))"
     by (simp add: TC_add)
   also have "\<dots> = lift x y \<squnion> TC x \<squnion> (SUP u\<in>elts y. lift x (TC u))"
     using assms by (auto simp: SUP_sup_distrib)
   also have "\<dots> = TC x \<squnion> lift x (TC y)"
     by (simp add: TC [of y] sup_aci image_image lift_sup_distrib lift_Sup_distrib)
   finally show ?thesis .
 qed
 
 proposition rank_add_distrib: "rank (x+y) = rank x + rank y"
 proof (induction y rule: eps_induct)
   case (step y)
   show ?case
   proof (cases "y=0")
     case False
     then obtain e where e: "e \<in> elts y"
       by fastforce
     have "rank (x+y) = (SUP u\<in>elts (x \<squnion> ZFC_in_HOL.set ((+) x ` elts y)). succ (rank u))"
       by (metis plus rank_Sup)
     also have "\<dots> = (SUP x\<in>elts x. succ (rank x)) \<squnion> (SUP z\<in>elts y. succ (rank x + rank z))"
       apply (simp add: Sup_Un_distrib image_Un image_image)
       apply (simp add: step cong: SUP_cong_simp)
       done
     also have "\<dots> = (SUP z \<in> elts y. rank x + succ (rank z))"
     proof -
       have "rank x \<le> (SUP z\<in>elts y. ZFC_in_HOL.succ (rank x + rank z))"
         using \<open>y \<noteq> 0\<close>
         by (auto simp: plus_eq_lift intro: order_trans [OF _ cSUP_upper [OF e]])
       then show ?thesis
         by (force simp: plus_V_succ_right simp flip: rank_Sup [of x] intro!: order_antisym)
     qed
     also have "\<dots> = rank x + (SUP z \<in> elts y. succ (rank z))"
       by (simp add: add_Sup_distrib False)
     also have "\<dots> = rank x + rank y"
       by (simp add: rank_Sup [of y])
     finally show ?thesis .
   qed auto
 qed
 
 lemma Ord_add [simp]: "\<lbrakk>Ord x; Ord y\<rbrakk> \<Longrightarrow> Ord (x+y)"
 proof (induction y rule: eps_induct)
   case (step y)
   then show ?case
     by (metis Ord_rank rank_add_distrib rank_of_Ord)
 qed
 
 lemma add_Sup_distrib_id: "A \<noteq> 0 \<Longrightarrow> x + \<Squnion>(elts A) = (SUP z\<in>elts A. x + z)"
   by (metis add_Sup_distrib image_ident image_image)
 
 lemma add_Limit: "Limit \<alpha> \<Longrightarrow> x + \<alpha> = (SUP z\<in>elts \<alpha>. x + z)"
   by (metis Limit_add_Sup_distrib Limit_eq_Sup_self image_ident image_image)
 
 lemma add_le_left:
   assumes "Ord \<alpha>" "Ord \<beta>" shows "\<beta> \<le> \<alpha>+\<beta>"
   using \<open>Ord \<beta>\<close>
 proof (induction rule: Ord_induct3)
   case 0
   then show ?case
     by auto
 next
   case (succ \<alpha>)
   then show ?case
     by (auto simp: plus_V_succ_right Ord_mem_iff_lt assms(1))
 next
   case (Limit \<mu>)
   then have k: "\<mu> = (SUP \<beta> \<in> elts \<mu>. \<beta>)"
     by (simp add: Limit_eq_Sup_self)
   also have "\<dots>  \<le> (SUP \<beta> \<in> elts \<mu>. \<alpha> + \<beta>)"
     using Limit.IH by auto
   also have "\<dots> = \<alpha> + (SUP \<beta> \<in> elts \<mu>. \<beta>)"
     using Limit.hyps Limit_add_Sup_distrib by presburger
   finally show ?case
     using k by simp
 qed
 
 lemma plus_\<omega>_equals_\<omega>:
   assumes "\<alpha> \<in> elts \<omega>"  shows "\<alpha> + \<omega> = \<omega>"
 proof (rule antisym)
   show "\<alpha> + \<omega> \<le> \<omega>"
     using Ord_trans assms by (auto simp: elim!: mem_plus_V_E)
   show "\<omega> \<le> \<alpha> + \<omega>"
     by (simp add: add_le_left assms)
 qed
 
 lemma one_plus_\<omega>_equals_\<omega> [simp]: "1 + \<omega> = \<omega>"
   by (simp add: one_V_def plus_\<omega>_equals_\<omega>)
 
 subsubsection \<open>Cancellation / set subtraction\<close>
 
 definition vle :: "V \<Rightarrow> V \<Rightarrow> bool" (infix "\<unlhd>" 50)
   where "x \<unlhd> y \<equiv> \<exists>z::V. x+z = y"
 
 lemma vle_refl [iff]: "x \<unlhd> x"
   by (metis (no_types) add.right_neutral vle_def)
 
 lemma vle_antisym: "\<lbrakk>x \<unlhd> y; y \<unlhd> x\<rbrakk> \<Longrightarrow> x = y"
   by (metis V_equalityI plus_eq_lift sup_ge1 vle_def vsubsetD)
 
 lemma vle_trans [trans]: "\<lbrakk>x \<unlhd> y; y \<unlhd> z\<rbrakk> \<Longrightarrow> x \<unlhd> z"
   by (metis add.assoc vle_def)
 
 definition vle_comparable :: "V \<Rightarrow> V \<Rightarrow> bool"
   where "vle_comparable x y \<equiv> x \<unlhd> y \<or> y \<unlhd> x"
 
 text\<open>Lemma 3.13\<close>
 lemma comparable:
   assumes "a+b = c+d"
   shows "vle_comparable a c"
 unfolding vle_comparable_def
 proof (rule ccontr)
   assume non: "\<not> (a \<unlhd> c \<or> c \<unlhd> a)"
   let ?\<phi> = "\<lambda>x. \<forall>z. a+x \<noteq> c+z"
   have "?\<phi> x" for x
   proof (induction x rule: eps_induct)
     case (step x)
     show ?case
     proof (cases "x=0")
       case True
       with non nonzero_less_TC show ?thesis
         using vle_def by auto
     next
       case False
       then obtain v where "v \<in> elts x"
         using trad_foundation by blast
       show ?thesis
       proof clarsimp
         fix z
         assume eq: "a + x = c + z"
         then have "z \<noteq> 0"
           using vle_def non by auto
         have av: "a+v \<in> elts (a+x)"
           by (simp add: \<open>v \<in> elts x\<close>)
         moreover have "a+x = c \<squnion> lift c z"
           using eq plus_eq_lift by fastforce
         ultimately have "a+v \<in> elts (c \<squnion> lift c z)"
           by simp
         moreover
         define u where "u \<equiv> set (elts x - {v})"
         have u: "v \<notin> elts u" and xeq: "x = vinsert v u"
           using \<open>v \<in> elts x\<close> by (auto simp: u_def intro: order_antisym)
         have case1: "a+v \<notin> elts c"
         proof
           assume avc: "a + v \<in> elts c"
           then have "a \<le> c"
             by clarify (metis Un_iff elts_sup_iff eq mem_not_sym mem_plus_V_E plus_eq_lift)
           moreover have "a \<squnion> lift a x = c \<squnion> lift c z"
             using eq by (simp add: plus_eq_lift)
           ultimately have "lift c z \<le> lift a x"
             by (metis inf.absorb_iff2 inf_commute inf_sup_absorb inf_sup_distrib2 lift_self_disjoint sup.commute)
           also have "\<dots> = vinsert (a+v) (lift a u)"
             by (simp add: lift_def vinsert_def xeq)
           finally have *: "lift c z \<le> vinsert (a + v) (lift a u)" .
           have "lift c z \<le> lift a u"
           proof -
             have "a + v \<notin> elts (lift c z)"
               using lift_self_disjoint [of c z] avc V_disjoint_iff by auto
             then show ?thesis
               using * less_eq_V_def by auto
           qed
           { fix e
             assume "e \<in> elts z"
             then have "c+e \<in> elts (lift c z)"
               by (simp add: lift_def)
             then have "c+e \<in> elts (lift a u)"
               using \<open>lift c z \<le> lift a u\<close> by blast
             then obtain y where "y \<in> elts u" "c+e = a+y"
               using lift_def by auto
             then have False
               by (metis elts_vinsert insert_iff step.IH xeq)
           }
           then show False
             using \<open>z \<noteq> 0\<close> by fastforce
         qed
         ultimately show False
           by (metis (no_types) \<open>v \<in> elts x\<close> av case1 eq mem_plus_V_E step.IH)
       qed
     qed
   qed
   then show False
     using assms by blast
 qed
 
 lemma vle1: "x \<unlhd> y \<Longrightarrow> x \<le> y"
   using vle_def plus_eq_lift by auto
 
 lemma vle2: "x \<unlhd> y \<Longrightarrow> x \<sqsubseteq> y"
   by (metis (full_types) TC_add' add.right_neutral le_TC_def vle_def nonzero_less_TC)
 
 lemma vle_iff_le_Ord:
   assumes "Ord \<alpha>" "Ord \<beta>"
   shows "\<alpha> \<unlhd> \<beta> \<longleftrightarrow> \<alpha> \<le> \<beta>"
 proof
   show "\<alpha> \<le> \<beta>" if "\<alpha> \<unlhd> \<beta>"
     using that by (simp add: vle1)
   show "\<alpha> \<unlhd> \<beta>" if "\<alpha> \<le> \<beta>"
     using \<open>Ord \<alpha>\<close> \<open>Ord \<beta>\<close> that
   proof (induction \<alpha> arbitrary: \<beta> rule: Ord_induct)
     case (step \<gamma>)
     then show ?case
       unfolding vle_def
       by (metis Ord_add Ord_linear add_le_left mem_not_refl mem_plus_V_E vsubsetD)
   qed
 qed
 
 lemma add_le_cancel_left0 [iff]:
   fixes x::V shows "x \<le> x+z"
   by (simp add: vle1 vle_def)
 
 lemma add_less_cancel_left0 [iff]:
   fixes x::V shows "x < x+z \<longleftrightarrow> 0<z"
   by (metis add_less_cancel_left add.right_neutral)
 
 lemma le_Ord_diff:
   assumes "\<alpha> \<le> \<beta>" "Ord \<alpha>" "Ord \<beta>"
   obtains \<gamma> where "\<alpha>+\<gamma> = \<beta>" "\<gamma> \<le> \<beta>" "Ord \<gamma>"
 proof -
   obtain \<gamma> where \<gamma>: "\<alpha>+\<gamma> = \<beta>" "\<gamma> \<le> \<beta>"
     by (metis add_le_cancel_left add_le_left assms vle_def vle_iff_le_Ord)
   then have "Ord \<gamma>"
     using Ord_def Transset_def \<open>Ord \<beta>\<close> by force
   with \<gamma> that show thesis by blast
 qed
 
 lemma plus_Ord_le:
   assumes "\<alpha> \<in> elts \<omega>" "Ord \<beta>" shows "\<alpha>+\<beta> \<le> \<beta>+\<alpha>"
 proof (cases "\<beta> \<in> elts \<omega>")
   case True
   with assms have "\<alpha>+\<beta> = \<beta>+\<alpha>"
     by (auto simp: elts_\<omega> add.commute ord_of_nat_add [symmetric])
   then show ?thesis by simp
 next
   case False
   then have "\<omega> \<le> \<beta>" 
     using Ord_linear2 Ord_mem_iff_lt \<open>Ord \<beta>\<close> by auto
   then obtain \<gamma> where "\<omega>+\<gamma> = \<beta>" "\<gamma> \<le> \<beta>" "Ord \<gamma>"
     using \<open>Ord \<beta>\<close> le_Ord_diff by auto
   then have "\<alpha>+\<beta> = \<beta>"
     by (metis add.assoc assms(1) plus_\<omega>_equals_\<omega>)
   then show ?thesis
     by simp
 qed
 
 lemma add_right_mono: "\<lbrakk>\<alpha> \<le> \<beta>; Ord \<alpha>; Ord \<beta>; Ord \<gamma>\<rbrakk> \<Longrightarrow> \<alpha>+\<gamma> \<le> \<beta>+\<gamma>"
   by (metis add_le_cancel_left add.assoc add_le_left le_Ord_diff)
 
 lemma add_strict_mono: "\<lbrakk>\<alpha> < \<beta>; \<gamma> < \<delta>; Ord \<alpha>; Ord \<beta>; Ord \<gamma>; Ord \<delta>\<rbrakk> \<Longrightarrow> \<alpha>+\<gamma> < \<beta>+\<delta>"
   by (metis order.strict_implies_order add_less_cancel_left add_right_mono le_less_trans)
 
 lemma add_right_strict_mono: "\<lbrakk>\<alpha> \<le> \<beta>; \<gamma> < \<delta>; Ord \<alpha>; Ord \<beta>; Ord \<gamma>; Ord \<delta>\<rbrakk> \<Longrightarrow> \<alpha>+\<gamma> < \<beta>+\<delta>"
   using add_strict_mono le_imp_less_or_eq by blast
 
 lemma Limit_add_Limit [simp]:
   assumes "Limit \<mu>" "Ord \<beta>" shows "Limit (\<beta> + \<mu>)"
   unfolding Limit_def
   proof (intro conjI allI impI)
   show "Ord (\<beta> + \<mu>)"
     using Limit_def assms by auto
   show "0 \<in> elts (\<beta> + \<mu>)"
     using Limit_def add_le_left assms by auto
 next
   fix \<gamma>
   assume "\<gamma> \<in> elts (\<beta> + \<mu>)"
   then consider "\<gamma> \<in> elts \<beta>" | \<xi> where "\<xi> \<in> elts \<mu>" "\<gamma> = \<beta> + \<xi>"
     using mem_plus_V_E by blast
   then show "succ \<gamma> \<in> elts (\<beta> + \<mu>)"
   proof cases
     case 1
     then show ?thesis
       by (metis Kirby.add_strict_mono Limit_def Ord_add Ord_in_Ord Ord_mem_iff_lt assms one_V_def succ_eq_add1)
   next
     case 2
     then show ?thesis
       by (metis Limit_def add_mem_right_cancel assms(1) plus_V_succ_right)
   qed
 qed
 
 
 subsection \<open>Generalised Difference\<close>
 
 definition odiff where "odiff y x \<equiv> THE z::V. (x+z = y) \<or> (z=0 \<and> \<not> x \<unlhd> y)"
 
 lemma vle_imp_odiff_eq: "x \<unlhd> y \<Longrightarrow> x + (odiff y x) = y"
   by (auto simp: vle_def odiff_def)
 
 lemma not_vle_imp_odiff_0: "\<not> x \<unlhd> y \<Longrightarrow> (odiff y x) = 0"
   by (auto simp: vle_def odiff_def)
 
 lemma Ord_odiff_eq:
   assumes "\<alpha> \<le> \<beta>" "Ord \<alpha>" "Ord \<beta>"
   shows "\<alpha> + odiff \<beta> \<alpha> = \<beta>"
   by (simp add: assms vle_iff_le_Ord vle_imp_odiff_eq)
 
 lemma Ord_odiff:
   assumes "Ord \<alpha>" "Ord \<beta>" shows "Ord (odiff \<beta> \<alpha>)"
 proof (cases "\<alpha> \<unlhd> \<beta>")
   case True
   then show ?thesis
     by (metis add_right_cancel assms le_Ord_diff vle1 vle_imp_odiff_eq)
 next
   case False
   then show ?thesis
     by (simp add: odiff_def vle_def)
 qed
 
 lemma Ord_odiff_le:
   assumes  "Ord \<alpha>" "Ord \<beta>" shows "odiff \<beta> \<alpha> \<le> \<beta>"
 proof (cases "\<alpha> \<unlhd> \<beta>")
   case True
   then show ?thesis
     by (metis add_right_cancel assms le_Ord_diff vle1 vle_imp_odiff_eq)
 next
   case False
   then show ?thesis 
     by (simp add: odiff_def vle_def)
 qed
 
 
 lemma odiff_0_right [simp]: "odiff x 0 = x"
   by (metis add.left_neutral vle_def vle_imp_odiff_eq)
 
 lemma odiff_succ: "y \<unlhd> x \<Longrightarrow> odiff (succ x) y = succ (odiff x y)"
   unfolding odiff_def
   by (metis add_right_cancel odiff_def plus_V_succ_right vle_def vle_imp_odiff_eq)
 
 lemma odiff_eq_iff: "z \<unlhd> x \<Longrightarrow> odiff x z = y \<longleftrightarrow> x = z + y"
   by (auto simp: odiff_def vle_def)
 
 lemma odiff_le_iff: "z \<unlhd> x \<Longrightarrow> odiff x z \<le> y \<longleftrightarrow> x \<le> z + y"
   by (auto simp: odiff_def vle_def)
 
 lemma odiff_less_iff: "z \<unlhd> x \<Longrightarrow> odiff x z < y \<longleftrightarrow> x < z + y"
   by (auto simp: odiff_def vle_def)
 
 lemma odiff_ge_iff: "z \<unlhd> x \<Longrightarrow> odiff x z \<ge> y \<longleftrightarrow> x \<ge> z + y"
   by (auto simp: odiff_def vle_def)
 
 lemma Ord_odiff_le_iff: "\<lbrakk>\<alpha> \<le> x; Ord x; Ord \<alpha>\<rbrakk> \<Longrightarrow> odiff x \<alpha> \<le> y \<longleftrightarrow> x \<le> \<alpha> + y"
   by (simp add: odiff_le_iff vle_iff_le_Ord)
 
 lemma odiff_le_odiff:
   assumes "x \<unlhd> y" shows "odiff x z \<le> odiff y z"
 proof (cases "z \<unlhd> x")
   case True
   then show ?thesis
     using assms odiff_le_iff vle1 vle_imp_odiff_eq vle_trans by presburger
 next
   case False
   then show ?thesis
     by (simp add: not_vle_imp_odiff_0)
 qed
 
 lemma Ord_odiff_le_odiff: "\<lbrakk>x \<le> y; Ord x; Ord y\<rbrakk> \<Longrightarrow> odiff x \<alpha> \<le> odiff y \<alpha>"
   by (simp add: odiff_le_odiff vle_iff_le_Ord)
 
 lemma Ord_odiff_less_odiff: "\<lbrakk>\<alpha> \<le> x; x < y; Ord x; Ord y; Ord \<alpha>\<rbrakk> \<Longrightarrow> odiff x \<alpha> < odiff y \<alpha>"
   by (metis Ord_odiff_eq Ord_odiff_le_odiff dual_order.strict_trans less_V_def)
 
 lemma Ord_odiff_less_imp_less: "\<lbrakk>odiff x \<alpha> < odiff y \<alpha>; Ord x; Ord y\<rbrakk> \<Longrightarrow> x < y"
   by (meson Ord_linear2 leD odiff_le_odiff vle_iff_le_Ord)
 
 lemma odiff_add_cancel [simp]: "odiff (x + y) x = y"
   by (simp add: odiff_eq_iff vle_def)
 
 lemma odiff_add_cancel_0 [simp]: "odiff x x = 0"
   by (simp add: odiff_eq_iff)
 
 lemma odiff_add_cancel_both [simp]: "odiff (x + y) (x + z) = odiff y z"
   by (simp add: add.assoc odiff_def vle_def)
 
 
 subsection \<open>Generalised Multiplication\<close>
 
 text \<open>Credited to Dana Scott\<close>
 
 instantiation V :: times
 begin
 
 text\<open>This definition is credited to Tarski\<close>
 definition times_V :: "V \<Rightarrow> V \<Rightarrow> V"
   where "times_V x \<equiv> transrec (\<lambda>f y. \<Squnion> ((\<lambda>u. lift (f u) x) ` elts y))"
 
 instance ..
 end
 
 lemma mult: "x * y = (SUP u\<in>elts y. lift (x * u) x)"
   unfolding times_V_def  by (subst transrec) (force simp:)
 
 text \<open>Lemma 4.2\<close>
 
 lemma mult_zero_right [simp]:
   fixes x::V shows "x * 0 = 0"
   by (metis ZFC_in_HOL.Sup_empty elts_0 image_empty mult)
 
 lemma mult_insert: "x * (vinsert y z) = x*z \<squnion> lift (x*y) x"
   by (metis (no_types, lifting) elts_vinsert image_insert replacement small_elts sup_commute mult Sup_V_insert)
 
 lemma mult_succ: "x * succ y = x*y + x"
   by (simp add: mult_insert plus_eq_lift succ_def)
 
 lemma ord_of_nat_mult: "ord_of_nat (m*n) = ord_of_nat m * ord_of_nat n"
 proof (induction n)
   case (Suc n)
   then show ?case
     by (simp add: add.commute [of m]) (simp add: ord_of_nat_add mult_succ)
 qed auto
 
 lemma omega_closed_mult [intro]:
   assumes "\<alpha> \<in> elts \<omega>" "\<beta> \<in> elts \<omega>" shows "\<alpha>*\<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>*\<beta> = ord_of_nat (m*n)"
     by (simp add: ord_of_nat_mult)
   then show ?thesis
     by (simp add: \<omega>_def)
 qed
 
 lemma zero_imp_le_mult: "0 \<in> elts y \<Longrightarrow> x \<le> x*y"
   by (auto simp: mult [of x y])
   
 subsubsection\<open>Proposition 4.3\<close>
 
 lemma mult_zero_left [simp]:
   fixes x::V shows "0 * x = 0"
 proof (induction x rule: eps_induct)
   case (step x)
   then show ?case
     by (subst mult) auto
 qed
 
 lemma mult_sup_distrib:
   fixes x::V shows "x * (y \<squnion> z) = x*y \<squnion> x*z"
   unfolding mult [of x "y \<squnion> z"] mult [of x y] mult [of x z]
   by (simp add: Sup_Un_distrib image_Un)
 
 lemma mult_Sup_distrib: "small Y \<Longrightarrow> x * (\<Squnion>Y) = \<Squnion> ((*) x ` Y)" for Y:: "V set"
   unfolding mult [of x "\<Squnion>Y"]
   by (simp add: cSUP_UNION) (metis mult)
 
 lemma mult_lift_imp_distrib: "x * (lift y z) = lift (x*y) (x*z) \<Longrightarrow> x * (y+z) = x*y + x*z"
   by (simp add: mult_sup_distrib plus_eq_lift)
 
 lemma mult_lift: "x * (lift y z) = lift (x*y) (x*z)"
 proof (induction z rule: eps_induct)
   case (step z)
   have "x * lift y z = (SUP u\<in>elts (lift y z). lift (x * u) x)"
     using mult by blast
   also have "\<dots> = (SUP v\<in>elts z. lift (x * (y + v)) x)"
     using lift_def by auto
   also have "\<dots> = (SUP v\<in>elts z. lift (x * y + x * v) x)"
     using mult_lift_imp_distrib step.IH by auto
   also have "\<dots> = (SUP v\<in>elts z. lift (x * y) (lift (x * v) x))"
     by (simp add: lift_lift)
   also have "\<dots> = lift (x * y) (SUP v\<in>elts z. lift (x * v) x)"
     by (simp add: image_image lift_Sup_distrib)
   also have "\<dots> = lift (x*y) (x*z)"
     by (metis mult)
   finally show ?case .
 qed
 
 lemma mult_Limit: "Limit \<gamma> \<Longrightarrow> x * \<gamma> = \<Squnion> ((*) x ` elts \<gamma>)"
   by (metis Limit_eq_Sup_self mult_Sup_distrib small_elts)
 
 lemma add_mult_distrib: "x * (y+z) = x*y + x*z" for x::V
   by (simp add: mult_lift mult_lift_imp_distrib)
 
 instantiation V :: monoid_mult
 begin
 instance
 proof
   show "1 * x = x" for x :: V
   proof (induction x rule: eps_induct)
     case (step x)
     then show ?case
       by (subst mult) auto
   qed
   show "x * 1 = x" for x :: V
     by (subst mult) auto
   show "(x * y) * z = x * (y * z)" for x y z::V
   proof (induction z rule: eps_induct)
     case (step z)
     have "(x * y) * z = (SUP u\<in>elts z. lift (x * y * u) (x * y))"
       using mult by blast
     also have "\<dots> = (SUP u\<in>elts z. lift (x * (y * u)) (x * y))"
       using step.IH by auto
     also have "\<dots> = (SUP u\<in>elts z. x * lift (y * u) y)"
       using mult_lift by auto
     also have "\<dots> = x * (SUP u\<in>elts z. lift (y * u) y)"
       by (simp add: image_image mult_Sup_distrib)
     also have "\<dots> = x * (y * z)"
       by (metis mult)
     finally show ?case .
   qed
 qed
 
 end
 
 lemma le_mult:
   assumes "Ord \<beta>" "\<beta> \<noteq> 0" shows "\<alpha> \<le> \<alpha> * \<beta>"
   using assms
 proof (induction rule: Ord_induct3)
   case (succ \<alpha>)
   then show ?case
     using mult_insert succ_def by fastforce
 next
   case (Limit \<mu>)
   have "\<alpha> \<in> (*) \<alpha> ` elts \<mu>"
     using Limit.hyps Limit_def one_V_def by (metis imageI mult.right_neutral)
   then have "\<alpha> \<le> \<Squnion> ((*) \<alpha> ` elts \<mu>)"
     by auto
   then show ?case
     by (simp add: Limit.hyps mult_Limit)
 qed auto
 
 lemma mult_sing_1 [simp]:
   fixes x::V shows "x * set{1} = lift x x"
   by (subst mult) auto
 
 lemma mult_2_right [simp]:
   fixes x::V shows "x * set{0,1} = x+x"
   by (subst mult) (auto simp: Sup_V_insert plus_eq_lift)
 
 lemma Ord_mult [simp]: "\<lbrakk>Ord y; Ord x\<rbrakk> \<Longrightarrow> Ord (x*y)"
 proof (induction y rule: Ord_induct3)
   case 0
   then show ?case
     by auto
 next
   case (succ k)
   then show ?case
     by (simp add: mult_succ)
 next
   case (Limit k)
   then have "Ord (x * \<Squnion> (elts k))"
     by (metis Ord_Sup imageE mult_Sup_distrib small_elts)
   then show ?case
     using Limit.hyps Limit_eq_Sup_self by auto
 qed
 
 
 subsubsection \<open>Proposition 4.4-5\<close>
 proposition rank_mult_distrib: "rank (x*y) = rank x * rank y"
 proof (induction y rule: eps_induct)
   case (step y)
   have "rank (x*y) = (SUP y\<in>elts (SUP u\<in>elts y. lift (x * u) x). succ (rank y))"
     by (metis rank_Sup mult)
   also have "\<dots> = (SUP u\<in>elts y. SUP r\<in>elts x. succ (rank (x * u + r)))"
     apply (simp add: lift_def image_image image_UN)
     apply (simp add: Sup_V_def)
     done
   also have "\<dots> = (SUP u\<in>elts y. SUP r\<in>elts x. succ (rank (x * u) + rank r))"
     using rank_add_distrib by auto
   also have "\<dots> = (SUP u\<in>elts y. SUP r\<in>elts x. succ (rank x * rank u + rank r))"
     using step arg_cong [where f = Sup] by auto
   also have "\<dots> = (SUP u\<in>elts y. rank x * rank u + rank x)"
   proof (rule SUP_cong)
     show "(SUP r\<in>elts x. succ (rank x * rank u + rank r)) = rank x * rank u + rank x"
       if "u \<in> elts y" for u
     proof (cases "x=0")
       case False
       have "(SUP r\<in>elts x. succ (rank x * rank u + rank r)) = rank x * rank u + (SUP y\<in>elts x. succ (rank y))"
       proof (rule order_antisym)
         show "(SUP r\<in>elts x. succ (rank x * rank u + rank r)) \<le> rank x * rank u + (SUP y\<in>elts x. succ (rank y))"
           by (auto simp: Sup_le_iff simp flip: plus_V_succ_right)
         have "rank x * rank u + (SUP y\<in>elts x. succ (rank y)) = (SUP y\<in>elts x. rank x * rank u + succ (rank y))"
           by (simp add: add_Sup_distrib False)
         also have "\<dots> \<le> (SUP r\<in>elts x. succ (rank x * rank u + rank r))"
           using plus_V_succ_right by auto
         finally show "rank x * rank u + (SUP y\<in>elts x. succ (rank y)) \<le> (SUP r\<in>elts x. succ (rank x * rank u + rank r))" .
       qed
       also have "\<dots> = rank x * rank u + rank x"
         by (metis rank_Sup)
       finally show ?thesis .
     qed auto
   qed auto
   also have "\<dots> = rank x * rank y"
     by (simp add: rank_Sup [of y] mult_Sup_distrib mult_succ image_image)
   finally show ?case .
 qed
 
 lemma mult_le1:
   fixes y::V assumes "y \<noteq> 0" shows "x \<sqsubseteq> x * y"
 proof (cases "x = 0")
   case False
   then obtain r where r: "r \<in> elts x"
     by fastforce
   from \<open>y \<noteq> 0\<close> show ?thesis
   proof (induction y rule: eps_induct)
     case (step y)
     show ?case
     proof (cases "y = 1")
       case False
       with \<open>y \<noteq> 0\<close> obtain p where p: "p \<in> elts y" "p \<noteq> 0"
         by (metis V_equalityI elts_1 insertI1 singletonD trad_foundation)
       then have "x*p + r \<in> elts (lift (x*p) x)"
         by (simp add: lift_def r)
       moreover have "lift (x*p) x \<le> x*y"
         by (metis bdd_above_iff_small cSUP_upper2 order_refl \<open>p \<in> elts y\<close> replacement small_elts mult)
       ultimately have "x*p + r \<in> elts (x*y)"
         by blast
       moreover have "x*p \<sqsubseteq> x*p + r"
         by (metis TC_add' V_equalityI add.right_neutral eps_induct le_TC_refl less_TC_iff less_imp_le_TC)
       ultimately show ?thesis
         using step.IH [OF p] le_TC_trans less_TC_iff by blast
     qed auto
   qed
 qed auto
 
 lemma mult_eq_0_iff [simp]:
   fixes y::V shows "x * y = 0 \<longleftrightarrow> x=0 \<or> y=0"
 proof
   show "x = 0 \<or> y = 0" if "x * y = 0"
     by (metis le_0 le_TC_def less_TC_imp_not_le mult_le1 that)
 qed auto
 
 lemma lift_lemma:
   assumes "x \<noteq> 0" "y \<noteq> 0"  shows "\<not> lift (x * y) x \<le> x"
   using assms mult_le1 [of concl: x y]
   by (auto simp: le_TC_def TC_lift less_TC_def less_TC_imp_not_le)
 
 lemma mult_le2:
   fixes y::V assumes "x \<noteq> 0" "y \<noteq> 0" "y \<noteq> 1" shows "x \<sqsubset> x * y"
 proof -
   obtain v where v: "v \<in> elts y" "v \<noteq> 0"
     using assms by fastforce
   have "x \<noteq> x * y"
     using lift_lemma [of x v]
     by (metis \<open>x \<noteq> 0\<close> bdd_above_iff_small cSUP_upper2 order_refl replacement small_elts mult v)
   then show ?thesis
   using assms mult_le1 [of y x]
     by (auto simp: le_TC_def)
 qed
 
 lemma elts_mult_\<omega>E:
   assumes "x \<in> elts (y * \<omega>)"
   obtains n where "n \<noteq> 0" "x \<in> elts (y * ord_of_nat n)" "\<And>m. m < n \<Longrightarrow> x \<notin> elts (y * ord_of_nat m)"
 proof -
   obtain k where k:  "k \<noteq> 0 \<and> x \<in> elts (y * ord_of_nat k)"
     using assms
     apply (simp add: mult_Limit elts_\<omega>)
     by (metis mult_eq_0_iff elts_0 ex_in_conv ord_of_eq_0_iff that)
   define n where "n \<equiv> (LEAST k. k \<noteq> 0 \<and> x \<in> elts (y * ord_of_nat k))"
   show thesis
   proof
     show "n \<noteq> 0" "x \<in> elts (y * ord_of_nat n)"
       unfolding n_def by (metis (mono_tags, lifting) LeastI_ex k)+
     show "\<And>m. m < n \<Longrightarrow> x \<notin> elts (y * ord_of_nat m)"
       by (metis (mono_tags, lifting) mult_eq_0_iff elts_0 empty_iff n_def not_less_Least ord_of_eq_0_iff)
   qed
 qed
 
 
 subsubsection\<open>Theorem 4.6\<close>
 
 theorem mult_eq_imp_0:
   assumes "a*x = a*y + b" "b \<sqsubset> a"
   shows "b=0"
 proof (cases "a=0 \<or> x=0")
   case True
   with assms show ?thesis
     by (metis add_le_cancel_left mult_eq_0_iff eq_iff le_0)
 next
   case False
   then have "a\<noteq>0" "x\<noteq>0"
     by auto
   then show ?thesis
   proof (cases "y=0")
     case True
     then show ?thesis
       using assms less_asym_TC mult_le2 by force
   next
     case False
     have "b=0" if "Ord \<alpha>" "x \<in> elts (Vset \<alpha>)" "y \<in> elts (Vset \<alpha>)" for \<alpha>
       using that assms
     proof (induction \<alpha> arbitrary: x y b rule: Ord_induct3)
       case 0
       then show ?case by auto
     next
       case (succ k)
       define \<Phi> where "\<Phi> \<equiv> \<lambda>x y. \<exists>r. 0 \<sqsubset> r \<and> r \<sqsubset> a \<and> a*x = a*y + r"
       show ?case
       proof (rule ccontr)
         assume "b \<noteq> 0"
         then have "0 \<sqsubset> b"
           by (metis nonzero_less_TC)
         then have "\<Phi> x y"
           unfolding \<Phi>_def using succ.prems by blast
         then obtain x' where "\<Phi> x' y" "x' \<sqsubseteq> x" and min: "\<And>x''. x'' \<sqsubset> x' \<Longrightarrow> \<not> \<Phi> x'' y"
           using less_TC_minimal [of "\<lambda>x. \<Phi> x y" x] by blast
         then obtain b' where "0 \<sqsubset> b'" "b' \<sqsubset> a" and eq: "a*x' = a*y + b'"
           using \<Phi>_def by blast
         have "a*y \<sqsubset> a*x'"
           using TC_add' \<open>0 \<sqsubset> b'\<close> eq by auto
         then obtain p where "p \<in> elts (a * x')" "a * y \<sqsubseteq> p"
           using less_TC_iff by blast
         then have "p \<notin> elts (a * y)"
           using less_TC_iff less_irrefl_TC by blast
         then have "p \<in> \<Union> (elts ` (\<lambda>v. lift (a * v) a) ` elts x')"
           by (metis \<open>p \<in> elts (a * x')\<close> elts_Sup replacement small_elts mult)
         then obtain u c where "u \<in> elts x'" "c \<in> elts a" "p = a*u + c"
           using lift_def by auto
         then have "p \<in> elts (lift (a*y) b')"
           using \<open>p \<in> elts (a * x')\<close> \<open>p \<notin> elts (a * y)\<close> eq plus_eq_lift by auto
         then obtain d where d: "d \<in> elts b'" "p = a*y + d" "p = a*u + c"
           by (metis \<open>p = a * u + c\<close> \<open>p \<in> elts (a * x')\<close> \<open>p \<notin> elts (a * y)\<close> eq mem_plus_V_E)
         have noteq: "a*y \<noteq> a*u"
         proof
           assume "a*y = a*u"
           then have "lift (a*y) a = lift (a*u) a"
             by metis
           also have "\<dots> \<le> a*x'"
             unfolding mult [of _ x'] using \<open>u \<in> elts x'\<close> by (auto intro: cSUP_upper)
           also have "\<dots> = a*y \<squnion> lift (a*y) b'"
             by (simp add: eq plus_eq_lift)
           finally have "lift (a*y) a \<le> a*y \<squnion> lift (a*y) b'" .
           then have "lift (a*y) a \<le> lift (a*y) b'"
             using add_le_cancel_left less_TC_imp_not_le plus_eq_lift \<open>b' \<sqsubset> a\<close> by auto
           then have "a \<le> b'"
             by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
           then show False
             using \<open>b' \<sqsubset> a\<close> less_TC_imp_not_le by auto
         qed
         consider "a*y \<unlhd> a*u" | "a*u \<unlhd> a*y"
           using d comparable vle_comparable_def by auto
         then show False
         proof cases
           case 1
           then obtain e where e: "a*u = a*y + e" "e \<noteq> 0"
             by (metis add.right_neutral noteq vle_def)
           moreover have "e + c = d"
             by (metis e add_right_cancel \<open>p = a * u + c\<close> \<open>p = a * y + d\<close> add.assoc)
           with \<open>d \<in> elts b'\<close> \<open>b' \<sqsubset> a\<close> have "e \<sqsubset> a"
             by (meson less_TC_iff less_TC_trans vle2 vle_def)
           ultimately show False
             \<comment>\<open>contradicts minimality of @{term x'}\<close>
             using min unfolding \<Phi>_def by (meson \<open>u \<in> elts x'\<close> le_TC_def less_TC_iff nonzero_less_TC)
         next
           case 2
           then obtain e where e: "a*y = a*u + e" "e \<noteq> 0"
             by (metis add.right_neutral noteq vle_def)
           moreover have "e + d = c"
             by (metis e add_right_cancel \<open>p = a * u + c\<close> \<open>p = a * y + d\<close> add.assoc)
           with \<open>d \<in> elts b'\<close> \<open>b' \<sqsubset> a\<close> have "e \<sqsubset> a"
             by (metis \<open>c \<in> elts a\<close> less_TC_iff vle2 vle_def)
           ultimately have "\<Phi> y u"
             unfolding \<Phi>_def using nonzero_less_TC by blast
           then obtain y' where "\<Phi> y' u" "y' \<sqsubseteq> y" and min: "\<And>x''. x'' \<sqsubset> y' \<Longrightarrow> \<not> \<Phi> x'' u"
             using less_TC_minimal [of "\<lambda>x. \<Phi> x u" y] by blast
           then obtain b' where "0 \<sqsubset> b'" "b' \<sqsubset> a" and eq: "a*y' = a*u + b'"
             using \<Phi>_def by blast
           have u_k: "u \<in> elts (Vset k)"
             using \<open>u \<in> elts x'\<close> \<open>x' \<sqsubseteq> x\<close> succ Vset_succ_TC less_TC_iff less_le_TC_trans by blast
           have "a*u \<sqsubset> a*y'"
             using TC_add' \<open>0 \<sqsubset> b'\<close> eq by auto
           then obtain p where "p \<in> elts (a * y')" "a * u \<sqsubseteq> p"
             using less_TC_iff by blast
           then have "p \<notin> elts (a * u)"
             using less_TC_iff less_irrefl_TC by blast
           then have "p \<in> \<Union> (elts ` (\<lambda>v. lift (a * v) a) ` elts y')"
             by (metis \<open>p \<in> elts (a * y')\<close> elts_Sup replacement small_elts mult)
           then obtain v c where "v \<in> elts y'" "c \<in> elts a" "p = a*v + c"
             using lift_def by auto
           then have "p \<in> elts (lift (a*u) b')"
             using \<open>p \<in> elts (a * y')\<close> \<open>p \<notin> elts (a * u)\<close> eq plus_eq_lift by auto
           then obtain d where d: "d \<in> elts b'" "p = a*u + d" "p = a*v + c"
             by (metis \<open>p = a * v + c\<close> \<open>p \<in> elts (a * y')\<close> \<open>p \<notin> elts (a * u)\<close> eq mem_plus_V_E)
           have v_k: "v \<in> elts (Vset k)"
             using Vset_succ_TC \<open>v \<in> elts y'\<close> \<open>y' \<sqsubseteq> y\<close> less_TC_iff less_le_TC_trans succ.hyps succ.prems(2) by blast
           have noteq: "a*u \<noteq> a*v"
             proof
               assume "a*u = a*v"
               then have "lift (a*v) a \<le> a*y'"
                 unfolding mult [of _ y'] using \<open>v \<in> elts y'\<close> by (auto intro: cSUP_upper)
               also have "\<dots> = a*u \<squnion> lift (a*u) b'"
                 by (simp add: eq plus_eq_lift)
               finally have "lift (a*v) a \<le> a*u \<squnion> lift (a*u) b'" .
               then have "lift (a*u) a \<le> lift (a*u) b'"
                 by (metis \<open>a * u = a * v\<close> le_iff_sup lift_sup_distrib sup_left_commute sup_lift_eq_lift)
               then have "a \<le> b'"
                 by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
               then show False
                 using \<open>b' \<sqsubset> a\<close> less_TC_imp_not_le by auto
             qed
           consider "a*u \<unlhd> a*v" | "a*v \<unlhd> a*u"
             using d comparable vle_comparable_def by auto
           then show False
           proof cases
             case 1
             then obtain e where e: "a*v = a*u + e" "e \<noteq> 0"
               by (metis add.right_neutral noteq vle_def)
             moreover have "e + c = d"
               by (metis add_right_cancel \<open>p = a * u + d\<close> \<open>p = a * v + c\<close> add.assoc e)
             with \<open>d \<in> elts b'\<close> \<open>b' \<sqsubset> a\<close> have "e \<sqsubset> a"
               by (meson less_TC_iff less_TC_trans vle2 vle_def)
             ultimately show False
               using succ.IH u_k v_k by blast
           next
             case 2
             then obtain e where e: "a*u = a*v + e" "e \<noteq> 0"
               by (metis add.right_neutral noteq vle_def)
             moreover have "e + d = c"
               by (metis add_right_cancel add.assoc d e)
             with \<open>d \<in> elts b'\<close> \<open>b' \<sqsubset> a\<close> have "e \<sqsubset> a"
               by (metis \<open>c \<in> elts a\<close> less_TC_iff vle2 vle_def)
            ultimately show False
              using succ.IH u_k v_k by blast
           qed
         qed
       qed
     next
       case (Limit k)
       obtain i j where k: "i \<in> elts k" "j \<in> elts k"
         and x: "x \<in> elts (Vset i)"
         and y: "y \<in> elts (Vset j)"
         using that Limit by (auto simp: Limit_Vfrom_eq)
       show ?case
       proof (rule Limit.IH [of "i \<squnion> j"])
         show "i \<squnion> j \<in> elts k"
           by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff)
         show "x \<in> elts (Vset (i \<squnion> j))" "y \<in> elts (Vset (i \<squnion> j))"
           using x y by (auto simp: Vfrom_sup)
       qed (use Limit.prems in auto)
     qed
     then show ?thesis
       by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt)
   qed
 qed
 
 subsubsection\<open>Theorem 4.7\<close>
 
 lemma mult_cancellation_half:
   assumes "a*x + r = a*y + s" "r \<sqsubset> a" "s \<sqsubset> a"
   shows "x \<le> y"
 proof -
   have "x \<le> y" if "Ord \<alpha>" "x \<in> elts (Vset \<alpha>)" "y \<in> elts (Vset \<alpha>)" for \<alpha>
     using that assms
   proof (induction \<alpha> arbitrary: x y r s rule: Ord_induct3)
     case 0
     then show ?case
       by auto
   next
     case (succ k)
     show ?case
     proof
       fix u
       assume u: "u \<in> elts x"
       have u_k: "u \<in> elts (Vset k)"
         using Vset_succ succ.hyps succ.prems(1) u by auto
       obtain r' where "r' \<in> elts a" "r \<sqsubseteq> r'"
         using less_TC_iff succ.prems(4) by blast
       have "a*u + r' \<in> elts (lift (a*u) a)"
         by (simp add: \<open>r' \<in> elts a\<close> lift_def)
       also have "\<dots> \<le> elts (a*x)"
         using u by (force simp: mult [of _ x])
       also have "\<dots> \<le> elts (a*y + s)"
         by (metis less_eq_V_def plus_eq_lift succ.prems(3) sup_ge1)
       also have "\<dots> = elts (a*y) \<union> elts (lift (a*y) s)"
         by (simp add: plus_eq_lift)
       finally have "a * u + r' \<in> elts (a * y) \<union> elts (lift (a * y) s)" .
       then show "u \<in> elts y"
       proof
         assume *: "a * u + r' \<in> elts (a * y)"
         show "u \<in> elts y"
         proof -
           obtain v e where v: "v \<in> elts y" "e \<in> elts a" "a * u + r' = a * v + e"
             using * by (auto simp: mult [of _ y] lift_def)
           then have v_k: "v \<in> elts (Vset k)"
             using Vset_succ_TC less_TC_iff succ.prems(2) by blast
           then have "u = v"
             by (metis succ.IH u_k V_equalityI \<open>r' \<in> elts a\<close> le_TC_refl less_TC_iff v(2) v(3) vsubsetD)
           then show ?thesis
             using \<open>v \<in> elts y\<close> by blast
         qed
       next
         assume "a * u + r' \<in> elts (lift (a * y) s)"
         then obtain t where "t \<in> elts s" and t: "a * u + r' = a * y + t"
           using lift_def by auto
         have noteq: "a*y \<noteq> a*u"
         proof
           assume "a*y = a*u"
           then have "lift (a*y) a = lift (a*u) a"
             by metis
           also have "\<dots> \<le> a*x"
             unfolding mult [of _ x] using \<open>u \<in> elts x\<close> by (auto intro: cSUP_upper)
           also have "\<dots> \<le> a*y \<squnion> lift (a*y) s"
             using \<open>elts (a * x) \<subseteq> elts (a * y + s)\<close> plus_eq_lift by auto
           finally have "lift (a*y) a \<le> a*y \<squnion> lift (a*y) s" .
           then have "lift (a*y) a \<le> lift (a*y) s"
             using add_le_cancel_left less_TC_imp_not_le plus_eq_lift \<open>s \<sqsubset> a\<close> by auto
           then have "a \<le> s"
             by (simp add: le_iff_sup lift_eq_lift lift_sup_distrib)
           then show False
             using \<open>s \<sqsubset> a\<close> less_TC_imp_not_le by auto
         qed
         consider "a * u \<unlhd> a * y" | "a * y \<unlhd> a * u"
           using t comparable vle_comparable_def by blast
         then have "False"
         proof cases
           case 1
           then obtain c where "a*y = a*u + c"
             by (metis vle_def)
           then have "c+t = r'"
             by (metis add_right_cancel add.assoc t)
           then have "c \<sqsubset> a"
             using \<open>r' \<in> elts a\<close> less_TC_iff vle2 vle_def by force
           moreover have "c \<noteq> 0"
             using \<open>a * y = a * u + c\<close> noteq by auto
           ultimately show ?thesis
             using \<open>a * y = a * u + c\<close> mult_eq_imp_0 by blast
         next
           case 2
           then obtain c where "a*u = a*y + c"
             by (metis vle_def)
           then have "c+r' = t"
             by (metis add_right_cancel add.assoc t)
           then have "c \<sqsubset> a"
             by (metis \<open>t \<in> elts s\<close> less_TC_iff less_TC_trans \<open>s \<sqsubset> a\<close> vle2 vle_def)
           moreover have "c \<noteq> 0"
             using \<open>a * u = a * y + c\<close> noteq by auto
           ultimately show ?thesis
             using \<open>a * u = a * y + c\<close> mult_eq_imp_0 by blast
         qed
         then show "u \<in> elts y" ..
       qed
     qed
   next
     case (Limit k)
     obtain i j where k: "i \<in> elts k" "j \<in> elts k"
       and x: "x \<in> elts (Vset i)" and y: "y \<in> elts (Vset j)"
       using that Limit by (auto simp: Limit_Vfrom_eq)
     show ?case
     proof (rule Limit.IH [of "i \<squnion> j"])
       show "i \<squnion> j \<in> elts k"
         by (meson k x y Limit.hyps Limit_def Ord_in_Ord Ord_mem_iff_lt Ord_sup union_less_iff)
       show "x \<in> elts (Vset (i \<squnion> j))" "y \<in> elts (Vset (i \<squnion> j))"
         using x y by (auto simp: Vfrom_sup)
       thm Limit.prems
     qed (auto intro: Limit.prems)
   qed
   then show ?thesis
     by (metis two_in_Vset Ord_rank Ord_VsetI rank_lt)
 qed
 
 
 theorem mult_cancellation_lemma:
   assumes "a*x + r = a*y + s" "r \<sqsubset> a" "s \<sqsubset> a"
   shows "x=y \<and> r=s"
   by (metis add_right_cancel mult_cancellation_half antisym assms)
 
 corollary mult_cancellation [simp]:
   fixes a::V
   assumes "a \<noteq> 0"
   shows "a*x = a*y \<longleftrightarrow> x=y"
   by (metis assms nonzero_less_TC mult_cancellation_lemma)
 
 corollary lift_mult_TC_disjoint:
   fixes x::V
   assumes "x \<noteq> y"
   shows "lift (a*x) (TC a) \<sqinter> lift (a*y) (TC a) = 0"
   apply (rule V_equalityI)
   using assms
   by (auto simp: less_TC_def inf_V_def lift_def image_iff dest: mult_cancellation_lemma)
 
 corollary lift_mult_disjoint:
   fixes x::V
   assumes "x \<noteq> y"
   shows "lift (a*x) a \<sqinter> lift (a*y) a = 0"
 proof -
   have "lift (a*x) a \<sqinter> lift (a*y) a \<le> lift (a*x) (TC a) \<sqinter> lift (a*y) (TC a)"
     by (metis TC' inf_mono lift_sup_distrib sup_ge1)
   then show ?thesis
     using assms lift_mult_TC_disjoint by auto
 qed
 
 lemma mult_add_mem:
   assumes "a*x + r \<in> elts (a*y)" "r \<sqsubset> a"
   shows "x \<in> elts y" "r \<in> elts a"
 proof -
   obtain v s where v: "a * x + r = a * v + s" "v \<in> elts y" "s \<in> elts a"
     using assms unfolding mult [of a y] lift_def by auto
   then show "x \<in> elts y"
     by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma vsubsetD)
   show "r \<in> elts a"
     by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma v(1) v(3) vsubsetD)
 qed
 
 lemma mult_add_mem_0 [simp]: "a*x \<in> elts (a*y) \<longleftrightarrow> x \<in> elts y \<and> 0 \<in> elts a"
   proof -
   have "x \<in> elts y"
     if "a * x \<in> elts (a * y) \<and> 0 \<in> elts a"
     using that   using mult_add_mem [of a x 0]
     using nonzero_less_TC by force
   moreover have "a * x \<in> elts (a * y)"
     if "x \<in> elts y" "0 \<in> elts a"
     using that  by (force simp: image_iff mult [of a y] lift_def)
   ultimately show ?thesis
     by (metis mult_eq_0_iff add.right_neutral mult_add_mem(2) nonzero_less_TC)
 qed
 
 lemma zero_mem_mult_iff: "0 \<in> elts (x*y) \<longleftrightarrow> 0 \<in> elts x \<and> 0 \<in> elts y" 
   by (metis Kirby.mult_zero_right mult_add_mem_0)
 
 lemma zero_less_mult_iff [simp]: "0 < x*y \<longleftrightarrow> 0 < x \<and> 0 < y" if "Ord x" 
   using Kirby.mult_eq_0_iff ZFC_in_HOL.neq0_conv by blast
 
 lemma mult_cancel_less_iff [simp]:
   "\<lbrakk>Ord \<alpha>; Ord \<beta>; Ord \<gamma>\<rbrakk> \<Longrightarrow> \<alpha>*\<beta> < \<alpha>*\<gamma> \<longleftrightarrow> \<beta> < \<gamma> \<and> 0 < \<alpha>"
   using mult_add_mem_0 [of \<alpha> \<beta> \<gamma>]
   by (meson Ord_0 Ord_mem_iff_lt Ord_mult)
 
 lemma mult_cancel_le_iff [simp]:
   "\<lbrakk>Ord \<alpha>; Ord \<beta>; Ord \<gamma>\<rbrakk> \<Longrightarrow> \<alpha>*\<beta> \<le> \<alpha>*\<gamma> \<longleftrightarrow> \<beta> \<le> \<gamma> \<or> \<alpha>=0"
   by (metis Ord_linear2 Ord_mult eq_iff leD mult_cancel_less_iff mult_cancellation)
 
 lemma mult_Suc_add_less: "\<lbrakk>\<alpha> < \<gamma>; \<beta> < \<gamma>; Ord \<alpha>; Ord \<beta>; Ord \<gamma>\<rbrakk>  \<Longrightarrow> \<gamma> * ord_of_nat m + \<alpha> < \<gamma> * ord_of_nat (Suc m) + \<beta>"
   apply (simp add: mult_succ add.assoc)
   by (meson Ord_add Ord_linear2 le_less_trans not_add_less_right)
 
 lemma mult_nat_less_add_less:
   assumes "m < n" "\<alpha> < \<gamma>" "\<beta> < \<gamma>" and ord: "Ord \<alpha>" "Ord \<beta>" "Ord \<gamma>"
     shows "\<gamma> * ord_of_nat m + \<alpha> < \<gamma> * ord_of_nat n + \<beta>"
 proof -
   have "Suc m \<le> n"
     using \<open>m < n\<close> by auto
   have "\<gamma> * ord_of_nat m + \<alpha> < \<gamma> * ord_of_nat (Suc m) + \<beta>"
     using assms mult_Suc_add_less by blast
   also have "\<dots> \<le> \<gamma> * ord_of_nat n + \<beta>"
     using Ord_mult Ord_ord_of_nat add_right_mono \<open>Suc m \<le> n\<close> ord mult_cancel_le_iff ord_of_nat_mono_iff by presburger
   finally show ?thesis .
 qed
 
+lemma add_mult_less_add_mult:
+  assumes "x < y" "x \<in> elts \<beta>" "y \<in> elts \<beta>" "\<mu> \<in> elts \<alpha>" "\<nu> \<in> elts \<alpha>" "Ord \<alpha>" "Ord \<beta>"
+    shows "\<alpha>*x + \<mu> < \<alpha>*y + \<nu>"
+proof -
+  obtain "Ord x" "Ord y"
+    using Ord_in_Ord assms by blast
+  then obtain \<delta> where "0 \<in> elts \<delta>" "y = x + \<delta>"
+    by (metis add.right_neutral \<open>x < y\<close> le_Ord_diff less_V_def mem_0_Ord)
+  then show ?thesis
+    apply (simp add: add_mult_distrib add.assoc)
+    by (meson OrdmemD add_le_cancel_left0 \<open>\<mu> \<in> elts \<alpha>\<close> \<open>Ord \<alpha>\<close> less_le_trans zero_imp_le_mult)
+qed
+
+lemma add_mult_less:
+  assumes "\<gamma> \<in> elts \<alpha>" "\<nu> \<in> elts \<beta>" "Ord \<alpha>" "Ord \<beta>"
+    shows "\<alpha> * \<nu> + \<gamma> \<in> elts (\<alpha> * \<beta>)"
+proof -
+  have "Ord \<nu>" 
+    using Ord_in_Ord assms by blast
+  with assms show ?thesis
+    by (metis Ord_mem_iff_lt Ord_succ add_mem_right_cancel mult_cancel_le_iff mult_succ succ_le_iff vsubsetD)
+qed
+
 lemma vcard_mult: "vcard (x * y) = vcard x \<otimes> vcard y"
 proof -
   have 1: "elts (lift (x * u) x) \<approx> elts x" if "u \<in> elts y" for u
     by (metis cardinal_eqpoll eqpoll_sym eqpoll_trans card_lift)
   have 2: "pairwise (\<lambda>u u'. disjnt (elts (lift (x * u) x)) (elts (lift (x * u') x)))  (elts y)"
     by (simp add: pairwise_def disjnt_def) (metis V_disjoint_iff lift_mult_disjoint)
   have "x * y = (SUP u\<in>elts y. lift (x * u) x)"
     using mult by blast
   then have "elts (x * y) \<approx> (\<Union>u\<in>elts y. elts (lift (x * u) x))"
     by simp
   also have "\<dots> \<approx> elts y \<times> elts x"
     using Union_eqpoll_Times [OF 1 2] .
   also have "\<dots> \<approx> elts x \<times> elts y"
     by (simp add: times_commute_eqpoll)
   also have "\<dots> \<approx> elts (vcard x) \<times> elts (vcard y)"
     using cardinal_eqpoll eqpoll_sym times_eqpoll_cong by blast
   also have "\<dots> \<approx> elts (vcard x \<otimes> vcard y)"
     by (simp add: cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym)
   finally have "elts (x * y) \<approx> elts (vcard x \<otimes> vcard y)" .
   then show ?thesis
     by (metis cadd_cmult_distrib cadd_def cardinal_cong cardinal_idem vsum_0_eqpoll)
 qed
 
 proposition TC_mult: "TC(x * y) = (SUP r \<in> elts (TC x). SUP u \<in> elts (TC y). set{x * u + r})"
 proof (cases "x = 0")
   case False
   have *: "TC(x * y) = (SUP u \<in> elts (TC y). lift (x * u) (TC x))" for y
   proof (induction y rule: eps_induct)
     case (step y)
     have "TC(x * y) = (SUP u \<in> elts y. TC (lift (x * u) x))"
       by (simp add: mult [of x y] TC_Sup_distrib image_image)
     also have "\<dots> = (SUP u \<in> elts y. TC(x * u) \<squnion> lift (x * u) (TC x))"
       by (simp add: TC_lift False)
     also have "\<dots> = (SUP u \<in> elts y. (SUP z \<in> elts (TC u). lift (x * z) (TC x)) \<squnion> lift (x * u) (TC x))"
       by (simp add: step)
     also have "\<dots> = (SUP u \<in> elts (TC y). lift (x * u) (TC x))"
       by (auto simp: TC' [of y] image_Un Sup_Un_distrib TC_Sup_distrib cSUP_UNION SUP_sup_distrib)
     finally show ?case .
   qed
   show ?thesis
     by (force simp: * lift_def)
 qed auto
 
 
 corollary vcard_TC_mult: "vcard (TC(x * y)) = vcard (TC x) \<otimes> vcard (TC y)"
 proof -
   have "(\<Union>u\<in>elts (TC x). \<Union>v\<in>elts (TC y). {x * v + u}) = (\<Union>u\<in>elts (TC x). (\<lambda>v. x * v + u) ` elts (TC y))"
     by (simp add: UNION_singleton_eq_range)
   also have "\<dots> \<approx> (\<Union>x\<in>elts (TC x). elts (lift (TC y * x) (TC y)))"
   proof (rule UN_eqpoll_UN)
     show "(\<lambda>v. x * v + u) ` elts (TC y) \<approx> elts (lift (TC y * u) (TC y))"
       if "u \<in> elts (TC x)" for u
     proof -
       have "inj_on (\<lambda>v. x * v + u) (elts (TC y))"
         by (meson inj_onI less_TC_def mult_cancellation_lemma that)
       then have "(\<lambda>v. x * v + u) ` elts (TC y) \<approx> elts (TC y)"
         by (rule inj_on_image_eqpoll_self)
       also have "\<dots> \<approx> elts (lift (TC y * u) (TC y))"
         by (simp add: eqpoll_lift eqpoll_sym)
       finally show ?thesis .
     qed
     show "pairwise (\<lambda>u ya. disjnt ((\<lambda>v. x * v + u) ` elts (TC y)) ((\<lambda>v. x * v + ya) ` elts (TC y))) (elts (TC x))"
       apply (auto simp: pairwise_def disjnt_def)
       using less_TC_def mult_cancellation_lemma by blast
     show "pairwise (\<lambda>u ya. disjnt (elts (lift (TC y * u) (TC y))) (elts (lift (TC y * ya) (TC y)))) (elts (TC x))"
       apply (auto simp: pairwise_def disjnt_def)
       by (metis Int_iff V_disjoint_iff empty_iff lift_mult_disjoint)
   qed
   also have "\<dots> = elts (TC y * TC x)"
     by (metis elts_Sup image_image mult replacement small_elts)
   finally have "(\<Union>u\<in>elts (TC x). \<Union>v\<in>elts (TC y). {x * v + u}) \<approx> elts (TC y * TC x)" .
   then show ?thesis
     apply (subst cmult_commute)
     by (simp add: TC_mult cardinal_cong flip: vcard_mult)
 qed
 
 lemma countable_mult:
   assumes "countable (elts A)" "countable (elts B)"
   shows "countable (elts (A*B))"
 proof -
   have "vcard A \<le> \<aleph>0" "vcard B \<le> \<aleph>0"
     using assms countable_iff_le_Aleph0 by blast+
   then have "vcard (A*B) \<le> \<aleph>0"
     unfolding vcard_mult
     by (metis InfCard_csquare_eq cmult_le_mono Aleph_0 Card_\<omega> InfCard_def order_refl)
   then show ?thesis
     by (simp add: countable_iff_le_Aleph0)
 qed
 
 subsection \<open>Ordertype properties\<close>
 
+lemma ordertype_image_plus:
+  assumes "Ord \<alpha>"
+  shows "ordertype ((+) u ` elts \<alpha>) VWF = \<alpha>"
+proof (subst ordertype_VWF_eq_iff)
+    have 1: "(u + x, u + y) \<in> VWF" if "x \<in> elts \<alpha>" "y \<in> elts \<alpha>" "x < y" for x y
+      using that
+      by (meson Ord_in_Ord Ord_mem_iff_lt add_mem_right_cancel assms mem_imp_VWF)
+  then have 2: "x < y"
+    if "x \<in> elts \<alpha>" "y \<in> elts \<alpha>" "(u + x, u + y) \<in> VWF" for x y
+    using that by (metis Ord_in_Ord Ord_linear_lt VWF_asym assms)
+  show "\<exists>f. bij_betw f ((+) u ` elts \<alpha>) (elts \<alpha>) \<and> (\<forall>x\<in>(+) u ` elts \<alpha>. \<forall>y\<in>(+) u ` elts \<alpha>. (f x < f y) = ((x, y) \<in> VWF))"
+    using 1 2 unfolding bij_betw_def inj_on_def
+    by (rule_tac x="\<lambda>x. odiff x u" in exI) (auto simp: image_iff)
+qed (use assms in auto)
+
 lemma ordertype_diff:
   assumes "\<beta> + \<delta> = \<alpha>" and \<alpha>: "\<delta> \<in> elts \<alpha>" "Ord \<alpha>"
   shows "ordertype (elts \<alpha> - elts \<beta>) VWF = \<delta>"
 proof -
   have *: "elts \<alpha> - elts \<beta> = ((+)\<beta>) ` elts \<delta>"
   proof
     show "elts \<alpha> - elts \<beta> \<subseteq> (+) \<beta> ` elts \<delta>"
       by clarsimp (metis assms(1) image_iff mem_plus_V_E)
     show "(+) \<beta> ` elts \<delta> \<subseteq> elts \<alpha> - elts \<beta>"
       using assms(1) not_add_mem_right by force
   qed
   have "ordertype ((+) \<beta> ` elts \<delta>) VWF = \<delta>"
   proof (subst ordertype_VWF_inc_eq)
     show "elts \<delta> \<subseteq> ON" "ordertype (elts \<delta>) VWF = \<delta>"
       using \<alpha> elts_subset_ON ordertype_eq_Ord by blast+
   qed (use "*" assms elts_subset_ON in auto)
   then show ?thesis
     by (simp add: *)
 qed
 
 lemma ordertype_interval_eq:
   assumes \<alpha>: "Ord \<alpha>" and \<beta>: "Ord \<beta>"
   shows "ordertype ({\<alpha> ..< \<alpha>+\<beta>} \<inter> ON) VWF = \<beta>"
 proof -
   have ON: "(+) \<alpha> ` elts \<beta> \<subseteq> ON"
     using assms Ord_add Ord_in_Ord by blast
   have "({\<alpha> ..< \<alpha>+\<beta>} \<inter> ON) = (+) \<alpha> ` elts \<beta>"
     using assms
     apply (simp add: image_def set_eq_iff)
     by (metis add_less_cancel_left Ord_add Ord_in_Ord Ord_linear2 Ord_mem_iff_lt le_Ord_diff not_add_less_right)
   moreover have "ordertype (elts \<beta>) VWF = ordertype ((+) \<alpha> ` elts \<beta>) VWF"
     using ON \<beta> elts_subset_ON ordertype_VWF_inc_eq by auto
   ultimately show ?thesis
     using \<beta> by auto
 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,2155 +1,2294 @@
 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 small_UN 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
 
 
 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)
 
 text\<open>Introduction rules for the injections (as equivalences)\<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)
 
 text \<open>Elimination rule\<close>
 
 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)
 
 text \<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)
 
 
 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"
+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"
-  using wf_VWF by auto
+  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 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 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
 
 
 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 r" "x \<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 r\<close> by (meson UNIV_I total_on_def)
   then show ?thesis
     by (meson ordermap_mono assms mem_not_sym)
 qed
 
 
 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 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 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 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 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 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) 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 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
 
 
 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
 
 
 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
+
+
 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
diff --git a/thys/ZFC_in_HOL/ZFC_in_HOL.thy b/thys/ZFC_in_HOL/ZFC_in_HOL.thy
--- a/thys/ZFC_in_HOL/ZFC_in_HOL.thy
+++ b/thys/ZFC_in_HOL/ZFC_in_HOL.thy
@@ -1,1247 +1,1289 @@
 section \<open>The ZF Axioms, Ordinals and Transfinite Recursion\<close>
 
 theory ZFC_in_HOL
   imports ZFC_Library
 
 begin
 
 subsection\<open>Syntax and axioms\<close>
 
 hide_const (open) list.set Sum subset
 
 notation
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
   Inf ("\<Sqinter>") and
   Sup ("\<Squnion>")
 
 typedecl V
 
 text\<open>Presentation refined by Dmitriy Traytel\<close>
 axiomatization elts :: "V \<Rightarrow> V set"
  where ext [intro?]:    "elts x = elts y \<Longrightarrow> x=y"
    and down_raw:        "Y \<subseteq> elts x \<Longrightarrow> Y \<in> range elts"
    and Union_raw:       "X \<in> range elts \<Longrightarrow> Union (elts ` X) \<in> range elts"
    and Pow_raw:         "X \<in> range elts \<Longrightarrow> inv elts ` Pow X \<in> range elts"
    and replacement_raw: "X \<in> range elts \<Longrightarrow> f ` X \<in> range elts"
    and inf_raw:         "range (g :: nat \<Rightarrow> V) \<in> range elts"
    and foundation:      "wf {(x,y). x \<in> elts y}"
 
 lemma mem_not_refl [simp]: "i \<notin> elts i"
   using wf_not_refl [OF foundation] by force
 
 lemma mem_not_sym: "\<not> (x \<in> elts y \<and> y \<in> elts x)"
   using wf_not_sym [OF foundation] by force
 
 text \<open>A set is small if it can be injected into the extension of a V-set.\<close>
 definition small :: "'a set \<Rightarrow> bool" 
   where "small X \<equiv> \<exists>V_of :: 'a \<Rightarrow> V. inj_on V_of X \<and> V_of ` X \<in> range elts"
 
 lemma small_empty [iff]: "small {}"
   by (simp add: small_def down_raw)
 
 lemma small_iff_range: "small X \<longleftrightarrow> X \<in> range elts"
   apply (simp add: small_def)
   by (metis inj_on_id2 replacement_raw the_inv_into_onto)
 
 text\<open>Small classes can be mapped to sets.\<close>
 definition   "set X \<equiv> (if small X then inv elts X else inv elts {})"
 
 lemma set_of_elts [simp]: "set (elts x) = x"
   by (force simp add: ext set_def f_inv_into_f small_def)
 
 lemma elts_of_set [simp]: "elts (set X) = (if small X then X else {})"
   by (simp add: ZFC_in_HOL.set_def down_raw f_inv_into_f small_iff_range)
 
 lemma down: "Y \<subseteq> elts x \<Longrightarrow> small Y"
   by (simp add: down_raw small_iff_range)
 
 lemma Union [intro]: "small X \<Longrightarrow> small (Union (elts ` X))"
   by (simp add: Union_raw small_iff_range)
 
 lemma Pow: "small X \<Longrightarrow> small (set ` Pow X)"
   unfolding small_iff_range using Pow_raw set_def down by force
 
 declare replacement_raw [intro,simp]
 
 lemma replacement [intro,simp]:
   assumes "small X"
   shows "small (f ` X)" 
 proof -
   let ?A = "inv_into X f ` (f ` X)"
   have AX: "?A \<subseteq> X"
     by (simp add: image_subsetI inv_into_into)
   have inj: "inj_on f ?A"
     by (simp add: f_inv_into_f inj_on_def)
   have injo: "inj_on (inv_into X f) (f ` X)"
     using inj_on_inv_into by blast
   have "\<exists>V_of. inj_on V_of (f ` X) \<and> V_of ` f ` X \<in> range elts"
     if "inj_on V_of X" and "V_of ` X = elts x"
     for V_of :: "'a \<Rightarrow> V" and x
   proof (intro exI conjI)
     show "inj_on (V_of \<circ> inv_into X f) (f ` X)"
       by (meson \<open>inv_into X f ` f ` X \<subseteq> X\<close> comp_inj_on inj_on_subset injo that)
     have "(\<lambda>x. V_of (inv_into X f (f x))) ` X = elts (set (V_of ` ?A))"
       by (metis AX down elts_of_set image_image image_mono that(2))
     then show "(V_of \<circ> inv_into X f) ` f ` X \<in> range elts"
       by (metis image_comp image_image rangeI)
   qed
   then show ?thesis
     using assms by (auto simp: small_def)
 qed
 
 lemma small_image_iff [simp]: "inj_on f A \<Longrightarrow> small (f ` A) \<longleftrightarrow> small A"
   by (metis replacement the_inv_into_onto)
 
 text \<open>A little bootstrapping is needed to characterise @{term small} for sets of arbitrary type.\<close>
 
 lemma inf: "small (range (g :: nat \<Rightarrow> V))"
   by (simp add: inf_raw small_iff_range)
 
 lemma small_image_nat_V [simp]: "small (g ` N)" for g :: "nat \<Rightarrow> V"
   by (metis (mono_tags, hide_lams) down elts_of_set image_iff inf rangeI subsetI)
 
 lemma Finite_V:
   fixes X :: "V set"
   assumes "finite X" shows "small X"
   using ex_bij_betw_nat_finite [OF assms] unfolding bij_betw_def by (metis small_image_nat_V)
 
 lemma small_insert_V:
   fixes X :: "V set"
   assumes "small X"
   shows "small (insert a X)"
 proof (cases "finite X")
   case True
   then show ?thesis
     by (simp add: Finite_V)
 next
   case False
   show ?thesis
     using infinite_imp_bij_betw2 [OF False]
     by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral)
 qed
 
 lemma small_UN [simp,intro]:
   fixes B :: "V \<Rightarrow> V set"
   assumes X: "small X" and B: "\<And>x. x \<in> X \<Longrightarrow> small (B x)"
   shows "small (\<Union>x\<in>X. B x)"
 proof -
   have "(\<Union> (elts ` (\<lambda>x. set (B x)) ` X)) = (\<Union> (B ` X))"
     using B by force
   then show ?thesis
     using Union [OF replacement [OF X, of "\<lambda>x. set (B x)"]] by simp
 qed
  
 definition vinsert where "vinsert x y \<equiv> set (insert x (elts y))"
 
 lemma elts_vinsert [simp]: "elts (vinsert x y) = insert x (elts y)"
   using down small_insert_V vinsert_def by auto
 
 definition succ where "succ x \<equiv> vinsert x x"
 
 lemma elts_succ [simp]: "elts (succ x) = insert x (elts x)"
   by (simp add: succ_def)
 
 lemma finite_imp_small:
   assumes "finite X" shows "small X"
   using assms
 proof induction
   case empty
   then show ?case
     by simp
 next
   case (insert a X)
   then obtain V_of u where u: "inj_on V_of X" "V_of ` X = elts u"
     by (meson small_def image_iff)
   show ?case
     unfolding small_def
   proof (intro exI conjI)
     show "inj_on (V_of(a:=u)) (insert a X)"
       using u
       apply (clarsimp simp add: inj_on_def)
       by (metis image_eqI mem_not_refl)
     have "(V_of(a:=u)) ` insert a X = elts (vinsert u u)"
       using insert.hyps(2) u(2) by auto
     then show "(V_of(a:=u)) ` insert a X \<in> range elts"
       by (blast intro:  elim: )
   qed
 qed
 
 lemma small_insert:
   assumes "small X"
   shows "small (insert a X)"
 proof (cases "finite X")
   case True
   then show ?thesis
     by (simp add: finite_imp_small)
 next
   case False
   show ?thesis
     using infinite_imp_bij_betw2 [OF False]
     by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral)
 qed
 
 lemma smaller_than_small:
   assumes "small A" "B \<subseteq> A" shows "small B"
   using assms
   by (metis down elts_of_set image_mono small_def small_iff_range subset_inj_on) 
 
 lemma small_insert_iff [iff]: "small (insert a X) \<longleftrightarrow> small X"
   by (meson small_insert smaller_than_small subset_insertI)
 
 lemma small_iff: "small X \<longleftrightarrow> (\<exists>x. X = elts x)"
   by (metis down elts_of_set subset_refl)
 
 lemma small_elts [iff]: "small (elts x)"
   by (auto simp: small_iff)
 
 lemma small_diff [iff]: "small (elts a - X)"
   by (meson Diff_subset down)
 
 lemma small_set [simp]: "small (list.set xs)"
   by (simp add: ZFC_in_HOL.finite_imp_small)
 
 lemma small_upair: "small {x,y}"
   by simp
 
 lemma small_Un: "small (elts x \<union> elts y)"
   using Union [OF small_upair] by auto
 
 lemma small_eqcong: "\<lbrakk>small X; X \<approx> Y\<rbrakk> \<Longrightarrow> small Y"
   by (metis bij_betw_imp_surj_on eqpoll_def replacement)
 
 lemma big_UNIV [simp]: "\<not> small (UNIV::V set)" (is  "\<not> small ?U")
   proof
     assume "small ?U"
     then have "small A" for A :: "V set"
       by (metis (full_types) UNIV_I down small_iff subsetI)
     then have "range elts = UNIV"
       by (meson small_iff surj_def)
   then show False
     by (metis Cantors_paradox Pow_UNIV)
 qed
 
 lemma inj_on_set: "inj_on set (Collect small)"
   by (metis elts_of_set inj_onI mem_Collect_eq)
 
 lemma set_injective [simp]: "\<lbrakk>small X; small Y\<rbrakk> \<Longrightarrow> set X = set Y \<longleftrightarrow> X=Y"
   by (metis elts_of_set)
 
 
 subsection\<open>Type classes and other basic setup\<close>
 
 instantiation V :: zero
 begin
 definition zero_V where "0 \<equiv> set {}"
 instance ..
 end
 
 lemma elts_0 [simp]: "elts 0 = {}"
   by (simp add: zero_V_def)
 
 lemma set_empty [simp]: "set {} = 0"
   by (simp add: zero_V_def)
 
 instantiation V :: one
 begin
 definition one_V where "1 \<equiv> succ 0"
 instance ..
 end
 
 lemma elts_1 [simp]: "elts 1 = {0}"
   by (simp add: one_V_def)
 
 lemma insert_neq_0 [simp]: "set (insert a X) = 0 \<longleftrightarrow> \<not> small X"
   unfolding zero_V_def
   by (metis elts_of_set empty_not_insert set_of_elts small_insert_iff)
 
 instantiation V :: distrib_lattice
 begin
 
 definition inf_V where "inf_V x y \<equiv> set (elts x \<inter> elts y)"
 
 definition sup_V where "sup_V x y \<equiv> set (elts x \<union> elts y)"
 
 definition less_eq_V where "less_eq_V x y \<equiv> elts x \<subseteq> elts y"
 
 definition less_V where "less_V x y \<equiv> less_eq x y \<and> x \<noteq> (y::V)"
 
 instance
 proof
   show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" for x :: V and y :: V
     using ext less_V_def less_eq_V_def by auto
   show "x \<le> x" for x :: V
     by (simp add: less_eq_V_def)
   show "x \<le> z" if "x \<le> y" "y \<le> z" for x y z :: V
     using that by (auto simp: less_eq_V_def)
   show "x = y" if "x \<le> y" "y \<le> x" for x y :: V
     using that by (simp add: ext less_eq_V_def)
   show "inf x y \<le> x" for x y :: V
     by (metis down elts_of_set inf_V_def inf_sup_ord(1) less_eq_V_def)
   show "inf x y \<le> y" for x y :: V
     by (metis Int_lower2 down elts_of_set inf_V_def less_eq_V_def)
   show "x \<le> inf y z" if "x \<le> y" "x \<le> z" for x y z :: V
   proof -
     have "small (elts y \<inter> elts z)"
       by (meson down inf.cobounded1)
     then show ?thesis
       using elts_of_set inf_V_def less_eq_V_def that by auto
   qed
   show "x \<le> x \<squnion> y" for x y :: V
     by (simp add: less_eq_V_def small_Un sup_V_def)
   show "y \<le> x \<squnion> y" for x y :: V
     by (simp add: less_eq_V_def small_Un sup_V_def)
   show "sup y z \<le> x" if "y \<le> x" "(z::V) \<le> x" for x y z :: V
     using elts_of_set less_eq_V_def small_Un sup_V_def that by auto
   show "sup x (inf y z) = inf (x \<squnion> y) (sup x z)" for x y z :: V
   proof -
     have "small (elts y \<inter> elts z)"
       by (meson down inf.cobounded2)
     then show ?thesis
       by (simp add: Un_Int_distrib inf_V_def small_Un sup_V_def)
   qed
 qed
 end
 
 lemma V_equalityI [intro]: "(\<And>x. x \<in> elts a \<longleftrightarrow> x \<in> elts b) \<Longrightarrow> a = b"
   by (meson dual_order.antisym less_eq_V_def subsetI)
 
 lemma vsubsetI [intro!]: "(\<And>x. x \<in> elts a \<Longrightarrow> x \<in> elts b) \<Longrightarrow> a \<le> b"
   by (simp add: less_eq_V_def subsetI)
 
 lemma vsubsetD [elim, intro?]: "a \<le> b \<Longrightarrow> c \<in> elts a \<Longrightarrow> c \<in> elts b"
   using less_eq_V_def by auto
 
 lemma rev_vsubsetD: "c \<in> elts a \<Longrightarrow> a \<le> b \<Longrightarrow> c \<in> elts b"
   \<comment> \<open>The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\<close>
   by (rule vsubsetD)
 
 lemma vsubsetCE [elim,no_atp]: "a \<le> b \<Longrightarrow> (c \<notin> elts a \<Longrightarrow> P) \<Longrightarrow> (c \<in> elts b \<Longrightarrow> P) \<Longrightarrow> P"
   \<comment> \<open>Classical elimination rule.\<close>
   using vsubsetD by blast
 
 lemma set_image_le_iff: "small A \<Longrightarrow> set (f ` A) \<le> B \<longleftrightarrow> (\<forall>x\<in>A. f x \<in> elts B)"
   by auto
 
 lemma eq0_iff: "x = 0 \<longleftrightarrow> (\<forall>y. y \<notin> elts x)"
   by auto
 
 lemma less_eq_V_0_iff [simp]: "x \<le> 0 \<longleftrightarrow> x = 0" for x::V
   by auto
 
 lemma subset_iff_less_eq_V:
   assumes "small B" shows "A \<subseteq> B \<longleftrightarrow> set A \<le> set B \<and> small A"
   using assms down small_iff by auto
 
 lemma small_Collect [simp]: "small A \<Longrightarrow> small {x \<in> A. P x}"
   by (simp add: smaller_than_small)
 
 lemma small_Union_iff: "small (\<Union>(elts ` X)) \<longleftrightarrow> small X"
   proof
   show "small X"
     if "small (\<Union> (elts ` X))"
   proof -
     have "X \<subseteq> set ` Pow (\<Union> (elts ` X))"
       by fastforce
     then show ?thesis
       using Pow subset_iff_less_eq_V that by auto
   qed
 qed auto
 
 lemma not_less_0 [iff]:
   fixes x::V shows "\<not> x < 0"
   by (simp add: less_eq_V_def less_le_not_le)
 
 lemma le_0 [iff]:
   fixes x::V shows "0 \<le> x"
   by auto
 
 lemma min_0L [simp]: "min 0 n = 0" for n :: V
   by (simp add: min_absorb1)
 
 lemma min_0R [simp]: "min n 0 = 0" for n :: V
   by (simp add: min_absorb2)
 
 lemma neq0_conv: "\<And>n::V. n \<noteq> 0 \<longleftrightarrow> 0 < n"
   by (simp add: less_V_def)
 
 
 definition VPow :: "V \<Rightarrow> V"
   where "VPow x \<equiv> set (set ` Pow (elts x))"
 
 lemma VPow_iff [iff]: "y \<in> elts (VPow x) \<longleftrightarrow> y \<le> x"
   using down Pow
   apply (auto simp: VPow_def less_eq_V_def)
   using less_eq_V_def apply fastforce
   done
 
 lemma VPow_le_VPow_iff [simp]: "VPow a \<le> VPow b \<longleftrightarrow> a \<le> b"
   by auto
 
 lemma elts_VPow: "elts (VPow x) = set ` Pow (elts x)"
   by (auto simp: VPow_def Pow)
 
 lemma small_sup_iff [simp]: "small (X \<union> Y) \<longleftrightarrow> small X \<and> small Y" for X::"V set"
   by (metis down small_Un small_iff sup_ge1 sup_ge2)
 
 lemma elts_sup_iff [simp]: "elts (x \<squnion> y) = elts x \<union> elts y"
   by (auto simp: sup_V_def small_Un)
 
 lemma trad_foundation:
   assumes z: "z \<noteq> 0" shows "\<exists>w. w \<in> elts z \<and> w \<sqinter> z = 0"
   using foundation assms
   by (simp add: wf_eq_minimal) (metis Int_emptyI equals0I inf_V_def set_of_elts zero_V_def)
 
 
 instantiation "V" :: Sup
 begin
 definition Sup_V where "Sup_V X \<equiv> if small X then set (Union (elts ` X)) else 0"
 instance ..
 end
 
 instantiation "V" :: Inf
 begin
 definition Inf_V where "Inf_V X \<equiv> if X = {} then 0 else set (Inter (elts ` X))"
 instance ..
 end
 
 lemma V_disjoint_iff: "x \<sqinter> y = 0 \<longleftrightarrow> elts x \<inter> elts y = {}"
   by (metis down elts_of_set inf_V_def inf_le1 zero_V_def)
 
 text\<open>I've no idea why @{term bdd_above} is treated differently from @{term bdd_below}, but anyway\<close>
 lemma bdd_above_iff_small [simp]: "bdd_above X = small X" for X::"V set"
 proof
   show "small X" if "bdd_above X"
   proof -
     obtain a where "\<forall>x\<in>X. x \<le> a"
       using that \<open>bdd_above X\<close> bdd_above_def by blast
     then show "small X"
       by (meson VPow_iff \<open>\<forall>x\<in>X. x \<le> a\<close> down subsetI)
   qed
   show "bdd_above X"
     if "small X"
   proof -
     have "\<forall>x\<in>X. x \<le> \<Squnion> X"
       by (simp add: SUP_upper Sup_V_def Union less_eq_V_def that)
     then show ?thesis
       by (meson bdd_above_def)
   qed
 qed
 
 
 instantiation "V" :: conditionally_complete_lattice
 begin
 
 definition bdd_below_V where "bdd_below_V X \<equiv> X \<noteq> {}"
 
 instance
   proof
   show "\<Sqinter> X \<le> x" if "x \<in> X" "bdd_below X"
     for x :: V and X :: "V set"
     using that by (auto simp: bdd_below_V_def Inf_V_def split: if_split_asm)
   show "z \<le> \<Sqinter> X"
     if "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
     for X :: "V set" and z :: V
     using that
     apply (clarsimp simp add: bdd_below_V_def Inf_V_def less_eq_V_def split: if_split_asm)
     by (meson INT_subset_iff down eq_refl equals0I)
   show "x \<le> \<Squnion> X" if "x \<in> X" and "bdd_above X" for x :: V and X :: "V set"
     using that Sup_V_def by auto
   show "\<Squnion> X \<le> (z::V)" if "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> x \<le> z" for X :: "V set" and z :: V
     using that  by (simp add: SUP_least Sup_V_def less_eq_V_def)
 qed
 end
 
 lemma Sup_upper: "\<lbrakk>x \<in> A; small A\<rbrakk> \<Longrightarrow> x \<le> \<Squnion>A" for A::"V set"
   by (auto simp: Sup_V_def SUP_upper Union less_eq_V_def)
 
 lemma Sup_least:
   fixes z::V shows "(\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
   by (auto simp: Sup_V_def SUP_least less_eq_V_def)
 
 lemma Sup_empty [simp]: "\<Squnion>{} = (0::V)"
   using Sup_V_def by auto
 
 lemma elts_Sup [simp]: "small X \<Longrightarrow> elts (\<Squnion> X) = \<Union>(elts ` X)"
   by (auto simp: Sup_V_def)
 
 lemma sup_V_0_left [simp]: "0 \<squnion> a = a" and sup_V_0_right [simp]: "a \<squnion> 0 = a" for a::V
   by auto
 
 lemma Sup_V_insert:
   fixes x::V assumes "small A" shows "\<Squnion>(insert x A) = x \<squnion> \<Squnion>A"
   by (simp add: assms cSup_insert_If)
 
 lemma Sup_Un_distrib: "\<lbrakk>small A; small B\<rbrakk> \<Longrightarrow> \<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B" for A::"V set"
   by auto
 
 lemma SUP_sup_distrib:
   fixes f :: "V \<Rightarrow> V"
   shows "small A \<Longrightarrow> (SUP x\<in>A. f x \<squnion> g x) = \<Squnion> (f ` A) \<squnion> \<Squnion> (g ` A)"
   by (force simp:)
 
 lemma SUP_const [simp]: "(SUP y \<in> A. a) = (if A = {} then (0::V) else a)"
   by simp
 
 lemma cSUP_subset_mono:
   fixes f :: "'a \<Rightarrow> V set" and g :: "'a \<Rightarrow> V set"
   shows "\<lbrakk>A \<subseteq> B; \<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<rbrakk> \<Longrightarrow> \<Squnion> (f ` A) \<le> \<Squnion> (g ` B)"
   by (simp add: SUP_subset_mono)
 
 lemma mem_Sup_iff [iff]: "x \<in> elts (\<Squnion>X) \<longleftrightarrow> x \<in> \<Union> (elts ` X) \<and> small X"
   using Sup_V_def by auto
 
 lemma cSUP_UNION:
   fixes B :: "V \<Rightarrow> V set" and f :: "V \<Rightarrow> V"
   assumes ne: "small A" and bdd_UN: "small (\<Union>x\<in>A. f ` B x)"
   shows "\<Squnion>(f ` (\<Union>x\<in>A. B x)) = \<Squnion>((\<lambda>x. \<Squnion>(f ` B x)) ` A)"
 proof -
   have bdd: "\<And>x. x \<in> A \<Longrightarrow> small (f ` B x)"
     using bdd_UN subset_iff_less_eq_V
     by (meson SUP_upper smaller_than_small)
   then have bdd2: "small ((\<lambda>x. \<Squnion>(f ` B x)) ` A)"
     using ne(1) by blast
   have "\<Squnion>(f ` (\<Union>x\<in>A. B x)) \<le> \<Squnion>((\<lambda>x. \<Squnion>(f ` B x)) ` A)"
     using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd)
   moreover have "\<Squnion>((\<lambda>x. \<Squnion>(f ` B x)) ` A) \<le> \<Squnion>(f ` (\<Union>x\<in>A. B x))"
     using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN)
   ultimately show ?thesis
     by (rule order_antisym)
 qed
 
 lemma Sup_subset_mono: "small B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Sup A \<le> Sup B" for A::"V set"
   by auto
 
 lemma Sup_le_iff: "small A \<Longrightarrow> Sup A \<le> a \<longleftrightarrow> (\<forall>x\<in>A. x \<le> a)" for A::"V set"
   by auto
 
 lemma SUP_le_iff: "small (f ` A) \<Longrightarrow> \<Squnion>(f ` A) \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)" for f :: "V \<Rightarrow> V"
   by blast
 
 lemma Sup_eq_0_iff [simp]: "\<Squnion>A = 0 \<longleftrightarrow> A \<subseteq> {0} \<or> \<not> small A" for A :: "V set"
   using Sup_upper by fastforce
 
 lemma Sup_Union_commute:
   fixes f :: "V \<Rightarrow> V set"
   assumes "small A" "\<And>x. x\<in>A \<Longrightarrow> small (f x)"
   shows "\<Squnion> (\<Union>x\<in>A. f x) = (SUP x\<in>A. \<Squnion> (f x))"
   using assms 
   by (force simp: subset_iff_less_eq_V intro!: antisym)
 
 lemma Sup_eq_Sup:
   fixes B :: "V set"
   assumes "B \<subseteq> A" "small A" and *: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y \<in> B. x \<le> y"
   shows "Sup A = Sup B"
 proof -
   have "small B"
     using assms subset_iff_less_eq_V by auto
   moreover have "\<exists>y\<in>B. u \<in> elts y"
     if "x \<in> A" "u \<in> elts x" for u x
     using that "*" by blast
   moreover have "\<exists>x\<in>A. v \<in> elts x"
     if "y \<in> B" "v \<in> elts y" for v y
     using that \<open>B \<subseteq> A\<close> by blast
   ultimately show ?thesis
     using assms by auto
 qed
 
 subsection\<open>Successor function\<close>
 
 lemma vinsert_not_empty [simp]: "vinsert a A \<noteq> 0"
   and empty_not_vinsert [simp]: "0 \<noteq> vinsert a A"
   by (auto simp: vinsert_def)
 
 lemma succ_not_0 [simp]: "succ n \<noteq> 0" and zero_not_succ [simp]: "0 \<noteq> succ n"
   by (auto simp: succ_def)
 
 instantiation V :: zero_neq_one
 begin
 instance 
   by intro_classes (metis elts_0 elts_succ empty_iff insert_iff one_V_def set_of_elts)
 end
 
 instantiation V :: zero_less_one
 begin
 instance 
   by intro_classes (simp add: less_V_def)
 end
 
 lemma succ_ne_self [simp]: "i \<noteq> succ i"
   by (metis elts_succ insertI1 mem_not_refl)
 
 lemma succ_notin_self: "succ i \<notin> elts i"
   using elts_succ mem_not_refl by blast
 
 lemma le_succE: "succ i \<le> succ j \<Longrightarrow> i \<le> j"
   using less_eq_V_def mem_not_sym by auto
 
 lemma succ_inject_iff [iff]: "succ i = succ j \<longleftrightarrow> i = j"
   by (simp add: dual_order.antisym le_succE)
 
 lemma inj_succ: "inj succ"
   by (simp add: inj_def)
 
 lemma succ_neq_zero: "succ x \<noteq> 0"
   by (metis elts_0 elts_succ insert_not_empty)
 
 definition pred where "pred i \<equiv> THE j. i = succ j"
 
 lemma pred_succ [simp]: "pred (succ i) = i"
   by (simp add: pred_def)
 
 
 subsection \<open>Ordinals\<close>
 
 definition Transset where "Transset x \<equiv> \<forall>y \<in> elts x. y \<le> x"
 
 definition Ord where "Ord x \<equiv> Transset x \<and> (\<forall>y \<in> elts x. Transset y)"
 
 abbreviation ON where "ON \<equiv> Collect Ord"
 
 subsubsection \<open>Transitive sets\<close>
 
 lemma Transset_0 [iff]: "Transset 0"
   by (auto simp: Transset_def)
 
 lemma Transset_succ [intro]:
   assumes "Transset x" shows "Transset (succ x)"
   using assms
   by (auto simp: Transset_def succ_def less_eq_V_def)
 
 lemma Transset_Sup:
   assumes "\<And>x. x \<in> X \<Longrightarrow> Transset x" shows "Transset (\<Squnion>X)"
 proof (cases "small X")
   case True
   with assms show ?thesis
     by (simp add: Transset_def) (meson Sup_upper assms dual_order.trans)
 qed (simp add: Sup_V_def)
 
 lemma Transset_sup:
   assumes "Transset x" "Transset y" shows "Transset (x \<squnion> y)"
   using Transset_def assms by fastforce
 
 lemma Transset_inf: "\<lbrakk>Transset i; Transset j\<rbrakk> \<Longrightarrow> Transset (i \<sqinter> j)"
   by (simp add: Transset_def rev_vsubsetD)
 
 lemma Transset_VPow: "Transset(i) \<Longrightarrow> Transset(VPow(i))"
   by (auto simp: Transset_def)
 
 lemma Transset_Inf: "(\<And>i. i \<in> A \<Longrightarrow> Transset i) \<Longrightarrow> Transset (\<Sqinter> A)"
   by (force simp: Transset_def Inf_V_def)
 
 lemma Transset_SUP: "(\<And>x. x \<in> A \<Longrightarrow> Transset (B x)) \<Longrightarrow> Transset (\<Squnion> (B ` A))"
   by (metis Transset_Sup imageE)
 
 lemma Transset_INT: "(\<And>x. x \<in> A \<Longrightarrow> Transset (B x)) \<Longrightarrow> Transset (\<Sqinter> (B ` A))"
   by (metis Transset_Inf imageE)
 
 
 subsubsection \<open>Zero, successor, sups\<close>
 
 lemma Ord_0 [iff]: "Ord 0"
   by (auto simp: Ord_def)
 
 lemma Ord_succ [intro]:
   assumes "Ord x" shows "Ord (succ x)"
   using assms by (auto simp: Ord_def)
 
 lemma Ord_Sup:
   assumes "\<And>x. x \<in> X \<Longrightarrow> Ord x" shows "Ord (\<Squnion>X)"
 proof (cases "small X")
   case True
   with assms show ?thesis
     by (auto simp: Ord_def Transset_Sup)
 qed (simp add: Sup_V_def)
 
 lemma Ord_Union:
   assumes "\<And>x. x \<in> X \<Longrightarrow> Ord x" "small X" shows "Ord (set (\<Union> (elts ` X)))"
   by (metis Ord_Sup Sup_V_def assms)
 
 lemma Ord_sup:
   assumes "Ord x" "Ord y" shows "Ord (x \<squnion> y)"
   using assms
   proof (clarsimp simp: Ord_def)
   show "Transset (x \<squnion> y) \<and> (\<forall>y\<in>elts x \<union> elts y. Transset y)"
     if "Transset x" "Transset y" "\<forall>y\<in>elts x. Transset y" "\<forall>y\<in>elts y. Transset y"
     using that small_Un sup_V_def Transset_sup by auto
 qed
 
 lemma big_ON [simp]: "\<not> small ON"
 proof
   assume "small ON"
   then have "set ON \<in> ON"
     by (metis Ord_Union Ord_succ Sup_upper elts_Sup elts_succ insertI1 mem_Collect_eq mem_not_refl set_of_elts vsubsetD)
   then show False
     by (metis \<open>small ON\<close> elts_of_set mem_not_refl)
 qed
 
 lemma Ord_1 [iff]: "Ord 1"
   using Ord_succ one_V_def succ_def vinsert_def by fastforce
 
 lemma OrdmemD: "Ord k \<Longrightarrow> j \<in> elts k \<Longrightarrow> j < k"
   using Ord_def Transset_def less_V_def by auto
 
 lemma Ord_trans: "\<lbrakk> i \<in> elts j;  j \<in> elts k;  Ord k \<rbrakk>  \<Longrightarrow> i \<in> elts k"
   using Ord_def Transset_def by blast
 
 lemma mem_0_Ord:
   assumes k: "Ord k" and knz: "k \<noteq> 0" shows "0 \<in> elts k"
   by (metis Ord_def Transset_def inf.orderE k knz trad_foundation)
 
 lemma Ord_in_Ord: "\<lbrakk> Ord k;  m \<in> elts k \<rbrakk>  \<Longrightarrow> Ord m"
   using Ord_def Ord_trans by blast
 
 lemma OrdI: "\<lbrakk>Transset i; \<And>x. x \<in> elts i \<Longrightarrow> Transset x\<rbrakk> \<Longrightarrow> Ord i"
   by (simp add: Ord_def)
 
 lemma Ord_is_Transset: "Ord i \<Longrightarrow> Transset i"
   by (simp add: Ord_def)
 
 lemma Ord_contains_Transset: "\<lbrakk>Ord i; j \<in> elts i\<rbrakk> \<Longrightarrow> Transset j"
   using Ord_def by blast
 
 lemma ON_imp_Ord:
   assumes "H \<subseteq> ON" "x \<in> H"
   shows "Ord x"
   using assms by blast
 
 lemma elts_subset_ON: "Ord \<alpha> \<Longrightarrow> elts \<alpha> \<subseteq> ON"
   using Ord_in_Ord by blast
 
 lemma Transset_pred [simp]: "Transset x \<Longrightarrow> \<Squnion>(elts (succ x)) = x"
   by (fastforce simp: Transset_def)
 
 lemma Ord_pred [simp]: "Ord \<beta> \<Longrightarrow> \<Squnion> (insert \<beta> (elts \<beta>)) = \<beta>"
   using Ord_def Transset_pred by auto
 
 
 subsubsection \<open>Induction, Linearity, etc.\<close>
 
 lemma Ord_induct [consumes 1, case_names step]:
   assumes k: "Ord k"
       and step: "\<And>x.\<lbrakk> Ord x; \<And>y. y \<in> elts x \<Longrightarrow> P y \<rbrakk>  \<Longrightarrow> P x"
     shows "P k"
   using foundation k
 proof (induction k rule: wf_induct_rule)
   case (less x)
   then show ?case
     using Ord_in_Ord local.step by auto
 qed
 
 text \<open>Comparability of ordinals\<close>
 lemma Ord_linear: "Ord k \<Longrightarrow> Ord l \<Longrightarrow> k \<in> elts l \<or> k=l \<or> l \<in> elts k"
 proof (induct k arbitrary: l rule: Ord_induct)
   case (step k)
   note step_k = step
   show ?case using \<open>Ord l\<close>
     proof (induct l rule: Ord_induct)
       case (step l)
       thus ?case using step_k
         by (metis Ord_trans V_equalityI)
     qed
 qed
 
 text \<open>The trichotomy law for ordinals\<close>
 lemma Ord_linear_lt:
   assumes "Ord k" "Ord l"
   obtains (lt) "k < l" | (eq) "k=l" | (gt) "l < k"
   using Ord_linear OrdmemD assms by blast
 
 lemma Ord_linear2:
   assumes "Ord k" "Ord l"
   obtains (lt) "k < l" | (ge) "l \<le> k"
   by (metis Ord_linear_lt eq_refl assms order.strict_implies_order)
 
 lemma Ord_linear_le:
   assumes "Ord k" "Ord l"
   obtains (le) "k \<le> l" | (ge) "l \<le> k"
   by (meson Ord_linear2 le_less assms)
 
 lemma union_less_iff [simp]: "\<lbrakk>Ord i; Ord j\<rbrakk> \<Longrightarrow> i \<squnion> j < k \<longleftrightarrow> i<k \<and> j<k"
   by (metis Ord_linear_le le_iff_sup sup.order_iff sup.strict_boundedE)
 
 lemma Ord_mem_iff_lt: "Ord k \<Longrightarrow> Ord l \<Longrightarrow> k \<in> elts l \<longleftrightarrow> k < l"
   by (metis Ord_linear OrdmemD less_le_not_le)
 
 lemma Ord_Collect_lt: "Ord \<alpha> \<Longrightarrow> {\<xi>. Ord \<xi> \<and> \<xi> < \<alpha>} = elts \<alpha>"
   by (auto simp flip: Ord_mem_iff_lt elim: Ord_in_Ord OrdmemD)
 
+lemma Ord_not_less: "\<lbrakk>Ord x; Ord y\<rbrakk> \<Longrightarrow> \<not> x < y \<longleftrightarrow> y \<le> x"
+  by (metis (no_types) Ord_linear2 leD)
+
+lemma Ord_not_le: "\<lbrakk>Ord x; Ord y\<rbrakk> \<Longrightarrow> \<not> x \<le> y \<longleftrightarrow> y < x"
+  by (metis (no_types) Ord_linear2 leD)
+
 lemma le_succ_iff: "Ord i \<Longrightarrow> Ord j \<Longrightarrow> succ i \<le> succ j \<longleftrightarrow> i \<le> j"
   by (metis Ord_linear_le Ord_succ le_succE order_antisym)
 
 lemma succ_le_iff: "Ord i \<Longrightarrow> Ord j \<Longrightarrow> succ i \<le> j \<longleftrightarrow> i < j"
   using Ord_mem_iff_lt dual_order.strict_implies_order less_eq_V_def by fastforce
 
 lemma succ_in_Sup_Ord:
   assumes eq: "succ \<beta> = \<Squnion>A" and "small A" "A \<subseteq> ON" "Ord \<beta>"
   shows "succ \<beta> \<in> A"
 proof -
   have "\<not> \<Squnion>A \<le> \<beta>"
     using eq \<open>Ord \<beta>\<close> succ_le_iff by fastforce
   then show ?thesis
     using assms by (metis Ord_linear2 Sup_least Sup_upper eq_iff mem_Collect_eq subsetD succ_le_iff)
 qed
 
 lemma zero_in_succ [simp,intro]: "Ord i \<Longrightarrow> 0 \<in> elts (succ i)"
   using mem_0_Ord by auto
 
 lemma Ord_finite_Sup: "\<lbrakk>finite A; A \<subseteq> ON; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<Squnion>A \<in> A"
 proof (induction A rule: finite_induct)
   case (insert x A)
   then have *: "small A" "A \<subseteq> ON" "Ord x"
     by (auto simp add: ZFC_in_HOL.finite_imp_small insert.hyps)
   show ?case
   proof (cases "A = {}")
     case False
     then have "\<Squnion>A \<in> A"
       using insert by blast
     then have "\<Squnion>A \<le> x" if "x \<squnion> \<Squnion>A \<notin> A"
       using * by (metis ON_imp_Ord Ord_linear_le sup.absorb2 that)
     then show ?thesis
       by (fastforce simp: \<open>small A\<close> Sup_V_insert)
   qed auto
 qed auto
 
 
 subsubsection \<open>The natural numbers\<close>
 
 primrec ord_of_nat :: "nat \<Rightarrow> V" where
   "ord_of_nat 0 = 0"
 | "ord_of_nat (Suc n) = succ (ord_of_nat n)"
 
 lemma ord_of_nat_eq_initial: "ord_of_nat n = set (ord_of_nat ` {..<n})"
   by (induction n) (auto simp: lessThan_Suc succ_def)
 
 lemma mem_ord_of_nat_iff [simp]: "x \<in> elts (ord_of_nat n) \<longleftrightarrow> (\<exists>m<n. x = ord_of_nat m)"
   by (subst ord_of_nat_eq_initial) auto
 
 lemma elts_ord_of_nat: "elts (ord_of_nat k) = ord_of_nat ` {..<k}"
   by auto
 
 lemma Ord_equality: "Ord i \<Longrightarrow> i = \<Squnion> (succ ` elts i)"
   by (force intro: Ord_trans)
 
 lemma Ord_ord_of_nat [simp]: "Ord (ord_of_nat k)"
   by (induct k, auto)
 
 lemma ord_of_nat_equality: "ord_of_nat n = \<Squnion> ((succ \<circ> ord_of_nat) ` {..<n})"
   by (metis Ord_equality Ord_ord_of_nat elts_of_set image_comp small_image_nat_V ord_of_nat_eq_initial)
 
 definition \<omega> :: V where "\<omega> \<equiv> set (range ord_of_nat)"
 
 lemma elts_\<omega>: "elts \<omega> = {\<alpha>. \<exists>n. \<alpha> = ord_of_nat n}"
   by (auto simp: \<omega>_def image_iff)
 
 lemma nat_into_Ord [simp]: "n \<in> elts \<omega> \<Longrightarrow> Ord n"
   by (metis Ord_ord_of_nat \<omega>_def elts_of_set image_iff inf)
 
 lemma Sup_\<omega>: "\<Squnion>(elts \<omega>) = \<omega>"
   unfolding \<omega>_def by force
 
 lemma Ord_\<omega> [iff]: "Ord \<omega>"
   by (metis Ord_Sup Sup_\<omega> nat_into_Ord)
 
 lemma zero_in_omega [iff]: "0 \<in> elts \<omega>"
   by (metis \<omega>_def elts_of_set inf ord_of_nat.simps(1) rangeI)
 
 lemma succ_in_omega [simp]: "n \<in> elts \<omega> \<Longrightarrow> succ n \<in> elts \<omega>"
   by (metis \<omega>_def elts_of_set image_iff small_image_nat_V ord_of_nat.simps(2) rangeI)
 
 lemma ord_of_eq_0: "ord_of_nat j = 0 \<Longrightarrow> j = 0"
   by (induct j) (auto simp: succ_neq_zero)
 
 lemma ord_of_nat_le_omega: "ord_of_nat n \<le> \<omega>"
   by (metis Sup_\<omega> ZFC_in_HOL.Sup_upper \<omega>_def elts_of_set inf rangeI)
 
 lemma ord_of_eq_0_iff [simp]: "ord_of_nat n = 0 \<longleftrightarrow> n=0"
   by (auto simp: ord_of_eq_0)
 
 lemma ord_of_nat_inject [iff]: "ord_of_nat i = ord_of_nat j \<longleftrightarrow> i=j"
 proof (induct i arbitrary: j)
   case 0 show ?case
     using ord_of_eq_0 by auto
 next
   case (Suc i) then show ?case
     by auto (metis elts_0 elts_succ insert_not_empty not0_implies_Suc ord_of_nat.simps succ_inject_iff)
 qed
 
 corollary inj_ord_of_nat: "inj ord_of_nat"
   by (simp add: linorder_injI)
 
 corollary countable:
   assumes "countable X" shows "small X"
 proof -
   have "X \<subseteq> range (from_nat_into X)"
     by (simp add: assms subset_range_from_nat_into)
   then show ?thesis
     by (meson inf_raw inj_ord_of_nat replacement small_def smaller_than_small)
 qed
 
 corollary infinite_\<omega>: "infinite (elts \<omega>)"
   using range_inj_infinite [of ord_of_nat]
   by (simp add: \<omega>_def inj_ord_of_nat)
 
 corollary ord_of_nat_mono_iff [iff]: "ord_of_nat i \<le> ord_of_nat j \<longleftrightarrow> i \<le> j"
   by (metis Ord_def Ord_ord_of_nat Transset_def eq_iff mem_ord_of_nat_iff not_less ord_of_nat_inject)
 
+corollary ord_of_nat_strict_mono_iff [iff]: "ord_of_nat i < ord_of_nat j \<longleftrightarrow> i < j"
+  by (simp add: less_le_not_le)
+
 lemma small_image_nat [simp]:
   fixes N :: "nat set" shows "small (g ` N)"
   by (simp add: countable)
 
 lemma finite_Ord_omega: "\<alpha> \<in> elts \<omega> \<Longrightarrow> finite (elts \<alpha>)"
   proof (clarsimp simp add: \<omega>_def)
   show "finite (elts (ord_of_nat n))" if "\<alpha> = ord_of_nat n" for n
     using that by (simp add: ord_of_nat_eq_initial [of n])
 qed
 
 lemma infinite_Ord_omega: "Ord \<alpha> \<Longrightarrow> infinite (elts \<alpha>) \<Longrightarrow> \<omega> \<le> \<alpha>"
   by (meson Ord_\<omega> Ord_linear2 Ord_mem_iff_lt finite_Ord_omega)
 
 lemma ord_of_minus_1: "n > 0 \<Longrightarrow> ord_of_nat n = succ (ord_of_nat (n - 1))"
   by (metis Suc_diff_1 ord_of_nat.simps(2))
 
 lemma card_ord_of_nat [simp]: "card (elts (ord_of_nat m)) = m"
   by (induction m) (auto simp: \<omega>_def finite_Ord_omega)
 
 lemma ord_of_nat_\<omega> [iff]:"ord_of_nat n \<in> elts \<omega>"
   by (simp add: \<omega>_def)
 
 lemma succ_\<omega>_iff [iff]: "succ n \<in> elts \<omega> \<longleftrightarrow> n \<in> elts \<omega>"
   by (metis Ord_\<omega> OrdmemD elts_vinsert insert_iff less_V_def succ_def succ_in_omega vsubsetD)
 
 lemma \<omega>_gt0: "\<omega> > 0"
   by (simp add: OrdmemD)
 
 lemma \<omega>_gt1: "\<omega> > 1"
   by (simp add: OrdmemD one_V_def)
 
 subsubsection\<open>Limit ordinals\<close>
 
 definition Limit :: "V\<Rightarrow>bool"
   where "Limit i \<equiv> Ord i \<and> 0 \<in> elts i \<and> (\<forall>y. y \<in> elts i \<longrightarrow> succ y \<in> elts i)"
 
 lemma zero_not_Limit [iff]: "\<not> Limit 0"
   by (simp add: Limit_def)
 
 lemma not_succ_Limit [simp]: "\<not> Limit(succ i)"
   by (metis Limit_def Ord_mem_iff_lt elts_succ insertI1 less_irrefl)
 
 lemma Limit_is_Ord: "Limit \<xi> \<Longrightarrow> Ord \<xi>"
   by (simp add: Limit_def)
 
 lemma succ_in_Limit_iff: "Limit \<xi> \<Longrightarrow> succ \<alpha> \<in> elts \<xi> \<longleftrightarrow> \<alpha> \<in> elts \<xi>"
   by (metis Limit_def OrdmemD elts_succ insertI1 less_V_def vsubsetD)
 
 lemma Limit_eq_Sup_self [simp]: "Limit i \<Longrightarrow> Sup (elts i) = i"
   apply (rule order_antisym)
   apply (simp add: Limit_def Ord_def Transset_def Sup_least)
   by (metis Limit_def Ord_equality Sup_V_def SUP_le_iff Sup_upper small_elts)
 
 lemma zero_less_Limit: "Limit \<beta> \<Longrightarrow> 0 < \<beta>"
   by (simp add: Limit_def OrdmemD)
 
 lemma non_Limit_ord_of_nat [iff]: "\<not> Limit (ord_of_nat m)"
   by (metis Limit_def mem_ord_of_nat_iff not_succ_Limit ord_of_eq_0_iff ord_of_minus_1)
 
 lemma Limit_omega [iff]: "Limit \<omega>"
   by (simp add: Limit_def)
 
 lemma omega_nonzero [simp]: "\<omega> \<noteq> 0"
   using Limit_omega by fastforce
 
 lemma Ord_cases_lemma:
   assumes "Ord k" shows "k = 0 \<or> (\<exists>j. k = succ j) \<or> Limit k"
 proof (cases "Limit k")
   case False
   have "succ j \<in> elts k" if  "\<forall>j. k \<noteq> succ j" "j \<in> elts k" for j
     by (metis Ord_in_Ord Ord_linear Ord_succ assms elts_succ insertE mem_not_sym that)
   with assms show ?thesis
     by (auto simp: Limit_def mem_0_Ord)
 qed auto
 
 lemma Ord_cases [cases type: V, case_names 0 succ limit]:
   assumes "Ord k"
   obtains "k = 0" | l where "Ord l" "succ l = k" | "Limit k"
   by (metis assms Ord_cases_lemma Ord_in_Ord elts_succ insertI1)
 
 lemma non_succ_LimitI:
   assumes "i\<noteq>0" "Ord(i)" "\<And>y. succ(y) \<noteq> i"
   shows "Limit(i)"
   using Ord_cases_lemma assms by blast
 
 lemma Ord_induct3 [consumes 1, case_names 0 succ Limit, induct type: V]:
   assumes \<alpha>: "Ord \<alpha>"
     and P: "P 0" "\<And>\<alpha>. \<lbrakk>Ord \<alpha>; P \<alpha>\<rbrakk> \<Longrightarrow> P (succ \<alpha>)"
            "\<And>\<alpha>. \<lbrakk>Limit \<alpha>; \<And>\<xi>. \<xi> \<in> elts \<alpha> \<Longrightarrow> P \<xi>\<rbrakk> \<Longrightarrow> P (SUP \<xi> \<in> elts \<alpha>. \<xi>)"
   shows "P \<alpha>"
   using \<alpha>
 proof (induction \<alpha> rule: Ord_induct)
   case (step \<alpha>)
   then show ?case
     by (metis Limit_eq_Sup_self Ord_cases P elts_succ image_ident insertI1)
 qed
 
 
 subsubsection\<open>Properties of LEAST for ordinals\<close>
+
 lemma
   assumes "Ord k" "P k"
   shows Ord_LeastI: "P (LEAST i. Ord i \<and> P i)" and Ord_Least_le: "(LEAST i. Ord i \<and> P i) \<le> k"
 proof -
   have "P (LEAST i. Ord i \<and> P i) \<and> (LEAST i. Ord i \<and> P i) \<le> k"
     using assms
   proof (induct k rule: Ord_induct)
     case (step x) then have "P x" by simp
     show ?case proof (rule classical)
       assume assm: "\<not> (P (LEAST a. Ord a \<and> P a) \<and> (LEAST a. Ord a \<and> P a) \<le> x)"
       have "\<And>y. Ord y \<and> P y \<Longrightarrow> x \<le> y"
       proof (rule classical)
         fix y
         assume y: "Ord y \<and> P y" "\<not> x \<le> y"
         with step obtain "P (LEAST a. Ord a \<and> P a)" and le: "(LEAST a. Ord a \<and> P a) \<le> y"
           by (meson Ord_linear2 Ord_mem_iff_lt)
         with assm have "x < (LEAST a. Ord a \<and> P a)"
           by (meson Ord_linear_le y order.trans \<open>Ord x\<close>)
         then show "x \<le> y"
           using le by auto
       qed
       then have Least: "(LEAST a. Ord a \<and> P a) = x"
         by (simp add: Least_equality \<open>Ord x\<close> step.prems)
       with \<open>P x\<close> show ?thesis by simp
     qed
   qed
   then show "P (LEAST i. Ord i \<and> P i)" and "(LEAST i. Ord i \<and> P i) \<le> k" by auto
 qed
 
 lemma Ord_Least:
   assumes "Ord k" "P k"
   shows "Ord (LEAST i. Ord i \<and> P i)"
 proof -
   have "Ord (LEAST i. Ord i \<and> (Ord i \<and> P i))"
     using Ord_LeastI [where P = "\<lambda>i. Ord i \<and> P i"] assms by blast
   then show ?thesis
     by simp
 qed
 
 \<comment> \<open>The following 3 lemmas are due to Brian Huffman\<close>
 lemma Ord_LeastI_ex: "\<exists>i. Ord i \<and> P i \<Longrightarrow> P (LEAST i. Ord i \<and> P i)"
   using Ord_LeastI by blast
 
 lemma Ord_LeastI2:
   "\<lbrakk>Ord a; P a; \<And>x. \<lbrakk>Ord x; P x\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q (LEAST i. Ord i \<and> P i)"
   by (blast intro: Ord_LeastI Ord_Least)
 
 lemma Ord_LeastI2_ex:
   "\<exists>a. Ord a \<and> P a \<Longrightarrow> (\<And>x. \<lbrakk>Ord x; P x\<rbrakk> \<Longrightarrow> Q x) \<Longrightarrow> Q (LEAST i. Ord i \<and> P i)"
   by (blast intro: Ord_LeastI_ex Ord_Least)
 
 lemma Ord_LeastI2_wellorder:
   assumes "Ord a" "P a"
   and "\<And>a. \<lbrakk> P a; \<forall>b. Ord b \<and> P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
   shows "Q (LEAST i. Ord i \<and> P i)"
 proof (rule LeastI2_order)
   show "Ord (LEAST i. Ord i \<and> P i) \<and> P (LEAST i. Ord i \<and> P i)"
     using Ord_Least Ord_LeastI assms by auto
 next
   fix y assume "Ord y \<and> P y" thus "(LEAST i. Ord i \<and> P i) \<le> y"
     by (simp add: Ord_Least_le)
 next
   fix x assume "Ord x \<and> P x" "\<forall>y. Ord y \<and> P y \<longrightarrow> x \<le> y" thus "Q x"
     by (simp add: assms(3))
 qed
 
 lemma Ord_LeastI2_wellorder_ex:
   assumes "\<exists>x. Ord x \<and> P x"
   and "\<And>a. \<lbrakk> P a; \<forall>b. Ord b \<and> P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
   shows "Q (LEAST i. Ord i \<and> P i)"
 using assms by clarify (blast intro!: Ord_LeastI2_wellorder)
 
 lemma not_less_Ord_Least: "\<lbrakk>k < (LEAST x. Ord x \<and> P x); Ord k\<rbrakk> \<Longrightarrow> \<not> P k"
   using Ord_Least_le less_le_not_le by auto
 
 lemma exists_Ord_Least_iff: "(\<exists>\<alpha>. Ord \<alpha> \<and> P \<alpha>) \<longleftrightarrow> (\<exists>\<alpha>. Ord \<alpha> \<and> P \<alpha> \<and> (\<forall>\<beta> < \<alpha>. Ord \<beta> \<longrightarrow> \<not> P \<beta>))" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs thus ?lhs by blast
 next
   assume H: ?lhs then obtain \<alpha> where \<alpha>: "Ord \<alpha>" "P \<alpha>" by blast
   let ?x = "LEAST \<alpha>. Ord \<alpha> \<and> P \<alpha>"
   have "Ord ?x"
     by (metis Ord_Least \<alpha>)
   moreover
   { fix \<beta> assume m: "\<beta> < ?x" "Ord \<beta>"
     from not_less_Ord_Least[OF m] have "\<not> P \<beta>" . }
   ultimately show ?rhs
     using Ord_LeastI_ex[OF H] by blast
 qed
 
+lemma Ord_mono_imp_increasing:
+  assumes fun_hD: "h \<in> D \<rightarrow> D"
+    and mono_h: "strict_mono_on h D" 
+    and "D \<subseteq> ON" and \<nu>: "\<nu> \<in> D"
+  shows "\<nu> \<le> h \<nu>"
+proof (rule ccontr)
+  assume non: "\<not> \<nu> \<le> h \<nu>"
+  define \<mu> where "\<mu> \<equiv> LEAST \<mu>. Ord \<mu> \<and> \<not> \<mu> \<le> h \<mu> \<and> \<mu> \<in> D"
+  have "Ord \<nu>"
+    using \<nu> \<open>D \<subseteq> ON\<close> by blast
+  then have \<mu>: "\<not> \<mu> \<le> h \<mu> \<and> \<mu> \<in> D"
+    unfolding \<mu>_def by (rule Ord_LeastI) (simp add: \<nu> non)
+  have "Ord (h \<nu>)"
+    using assms by auto
+  then have "Ord (h (h \<nu>))"
+    by (meson ON_imp_Ord \<nu> assms funcset_mem)
+  have "Ord \<mu>"
+    using \<mu> \<open>D \<subseteq> ON\<close> by blast
+  then have "h \<mu> < \<mu>"
+    by (metis ON_imp_Ord Ord_linear2 PiE \<mu> \<open>D \<subseteq> ON\<close> fun_hD)
+  then have "\<not> h \<mu> \<le> h (h \<mu>)"
+    using \<mu> fun_hD mono_h by (force simp: strict_mono_on_def)
+  moreover have *: "h \<mu> \<in> D"
+    using \<mu> fun_hD by auto
+  moreover have "Ord (h \<mu>)"
+    using \<open>D \<subseteq> ON\<close> * by blast
+  ultimately have "\<mu> \<le> h \<mu>"
+    by (simp add: \<mu>_def Ord_Least_le)
+  then show False
+    using \<mu> by blast
+qed
+
 lemma le_Sup_iff:
   assumes "A \<subseteq> ON" "Ord x" "small A" shows "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y \<in> ON. y<x \<longrightarrow> (\<exists>a\<in>A. y < a))"
 proof (intro iffI ballI impI)
   show "\<exists>a\<in>A. y < a"
     if "x \<le> \<Squnion> A" "y \<in> ON" "y < x"
     for y
   proof -
     have "\<not> \<Squnion> A \<le> y" "Ord y"
       using that by auto
     then show ?thesis
       by (metis Ord_linear2 Sup_least \<open>A \<subseteq> ON\<close> mem_Collect_eq subset_eq)
   qed
   show "x \<le> \<Squnion> A"
     if "\<forall>y\<in>ON. y < x \<longrightarrow> (\<exists>a\<in>A. y < a)"
     using that assms
     by (metis Ord_Sup Ord_linear_le Sup_upper less_le_not_le mem_Collect_eq subsetD)
 qed
 
 lemma le_SUP_iff: "\<lbrakk>f ` A \<subseteq> ON; Ord x; small A\<rbrakk> \<Longrightarrow> x \<le> \<Squnion>(f ` A) \<longleftrightarrow> (\<forall>y \<in> ON. y<x \<longrightarrow> (\<exists>i\<in>A. y < f i))"
   by (simp add: le_Sup_iff)
 
 subsection\<open>Transfinite Recursion and the V-levels\<close>
 
 definition transrec :: "[[V\<Rightarrow>V,V]\<Rightarrow>V, V] \<Rightarrow> V"
   where "transrec H a \<equiv> wfrec {(x,y). x \<in> elts y} H a"
 
 lemma transrec: "transrec H a = H (\<lambda>x \<in> elts a. transrec H x) a"
 proof -
   have "(cut (wfrec {(x, y). x \<in> elts y} H) {(x, y). x \<in> elts y} a)
       = (\<lambda>x\<in>elts a. wfrec {(x, y). x \<in> elts y} H x)"
     by (force simp: cut_def)
   then show ?thesis
     unfolding transrec_def
     by (simp add: foundation wfrec)
 qed
 
 text\<open>Avoids explosions in proofs; resolve it with a meta-level definition\<close>
 lemma def_transrec:
     "\<lbrakk>\<And>x. f x \<equiv> transrec H x\<rbrakk> \<Longrightarrow> f a = H(\<lambda>x \<in> elts a. f x) a"
   by (metis restrict_ext transrec)
 
 lemma eps_induct [case_names step]:
   assumes "\<And>x. (\<And>y. y \<in> elts x \<Longrightarrow> P y) \<Longrightarrow> P x"
   shows "P a"
   using wf_induct [OF foundation] assms by auto
 
 
 definition Vfrom :: "[V,V] \<Rightarrow> V"
   where "Vfrom a \<equiv> transrec (\<lambda>f x. a \<squnion> \<Squnion>((\<lambda>y. VPow(f y)) ` elts x))"
 
 abbreviation Vset :: "V \<Rightarrow> V" where "Vset \<equiv> Vfrom 0"
 
 lemma Vfrom: "Vfrom a i = a \<squnion> \<Squnion>((\<lambda>j. VPow(Vfrom a j)) ` elts i)"
   apply (subst Vfrom_def)
   apply (subst transrec)
   using Vfrom_def by auto
 
 lemma Vfrom_0 [simp]: "Vfrom a 0 = a"
   by (subst Vfrom) auto
 
 lemma Vset: "Vset i = \<Squnion>((\<lambda>j. VPow(Vset j)) ` elts i)"
   by (subst Vfrom) auto
 
 lemma Vfrom_mono1:
   assumes "a \<le> b" shows "Vfrom a i \<le> Vfrom b i"
 proof (induction i rule: eps_induct)
   case (step i)
   then have "a \<squnion> (SUP j\<in>elts i. VPow (Vfrom a j)) \<le> b \<squnion> (SUP j\<in>elts i. VPow (Vfrom b j))"
     by (intro sup_mono cSUP_subset_mono \<open>a \<le> b\<close>) auto
   then show ?case
     by (metis Vfrom)
 qed
 
 lemma Vfrom_mono2: "Vfrom a i \<le> Vfrom a (i \<squnion> j)"
 proof (induction arbitrary: j rule: eps_induct)
   case (step i)
   then have "a \<squnion> (SUP j\<in>elts i. VPow (Vfrom a j))
            \<le> a \<squnion> (SUP j\<in>elts (i \<squnion> j). VPow (Vfrom a j))"
     by (intro sup_mono cSUP_subset_mono order_refl) auto
   then show ?case
     by (metis Vfrom)
 qed
 
 lemma Vfrom_mono: "\<lbrakk>Ord i; a\<le>b; i\<le>j\<rbrakk> \<Longrightarrow> Vfrom a i \<le> Vfrom b j"
   by (metis (no_types) Vfrom_mono1 Vfrom_mono2 dual_order.trans sup.absorb_iff2)
 
 lemma Transset_Vfrom: "Transset(A) \<Longrightarrow> Transset(Vfrom A i)"
 proof (induction i rule: eps_induct)
   case (step i)
   then show ?case
     by (metis Transset_SUP Transset_VPow Transset_sup Vfrom)
 qed
 
 lemma Transset_Vset [simp]: "Transset(Vset i)"
   by (simp add: Transset_Vfrom)
 
 lemma Vfrom_sup: "Vfrom a (i \<squnion> j) = Vfrom a i \<squnion> Vfrom a j"
 proof (rule order_antisym)
   show "Vfrom a (i \<squnion> j) \<le> Vfrom a i \<squnion> Vfrom a j"
     by (simp add: Vfrom [of a "i \<squnion> j"] Vfrom [of a i] Vfrom [of a j] Sup_Un_distrib image_Un sup.assoc sup.left_commute)
   show "Vfrom a i \<squnion> Vfrom a j \<le> Vfrom a (i \<squnion> j)"
     by (metis Vfrom_mono2 le_supI sup_commute)
 qed
 
 lemma Vfrom_succ_Ord:
   assumes "Ord i" shows "Vfrom a (succ i) = a \<squnion> VPow(Vfrom a i)"
 proof (cases "i = 0")
   case True
   then show ?thesis
     by (simp add: Vfrom [of _ "succ 0"])
 next
   case False
   have *: "(SUP x\<in>elts i. VPow (Vfrom a x)) \<le> VPow (Vfrom a i)"
   proof (rule cSup_least)
     show "(\<lambda>x. VPow (Vfrom a x)) ` elts i \<noteq> {}"
       using False by auto
     show "x \<le> VPow (Vfrom a i)" if "x \<in> (\<lambda>x. VPow (Vfrom a x)) ` elts i" for x
       using that
       by clarsimp (meson Ord_in_Ord Ord_linear_le Vfrom_mono assms mem_not_refl order_refl vsubsetD)
   qed
   show ?thesis
   proof (rule Vfrom [THEN trans])
     show "a \<squnion> (SUP j\<in>elts (succ i). VPow (Vfrom a j)) = a \<squnion> VPow (Vfrom a i)"
       using assms
       by (intro sup_mono order_antisym) (auto simp: Sup_V_insert *)
   qed
 qed
 
 lemma Vset_succ: "Ord i \<Longrightarrow> Vset(succ(i)) = VPow(Vset(i))"
   by (simp add: Vfrom_succ_Ord)
 
 lemma Vfrom_Sup:
   assumes "X \<noteq> {}" "small X"
   shows "Vfrom a (Sup X) = (SUP y\<in>X. Vfrom a y)"
 proof (rule order_antisym)
   have "Vfrom a (\<Squnion> X) = a \<squnion> (SUP j\<in>elts (\<Squnion> X). VPow (Vfrom a j))"
     by (metis Vfrom)
   also have "\<dots> \<le> \<Squnion> (Vfrom a ` X)"
   proof -
     have "a \<le> \<Squnion> (Vfrom a ` X)"
       by (metis Vfrom all_not_in_conv assms bdd_above_iff_small cSUP_upper2 replacement sup_ge1)
     moreover have "(SUP j\<in>elts (\<Squnion> X). VPow (Vfrom a j)) \<le> \<Squnion> (Vfrom a ` X)"
     proof -
       have "VPow (Vfrom a x) \<le> \<Squnion> (Vfrom a ` X)"
         if "y \<in> X" "x \<in> elts y" for x y
       proof -
         have "VPow (Vfrom a x) \<le> Vfrom a y"
           by (metis Vfrom bdd_above_iff_small cSUP_upper2 le_supI2 order_refl replacement small_elts that(2))
         also have "\<dots> \<le> \<Squnion> (Vfrom a ` X)"
           using assms that by (force intro: cSUP_upper)
         finally show ?thesis .
       qed
       then show ?thesis
         by (simp add: SUP_le_iff \<open>small X\<close>)
     qed
     ultimately show ?thesis
       by auto
   qed
   finally show "Vfrom a (\<Squnion> X) \<le> \<Squnion> (Vfrom a ` X)" .
   have "\<And>x. x \<in> X \<Longrightarrow>
          a \<squnion> (SUP j\<in>elts x. VPow (Vfrom a j))
          \<le> a \<squnion> (SUP j\<in>elts (\<Squnion> X). VPow (Vfrom a j))"
     using cSUP_subset_mono \<open>small X\<close> by auto
   then show "\<Squnion> (Vfrom a ` X) \<le> Vfrom a (\<Squnion> X)"
     by (metis Vfrom assms(1) cSUP_least)
 qed
 
 lemma Limit_Vfrom_eq:
     "Limit(i) \<Longrightarrow> Vfrom a i = (SUP y \<in> elts i. Vfrom a y)"
   by (metis Limit_def Limit_eq_Sup_self Vfrom_Sup ex_in_conv small_elts)
 
 end