Theory ZFC_in_HOL.ZFC_Cardinals

section ‹Cartesian products, Disjoint Sums, Ranks, Cardinals›

theory ZFC_Cardinals
  imports ZFC_in_HOL

begin

declare [[coercion_enabled]]
declare [[coercion "ord_of_nat :: nat ⇒ V"]]

subsection ‹Ordered Pairs›

lemma singleton_eq_iff [iff]: "set {a} = set {b} ⟷ a=b"
  by simp

lemma doubleton_eq_iff: "set {a,b} = set {c,d} ⟷ (a=c ∧ b=d) ∨ (a=d ∧ b=c)"
  by (simp add: Set.doubleton_eq_iff)

definition vpair :: "V ⇒ V ⇒ V"
  where "vpair a b = set {set {a},set {a,b}}"

definition vfst :: "V ⇒ V"
  where "vfst p ≡ THE x. ∃y. p = vpair x y"

definition vsnd :: "V ⇒ V"
  where "vsnd p ≡ THE y. ∃x. p = vpair x y"

definition vsplit :: "[[V, V] ⇒ 'a, V] ⇒ 'a::{}"  ― ‹for pattern-matching›
  where "vsplit c ≡ λp. c (vfst p) (vsnd p)"

nonterminal Vs
syntax (ASCII)
  "_Tuple"    :: "[V, Vs] ⇒ V"              (‹<(_,/ _)>›)
  "_hpattern" :: "[pttrn, patterns] ⇒ pttrn"   (‹<_,/ _>›)
syntax
  ""          :: "V ⇒ Vs"                    (‹_›)
  "_Enum"     :: "[V, Vs] ⇒ Vs"             (‹_,/ _›)
  "_Tuple"    :: "[V, Vs] ⇒ V"              (‹⟨(_,/ _)⟩›)
  "_hpattern" :: "[pttrn, patterns] ⇒ pttrn"   (‹⟨_,/ _⟩›)
syntax_consts
  "_Enum" "_Tuple" ⇌ vpair and
  "_hpattern" ⇌ vsplit
translations
  "<x, y, z>"    ⇌ "<x, <y, z>>"
  "<x, y>"       ⇌ "CONST vpair x y"
  "<x, y, z>"    ⇌ "<x, <y, z>>"
  "λ<x,y,zs>. b" ⇌ "CONST vsplit(λx <y,zs>. b)"
  "λ<x,y>. b"    ⇌ "CONST vsplit(λ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' ⟷ a=a' ∧ 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 ⟨a,b⟩ = a"
  by (simp add: vfst_def)

lemma vsnd_conv [simp]: "vsnd ⟨a,b⟩ = b"
  by (simp add: vsnd_def)

lemma vsplit [simp]: "vsplit c ⟨a,b⟩ = c a b"
  by (simp add: vsplit_def)

lemma vpair_neq_fst: "⟨a,b⟩ ≠ a"
  by (metis elts_of_set insertI1 mem_not_sym small_upair vpair_def')

lemma vpair_neq_snd: "⟨a,b⟩ ≠ b"
  by (metis elts_of_set insertI1 mem_not_sym small_upair subsetD subset_insertI vpair_def')

lemma vpair_nonzero [simp]: "⟨x,y⟩ ≠ 0"
  by (metis elts_0 elts_of_set empty_not_insert small_upair vpair_def)

lemma zero_notin_vpair: "0 ∉ elts ⟨x,y⟩"
  by (auto simp: vpair_def)

lemma inj_on_vpair [simp]: "inj_on (λ(x, y). ⟨x, y⟩) A"
  by (auto simp: inj_on_def)


subsection ‹Generalized Cartesian product›

definition VSigma :: "V ⇒ (V ⇒ V) ⇒ V"
  where "VSigma A B ≡ set(⋃x ∈ elts A. ⋃y ∈ elts (B x). {⟨x,y⟩})"

abbreviation vtimes where "vtimes A B ≡ VSigma A (λx. B)"

definition pairs :: "V ⇒ (V * V)set"
  where "pairs r ≡ {(x,y). ⟨x,y⟩ ∈ elts r} "

lemma pairs_iff_elts: "(x,y) ∈ pairs z ⟷ ⟨x,y⟩ ∈ elts z"
  by (simp add: pairs_def)

lemma VSigma_iff [simp]: "⟨a,b⟩ ∈ elts (VSigma A B) ⟷ a ∈ elts A ∧ b ∈ elts (B a)"
  by (auto simp: VSigma_def UNION_singleton_eq_range)

lemma VSigmaI [intro!]: "⟦ a ∈ elts A;  b ∈ elts (B a)⟧  ⟹ ⟨a,b⟩ ∈ elts (VSigma A B)"
  by simp

lemmas VSigmaD1 = VSigma_iff [THEN iffD1, THEN conjunct1]
lemmas VSigmaD2 = VSigma_iff [THEN iffD1, THEN conjunct2]

text ‹The general elimination rule›
lemma VSigmaE [elim!]:
  assumes "c ∈ elts (VSigma A B)"
  obtains x y where "x ∈ elts A" "y ∈ elts (B x)" "c=⟨x,y⟩"
  using assms by (auto simp: VSigma_def split: if_split_asm)

lemma VSigmaE2 [elim!]:
  assumes "⟨a,b⟩ ∈ elts (VSigma A B)" obtains "a ∈ elts A" and "b ∈ elts (B a)"
  using assms  by auto

lemma VSigma_empty1 [simp]: "VSigma 0 B = 0"
  by auto

lemma times_iff [simp]: "⟨a,b⟩ ∈ elts (vtimes A B) ⟷ a ∈ elts A ∧ b ∈ elts B"
  by simp

lemma timesI [intro!]: "⟦a ∈ elts A;  b ∈ elts B⟧  ⟹ ⟨a,b⟩ ∈ 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 ⟷ A=0 ∨ (∀x ∈ elts A. B x = 0)"
  by (metis VSigmaE VSigmaI elts_0 empty_iff trad_foundation)

lemma elts_VSigma: "elts (VSigma A B) = (λ(x,y). vpair x y) ` Sigma (elts A) (λx. elts (B x))"
  by auto
    
lemma small_Sigma [simp]:
  assumes A: "small A" and B: "⋀x. x ∈ A ⟹ small (B x)"
  shows "small (Sigma A B)"
proof -
  obtain a where "elts a ≈ A" 
    by (meson assms small_eqpoll)
  then obtain f where f: "bij_betw f (elts a) A"
    using eqpoll_def by blast
  have "∃y. elts y ≈ B x" if "x ∈ A" for x
    using B small_eqpoll that by blast
  then obtain g where g: "⋀x. x ∈ A ⟹ elts (g x) ≈ B x"
    by metis 
  with f have "elts (VSigma a (g ∘ f)) ≈ Sigma A B"
    by (simp add: elts_VSigma Sigma_eqpoll_cong bij_betwE)
  then show ?thesis
    using small_eqpoll by blast
qed

lemma small_Times [simp]:
  assumes "small A" "small B"  shows "small (A × B)"
  by (simp add: assms)

lemma small_Times_iff: "small (A × B) ⟷ small A ∧ small B ∨ A={} ∨ B={}"  (is "_ = ?rhs")
proof
  assume *: "small (A × B)"
  { have "small A ∧ small B" if "x ∈ A" "y ∈ B" for x y
    proof -
      have "A ⊆ fst ` (A × B)" "B ⊆ snd ` (A × B)"
        using that by auto
      with that show ?thesis
        by (metis * replacement smaller_than_small)
    qed    }
  then show ?rhs
    by (metis equals0I)
next
  assume ?rhs
  then show "small (A × B)"
    by auto
qed

subsection ‹Disjoint Sum›

definition vsum :: "V ⇒ V ⇒ V" (infixl ‹⨄› 65) where
 "A ⨄ B ≡ (VSigma (set {0}) (λx. A)) ⊔ (VSigma (set {1}) (λx. B))"

definition Inl :: "V⇒V" where
     "Inl a ≡ ⟨0,a⟩"

definition Inr :: "V⇒V" where
     "Inr b ≡ ⟨1,b⟩"

lemmas sum_defs = vsum_def Inl_def Inr_def

lemma Inl_nonzero [simp]:"Inl x ≠ 0"
  by (metis Inl_def vpair_nonzero)

lemma Inr_nonzero [simp]:"Inr x ≠ 0"
  by (metis Inr_def vpair_nonzero)

subsubsection‹Equivalences for the injections and an elimination rule›

lemma Inl_in_sum_iff [iff]: "Inl a ∈ elts (A ⨄ B) ⟷ a ∈ elts A"
  by (auto simp: sum_defs)

lemma Inr_in_sum_iff [iff]: "Inr b ∈ elts (A ⨄ B) ⟷ b ∈ elts B"
  by (auto simp: sum_defs)

lemma sumE [elim!]:
  assumes u: "u ∈ elts (A ⨄ B)"
  obtains x where "x ∈ elts A" "u=Inl x" | y where "y ∈ elts B" "u=Inr y" using u
  by (auto simp: sum_defs)

subsubsection ‹Injection and freeness equivalences, for rewriting›

lemma Inl_iff [iff]: "Inl a=Inl b ⟷ a=b"
  by (simp add: sum_defs)

lemma Inr_iff [iff]: "Inr a=Inr b ⟷ 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 ⟷ False"
  by (simp add: sum_defs)

lemma Inr_Inl_iff [iff]: "Inr b=Inl a ⟷ False"
  by (simp add: sum_defs)

lemma sum_empty [simp]: "0 ⨄ 0 = 0"
  by auto

lemma elts_vsum: "elts (a ⨄ b) = Inl ` (elts a) ∪ Inr ` (elts b)"
  by auto

lemma sum_iff: "u ∈ elts (A ⨄ B) ⟷ (∃x. x ∈ elts A ∧ u=Inl x) ∨ (∃y. y ∈ elts B ∧ u=Inr y)"
  by blast

lemma sum_subset_iff: "A⨄B ≤ C⨄D ⟷ A≤C ∧ B≤D"
  by (auto simp: less_eq_V_def)

lemma sum_equal_iff:
  fixes A :: V shows "A⨄B = C⨄D ⟷ A=C ∧ B=D"
  by (simp add: eq_iff sum_subset_iff)

definition is_sum :: "V ⇒ bool"
  where "is_sum z = (∃x. z = Inl x ∨ z = Inr x)"

definition sum_case  :: "(V ⇒ 'a) ⇒ (V ⇒ 'a) ⇒ V ⇒ 'a"
  where
  "sum_case f g a ≡
    THE z. (∀x. a = Inl x ⟶ z = f x) ∧ (∀y. a = Inr y ⟶ z = g y) ∧ (¬ is_sum a ⟶ 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]: "¬ is_sum a ⟹ sum_case f g a = undefined"
  by (simp add: sum_case_def is_sum_def)

lemma is_sum_cases: "(∃x. z = Inl x ∨ z = Inr x) ∨ ¬ is_sum z"
  by (auto simp: is_sum_def)

lemma sum_case_split:
  "P (sum_case f g a) ⟷ (∀x. a = Inl x ⟶ P(f x)) ∧ (∀y. a = Inr y ⟶ P(g y)) ∧ (¬ is_sum a ⟶ P undefined)"
  by (cases "is_sum a") (auto simp: is_sum_def)

lemma sum_case_split_asm:
  "P (sum_case f g a) ⟷ ¬ ((∃x. a = Inl x ∧ ¬ P(f x)) ∨ (∃y. a = Inr y ∧ ¬ P(g y)) ∨ (¬ is_sum a ∧ ¬ P undefined))"
  by (auto simp: sum_case_split)

subsubsection ‹Applications of disjoint sums and pairs: general union theorems for small sets›

lemma small_Un:
  assumes X: "small X" and Y: "small Y"
  shows "small (X ∪ Y)"
proof -
  obtain x y where "elts x ≈ X" "elts y ≈ Y"
    by (meson assms small_eqpoll)
  then have "X ∪ Y ≲ Inl ` (elts x) ∪ Inr ` (elts y)"
    by (metis (mono_tags, lifting) Inr_Inl_iff Un_lepoll_mono disjnt_iff eqpoll_imp_lepoll eqpoll_sym f_inv_into_f inj_on_Inl inj_on_Inr inj_on_image_lepoll_2)
  then show ?thesis
    by (metis lepoll_iff replacement small_elts small_sup_iff smaller_than_small)
qed

lemma small_UN [simp,intro]:
  assumes A: "small A" and B: "⋀x. x ∈ A ⟹ small (B x)"
  shows "small (⋃x∈A. B x)"
proof -
  obtain a where "elts a ≈ A" 
    by (meson assms small_eqpoll)
  then obtain f where f: "bij_betw f (elts a) A"
    using eqpoll_def by blast
  have "∃y. elts y ≈ B x" if "x ∈ A" for x
    using B small_eqpoll that by blast
  then obtain g where g: "⋀x. x ∈ A ⟹ elts (g x) ≈ B x" 
    by metis
  have sm: "small (Sigma (elts a) (elts ∘ g ∘ f))"
    by simp
  have "(⋃x∈A. B x) ≲ Sigma A B"
    by (metis image_lepoll snd_image_Sigma)
  also have "...  ≲ Sigma (elts a) (elts ∘ g ∘ f)"
    by (smt (verit) Sigma_eqpoll_cong bij_betw_iff_bijections comp_apply eqpoll_imp_lepoll eqpoll_sym f g)
  finally show ?thesis
    using lepoll_small sm by blast
qed

lemma small_Union [simp,intro]:
  assumes "𝒜 ⊆ Collect small" "small 𝒜"
  shows "small (⋃ 𝒜)"
  using small_UN [of 𝒜 "λx. x"] assms by (simp add: subset_iff)

subsection‹Generalised function space and lambda›

definition VLambda :: "V ⇒ (V ⇒ V) ⇒ V"
  where "VLambda A b ≡ set ((λx. ⟨x,b x⟩) ` elts A)"

definition app :: "[V,V] ⇒ V"
  where "app f x ≡ THE y. ⟨x,y⟩ ∈ elts f"

lemma beta [simp]:
  assumes "x ∈ elts A"
  shows "app (VLambda A b) x = b x"
  using assms by (auto simp: VLambda_def app_def)

definition VPi :: "V ⇒ (V ⇒ V) ⇒ V"
  where "VPi A B ≡ set {f ∈ elts (VPow(VSigma A B)). elts A ≤ Domain (pairs f) ∧ single_valued (pairs f)}"

lemma VPi_I:
  assumes "⋀x. x ∈ elts A ⟹ b x ∈ elts (B x)"
  shows "VLambda A b ∈ elts (VPi A B)"
  proof (clarsimp simp: VPi_def, intro conjI impI)
  show "VLambda A b ≤ VSigma A B"
    by (auto simp: assms VLambda_def split: if_split_asm)
  show "elts A ⊆ 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 ≤ VSigma A B ∧ elts A ⊆ Domain (pairs f) ∧ single_valued (pairs f)}"
    by (metis (mono_tags, lifting) down VPow_iff mem_Collect_eq subsetI)
qed

lemma apply_pair:
  assumes f: "f ∈ elts (VPi A B)" and x: "x ∈ elts A"
  shows "⟨x, app f x⟩ ∈ elts f"
proof -
  have "x ∈ 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: "⟨x,y⟩ ∈ elts f"
    using pairs_iff_elts by auto
  show ?thesis
    unfolding app_def
  proof (rule theI)
    show "⟨x, y⟩ ∈ elts f"
      by (rule y)
    show "z = y" if "⟨x, z⟩ ∈ 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 ∈ elts (VPi A B)" and x: "x ∈ elts A"
  shows "app f x ∈ elts (B x)"
proof -
  have "f ≤ 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 ∈ elts (VPi A B)" and p: "p ∈ elts f"
  obtains x where "x ∈ elts A" "p = ⟨x, app f x⟩"
proof -
  have "f ≤ 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 = ⟨x,y⟩" "x ∈ 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 ‹p = ⟨x, y⟩› ‹x ∈ elts A› that by blast
qed

lemma fun_ext:
  assumes "f ∈ elts (VPi A B)" "g ∈ elts (VPi A B)" "⋀x. x ∈ elts A ⟹ app f x = app g x"
  shows "f = g"
  by (metis VPi_memberD V_equalityI apply_pair assms)

lemma eta[simp]:
  assumes "f ∈ elts (VPi A B)"
  shows "VLambda A ((app)f) = f"
  proof (rule fun_ext [OF _ assms])
  show "VLambda A (app f) ∈ 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 ⟹ A = B"
  by (metis ZFC_in_HOL.ext fst_pairs_VLambda)

lemma VLambda_eq_D2: "⟦VLambda A f = VLambda A g; x ∈ elts A⟧ ⟹ f x = g x"
  by (metis beta)


subsection‹Transitive closure of a set›

definition TC :: "V⇒V"
  where "TC ≡ transrec (λf x. x ⊔ ⨆ (f ` elts x))"

lemma TC: "TC a = a ⊔ ⨆ (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 ≤ 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 ∈ elts (TC x)" if "v ∈ elts u" "u ∈ elts x" for u v
    using that unfolding TC [of x]
    using arg_subset_TC by fastforce
  have 2: "v ∈ elts (TC x)" if "v ∈ elts u" "∃x∈elts x. u ∈ 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: "⟦Transset x;  a≤x⟧ ⟹ TC a ≤ 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 "⨆ (TC ` elts y) ≤ x"
    proof (rule cSup_least)
      show "TC ` elts y ≠ {}"
        using False by auto
      show "z ≤ x" if "z ∈ 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 ‹⊏› 50)
  where "x ⊏ y ≡ x ∈ elts (TC y)"

definition le_TC (infix ‹⊑› 50)
  where "x ⊑ y ≡ x ⊏ y ∨ x=y"

lemma less_TC_imp_not_le: "x ⊏ a ⟹ ¬ a ≤ 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]: "¬ (x ⊏ 0)"
  using less_TC_imp_not_le by blast

lemma less_TC_iff: "x ⊏ y ⟷ (∃z ∈ elts y. x ⊑ z)"
  by (auto simp: less_TC_def le_TC_def TC [of y])

lemma nonzero_less_TC: "x ≠ 0 ⟹ 0 ⊏ x"
  by (metis eps_induct le_TC_def less_TC_iff trad_foundation)

lemma less_irrefl_TC [simp]: "¬ x ⊏ x"
  using less_TC_imp_not_le by blast

lemma less_asym_TC: "⟦x ⊏ y; y ⊏ x⟧ ⟹ 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: "⟦x ⊑ y; y ⊑ x⟧ ⟹ x = y"
  using le_TC_def less_asym_TC by auto

lemma less_le_TC: "x ⊏ y ⟷ x ⊑ y ∧ x ≠ y"
  using le_TC_def less_asym_TC by blast

lemma less_imp_le_TC [iff]: "x ⊏ y ⟹ x ⊑ y"
  by (simp add: le_TC_def)

lemma le_TC_refl [iff]: "x ⊑ x"
  by (simp add: le_TC_def)

lemma le_TC_trans [trans]: "⟦x ⊑ y; y ⊑ z⟧ ⟹ x ⊑ z"
  by (smt (verit, best) TC_least Transset_TC Transset_def le_TC_def less_TC_def vsubsetD)

context order
begin

lemma nless_le_TC: "(¬ a ⊏ b) ⟷ (¬ a ⊑ b) ∨ a = b"
  using le_TC_def less_asym_TC by blast

lemma eq_refl_TC: "x = y ⟹ x ⊑ y"
  by simp

local_setup ‹
  HOL_Order_Tac.declare_order {
    ops = {eq = @{term ‹(=) :: V ⇒ V ⇒ bool›}, le = @{term ‹(⊑)›}, lt = @{term ‹(⊏)›}},
    thms = {trans = @{thm le_TC_trans}, refl = @{thm le_TC_refl}, eqD1 = @{thm eq_refl_TC},
            eqD2 = @{thm eq_refl_TC[OF sym]}, antisym = @{thm le_antisym_TC}, contr = @{thm notE}},
    conv_thms = {less_le = @{thm eq_reflection[OF less_le_TC]},
                 nless_le = @{thm eq_reflection[OF nless_le_TC]}}
  }
›

end


lemma less_TC_trans [trans]: "⟦x ⊏ y; y ⊏ z⟧ ⟹ x ⊏ z" 
  and less_le_TC_trans: "⟦x ⊏ y; y ⊑ z⟧ ⟹ x ⊏ z" 
  and le_less_TC_trans [trans]: "⟦x ⊑ y; y ⊏ z⟧ ⟹ x ⊏ z"
  by simp_all

lemma TC_sup_distrib: "TC (x ⊔ y) = TC x ⊔ TC y"
  by (simp add: Sup_Un_distrib TC [of "x ⊔ y"] TC [of x] TC [of y] image_Un sup.assoc sup_left_commute)

lemma TC_Sup_distrib:
  assumes "small X" shows "TC (⨆X) = ⨆(TC ` X)"
proof -
  have "⨆X ≤ ⨆ (TC ` X)"
    using arg_subset_TC by fastforce
  moreover have "⨆ (⋃x∈X. TC ` elts x) ≤ ⨆ (TC ` X)"
    using assms 
    by clarsimp (meson TC_least Transset_TC Transset_def arg_subset_TC replacement vsubsetD)
  ultimately
  have "⨆ X ⊔ ⨆ (⋃x∈X. TC ` elts x) ≤ ⨆ (TC ` X)"
    by simp
  moreover have "⨆ (TC ` X) ≤ ⨆ X ⊔ ⨆ (⋃x∈X. TC ` elts x)"
  proof (clarsimp simp add: Sup_le_iff assms)
    show "∃x∈X. y ∈ elts x"
      if "x ∈ X" "y ∈ elts (TC x)" "∀x∈X. ∀u∈elts x. y ∉ elts (TC u)" for x y
      using that by (auto simp: TC [of x])
  qed
  ultimately show ?thesis
    using Sup_Un_distrib TC [of "⨆X"] image_Union assms
    by (simp add: image_Union inf_sup_aci(5) sup.absorb_iff2)
qed

lemma TC': "TC x = x ⊔ TC (⨆ (elts x))"
  by (simp add: TC [of x] TC_Sup_distrib)

lemma TC_eq_0_iff [simp]: "TC x = 0 ⟷ x=0"
  using arg_subset_TC by fastforce

text‹A distinctive induction principle›
lemma TC_induct_down_lemma:
  assumes ab: "a ⊏ b" and base: "b ≤ d"
      and step: "⋀y z. ⟦y ⊏ b; y ∈ elts d; z ∈ elts y⟧ ⟹ z ∈ elts d"
    shows "a ∈ elts d"
proof -
  have "Transset (TC b ⊓ 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 ≤ TC b ⊓ 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 ⊏ b"
    and "⋀y. y ∈ elts b ⟹ P y"
    and "⋀y z. ⟦y ⊏ b; P y; z ∈ elts y⟧ ⟹ 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‹Rank of a set›

definition rank :: "V⇒V"
  where "rank a ≡ transrec (λf x. set (⋃y∈elts x. elts (succ(f y)))) a"

lemma rank: "rank a = set(⋃y ∈ elts a. elts (succ(rank y)))"
  by (subst rank_def [THEN def_transrec], simp)

lemma rank_Sup: "rank a = ⨆((λ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 ⟹ rank i = i"
  by (induction rule: Ord_induct) (metis (no_types, lifting) Ord_equality SUP_cong rank_Sup)

lemma Ord_iff_rank: "Ord x ⟷ rank x = x"
  using Ord_rank [of x] rank_of_Ord by fastforce

lemma rank_lt: "a ∈ elts b ⟹ rank a < rank b"
  by (metis Ord_linear2 Ord_rank ZFC_in_HOL.SUP_le_iff rank_Sup replacement small_elts succ_le_iff order.irrefl)

lemma rank_0 [simp]: "rank 0 = 0"
  using transrec Ord_0 rank_def rank_of_Ord by presburger

lemma rank_succ [simp]: "rank(succ x) = succ(rank x)"
proof (rule order_antisym)
  show "rank (succ x) ≤ succ (rank x)"
    by (metis (no_types, lifting) Sup_insert elts_of_set elts_succ image_insert rank small_UN small_elts subset_insertI sup.orderE vsubsetI)
  show "succ (rank x) ≤ 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 ≤ b ⟹ rank a ≤ rank b"
  using rank [of a] rank [of b] small_UN by force

lemma VsetI: "rank b ⊏ i ⟹ b ∈ elts (Vset i)"
proof (induction i arbitrary: b rule: eps_induct)
  case (step x)
  then consider "rank b ∈ elts x" | "(∃y∈elts x. rank b ∈ elts (TC y))"
    using le_TC_def less_TC_def less_TC_iff by fastforce
  then have "∃y∈elts x. b ≤ Vset y"
  proof cases
    case 1
    then have "b ≤ 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: "⟦Ord i; rank b < i⟧ ⟹ b ∈ 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 ≤ Vset(rank a)"
  by (simp add: Ord_VsetI rank_lt vsubsetI)

lemma two_in_Vset:
  obtains α where  "x ∈ elts (Vset α)" "y ∈ elts (Vset α)"
  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 ⟷ 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 ≡ set (⋃(elts ` (rank ` A)))"
  have "Ord i"
    unfolding i_def using Ord_Union Ord_rank assms imageE by blast
  have *: "Vset (rank x) ≤ (Vset i)" if "x ∈ 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 ⊆ 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(⨆ A) = ⨆ (rank ` A)"
proof (rule order_antisym)
  have "elts (⨆y∈elts (⨆ A). succ (rank y)) ⊆ elts (⨆ (rank ` A))"
    by clarsimp (meson Ord_mem_iff_lt Ord_rank less_V_def rank_lt vsubsetD)
  then show "rank (⨆ A) ≤ ⨆ (rank ` A)"
    by (metis less_eq_V_def rank_Sup)
  show "⨆ (rank ` A) ≤ rank (⨆ A)"
  proof (cases "small A")
    case True
    then show ?thesis
      by (simp add: ZFC_in_HOL.SUP_le_iff ZFC_in_HOL.Sup_upper rank_mono)
  next
    case False
    then have "¬ 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 ∈ elts a}"
proof -
  have "{x. rank x ∈ elts a} ⊆ {x. rank x ⊏ a}"
    using less_TC_iff by auto
  also have "… ⊆ elts (Vset a)"
    using VsetI by blast
  finally show ?thesis
    using down by simp
qed

lemma small_bounded_rank_le:  "small {x. rank x ≤ a}"
  using small_bounded_rank [of "VPow a"] VPow_iff [of _ a]  by simp

lemma TC_rank_lt: "a ⊏ b ⟹ 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
    using 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 ⊏ y ⟹ rank x ∈ elts (rank y)"
  by (simp add: Ord_mem_iff_lt TC_rank_lt)

lemma wf_TC_less: "wf {(x,y). x ⊏ y}"
  proof (rule wf_subset [OF wf_inv_image [OF foundation, of rank]])
    show "{(x, y). x ⊏ y} ⊆ inv_image {(x, y). x ∈ 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 ⊑ a" "⋀y. y ⊏ x ⟹ ¬ P y"
  using wfE_min' [OF wf_TC_less, of "{x. P x ∧ x ⊑ 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) ≤ Vfrom A x"
  proof (induction x rule: eps_induct)
    case (step x)
    have "(⨆j∈elts (rank x). VPow (Vfrom A j)) ≤ (⨆j∈elts x. VPow (Vfrom A j))"
      apply (rule Sup_least)
      apply (clarsimp simp add: rank [of x])
      by (meson Ord_in_Ord Ord_rank OrdmemD Vfrom_mono order.trans less_imp_le order.refl step)
    then show ?case
      by (simp add: Vfrom [of _ x] Vfrom [of _ "rank(x)"] sup.coboundedI2)
qed
  show "Vfrom A x ≤ Vfrom A (rank x)"
  proof (induction x rule: eps_induct)
    case (step x)
    have "(⨆j∈elts x. VPow (Vfrom A j)) ≤ (⨆j∈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 ⊔ VPow(Vfrom A i)"
  by (metis Ord_rank Vfrom_rank_eq Vfrom_succ_Ord rank_succ)

lemma Vset_succ_TC:
  assumes "x ∈ elts (Vset (ZFC_in_HOL.succ k))" "u ⊏ x"
  shows "u ∈ elts (Vset k)"
  using assms
  using TC_least Transset_Vfrom Vfrom_succ less_TC_def by auto

subsection‹Cardinal Numbers›

text‹We extend the membership relation to a wellordering›
definition VWO :: "(V × V) set"
  where "VWO ≡ @r. {(x,y). x ∈ elts y} ⊆ r ∧ Well_order r ∧ Field r = UNIV"

lemma VWO: "{(x,y). x ∈ elts y} ⊆ VWO ∧ Well_order VWO ∧ 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 ∧ 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 ‹Transitive Closure and VWO›

lemma mem_imp_VWO: "x ∈ elts y ⟹ (x,y) ∈ VWO"
  using VWO by blast

lemma less_TC_imp_VWO: "x ⊏ y ⟹ (x,y) ∈ VWO"
  unfolding less_TC_def
proof (induction y arbitrary: x rule: eps_induct)
  case (step y' u)
  then consider "u ∈ elts y'" | v where "v ∈ elts y'" "u ∈ 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 ⊑ y ⟹ (x,y) ∈ VWO"
  by (metis Diff_iff Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO le_TC_def less_TC_imp_VWO)

lemma le_TC_0_iff [simp]: "x ⊑ 0 ⟷ x = 0"
  by (simp add: le_TC_def)

lemma less_TC_succ: " x ⊏ succ β ⟷ x ⊏ β ∨ x = β"
  by (metis elts_succ insert_iff le_TC_def less_TC_iff)

lemma le_TC_succ: "x ⊑ succ β ⟷ x ⊑ β ∨ x = succ β"
  by (simp add: le_TC_def less_TC_succ)

lemma Transset_TC_eq [simp]: "Transset x ⟹ TC x = x"
  by (simp add: TC_least arg_subset_TC eq_iff)

lemma Ord_TC_less_iff: "⟦Ord α; Ord β⟧ ⟹ β ⊏ α ⟷ β < α"
  by (metis Ord_def Ord_mem_iff_lt Transset_TC_eq less_TC_def)

lemma Ord_mem_iff_less_TC: "Ord l ⟹ k ∈ elts l ⟷ k ⊏ l"
  by (simp add: Ord_def less_TC_def)

lemma le_TC_Ord: "⟦β ⊑ α; Ord α⟧ ⟹ Ord β"
  by (metis Ord_def Ord_in_Ord Transset_TC_eq le_TC_def less_TC_def)

lemma Ord_less_TC_mem:
  assumes "Ord α" "β ⊏ α" shows "β ∈ elts α"
  using Ord_def assms less_TC_def by auto

lemma VWO_TC_le: "⟦Ord α; Ord β; (β, α) ∈ VWO⟧ ⟹ β ⊑ α"
proof (induct α arbitrary: β rule: Ord_induct)
  case (step α)
  then show ?case
    by (metis DiffI IdD Linear_order_VWO Linear_order_in_diff_Id Ord_linear Ord_mem_iff_less_TC VWO iso_tuple_UNIV_I le_TC_def mem_imp_VWO)
qed

lemma VWO_iff_Ord_le [simp]: "⟦Ord α; Ord β⟧ ⟹ (β, α) ∈ VWO ⟷ β ≤ α"
  by (metis VWO_TC_le Ord_TC_less_iff le_TC_def le_TC_imp_VWO le_less)

lemma zero_TC_le [iff]: "0 ⊑ y"
  using le_TC_def nonzero_less_TC by auto

lemma succ_le_TC_iff: "Ord j ⟹ succ i ⊑ j ⟷ i ⊏ 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) ∈ VWO ⟷ x=0"
proof
  show "x = 0" if "(x, 0) ∈ 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) ∈ VWO" "(y,x) ∈ VWO" shows "x=y"
  by (metis Diff_iff IdD Linear_order_VWO Linear_order_in_diff_Id UNIV_I VWO assms)

subsubsection ‹Relation VWF›

definition VWF where "VWF ≡ 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 wf_VWF wf_imp_asym)

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) ∈ VWF" "(y,x) ∈ VWF" shows False
  using VWF_def assms wf_VWO wf_not_sym by fastforce

lemma VWF_non_refl [iff]: "(x,x) ∉ VWF"
  by simp

lemma VWF_iff_Ord_less [simp]: "⟦Ord α; Ord β⟧ ⟹ (α,β) ∈ VWF ⟷ α < β"
  by (simp add: VWF_def less_V_def)

lemma mem_imp_VWF: "x ∈ elts y ⟹ (x,y) ∈ VWF"
  using VWF_def mem_imp_VWO by fastforce


subsection‹Order types›

definition ordermap :: "'a set ⇒ ('a × 'a) set ⇒ 'a ⇒ V"
  where "ordermap A r ≡ wfrec r (λf x. set (f ` {y ∈ A. (y,x) ∈ r}))"

definition ordertype :: "'a set ⇒ ('a × 'a) set ⇒ V"
  where "ordertype A r ≡ set (ordermap A r ` A)"

lemma ordermap_type:
    "small A ⟹ ordermap A r ∈ A → elts (ordertype A r)"
  by (simp add: ordertype_def)

lemma ordermap_in_ordertype [intro]: "⟦a ∈ A; small A⟧ ⟹ ordermap A r a ∈ elts (ordertype A r)"
  by (simp add: ordertype_def)

lemma ordermap: "wf r ⟹ ordermap A r a = set (ordermap A r ` {y ∈ A. (y,a) ∈ r})"
  unfolding ordermap_def
  by (auto simp: wfrec_fixpoint adm_wf_def)

lemma wf_Ord_ordermap [iff]: assumes "wf r" "trans r" shows "Ord (ordermap A r x)"
  using ‹wf r›
proof (induction x rule: wf_induct_rule)
  case (less u)
  have "Transset (set (ordermap A r ` {y ∈ A. (y, u) ∈ r}))"
  proof (clarsimp simp add: Transset_def)
    show "x ∈ ordermap A r ` {y ∈ A. (y, u) ∈ r}"
      if "small (ordermap A r ` {y ∈ A. (y, u) ∈ r})"
        and x: "x ∈ elts (ordermap A r y)" and "y ∈ A" "(y, u) ∈ r" for x y
    proof -
      have "ordermap A r y = ZFC_in_HOL.set (ordermap A r ` {a ∈ A. (a, y) ∈ r})"
        using ordermap assms(1) by force
      then have "x ∈ ordermap A r ` {z ∈ A. (z, y) ∈ r}"
        by (metis (no_types, lifting) elts_of_set empty_iff x)
      then have "∃v. v ∈ A ∧ (v, u) ∈ r ∧ x = ordermap A r v"
        using that transD [OF ‹trans r›] by blast
      then show ?thesis
        by blast
    qed
  qed
  moreover have "Ord x"
    if "x ∈ elts (set (ordermap A r ` {y ∈ A. (y, u) ∈ 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 ≤ set (ordermap A r ` A)"
    if "y = ordermap A r x" "x ∈ A" "small (ordermap A r ` A)" for x y
    using that by (auto simp: less_eq_V_def ordermap [OF ‹wf r›, of A x])
  moreover have "z ≤ y" if "y ∈ ordermap A r ` A" "z ∈ elts y" for y z
    by (metis wf_Ord_ordermap OrdmemD assms imageE order.strict_implies_order that)
  ultimately show ?thesis
    unfolding ordertype_def Ord_def Transset_def by simp
qed

lemma Ord_ordertype [simp]: "Ord(ordertype A VWF)"
  using wf_Ord_ordertype by blast

lemma Ord_ordermap [simp]: "Ord (ordermap A VWF x)"
  by blast

lemma ordertype_singleton [simp]:
  assumes "wf r" 
  shows "ordertype {x} r = 1"
proof -
  have †: "{y. y = x ∧ (y, x) ∈ r} = {}"
    using assms by auto
  show ?thesis
    by (auto simp add: ordertype_def assms † ordermap [where a=x])
qed


subsubsection‹@{term ordermap} preserves the orderings in both directions›

lemma ordermap_mono:
  assumes wx: "(w, x) ∈ r" and "wf r" "w ∈ A" "small A"
    shows "ordermap A r w ∈ elts (ordermap A r x)"
proof -
  have "small {a ∈ A. (a, x) ∈ r} ∧ w ∈ A ∧ (w, x) ∈ 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 ∈ elts (ordermap A r x)" "wf r" "total_on A r" "x ∈ A" "y ∈ A" "small A"
  shows "(y, x) ∈ 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) ∈ r" | "(y,x) ∈ r"
    using ‹total_on A r› assms by (meson UNIV_I total_on_def)
  then show ?thesis
    by (meson ordermap_mono assms mem_not_sym)
qed

lemma converse_ordermap_mono_iff:
  assumes "wf r" "total_on A r" "x ∈ A" "y ∈ A" "small A"
  shows "ordermap A r y ∈ elts (ordermap A r x) ⟷ (y, x) ∈ r"
  by (metis assms converse_ordermap_mono ordermap_mono)

lemma ordermap_surj: "elts (ordertype A r) ⊆ 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 ‹small A› elts_of_set replacement)
qed

lemma ordermap_eq_iff [simp]: 
  "⟦x ∈ A; y ∈ A; wf r; total_on A r; small A⟧ ⟹ ordermap A r x = ordermap A r y ⟷ x = y"
  by (metis bij_betw_iff_bijections ordermap_bij)

lemma inv_into_ordermap: "α ∈ elts (ordertype A r) ⟹ inv_into A (ordermap A r) α ∈ A"
  by (meson in_mono inv_into_into ordermap_surj)

lemma ordertype_nat_imp_finite:
  assumes "ordertype A r = ord_of_nat m" "small A" "wf r" "total_on A r"
  shows "finite A"
proof -
  have "A ≈ 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) ≈ A"
  using assms eqpoll_def eqpoll_sym ordermap_bij by blast

lemma ordertype_eqpoll:
  assumes "small A"
  shows "elts (ordertype A VWF) ≈ A"
  using assms wf_ordertype_eqpoll total_VWF wf_VWF
  by (simp add: wf_ordertype_eqpoll total_on_def)

subsection ‹More advanced @{term ordertype} and @{term ordermap} results›

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]: "⟦small X; wf r⟧ ⟹ ordertype X r = 0 ⟷ X = {}"
  by (metis ordertype_def elts_of_set replacement image_is_empty zero_V_def)

lemma ordermap_mono_less:
  assumes "(w, x) ∈ r"
      and "wf r" "trans r"
      and "w ∈ A" "x ∈ 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) ∈ r ∨ w=x"
      and "wf r" "trans r"
      and "w ∈ A" "x ∈ A"
      and "small A"
    shows "ordermap A r w ≤ 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 ≤ ordermap A r x" "wf r" "total r"  "x ∈ A" "small A"
  shows "(y, x) ∈ r ∨ y=x"
  by (meson UNIV_I assms mem_not_refl ordermap_mono total_on_def vsubsetD)

lemma ordertype_mono:
  assumes "X ⊆ Y" and r: "wf r" "trans r" and "small Y"
  shows "ordertype X r ≤ ordertype Y r"
proof -
  have "small X"
    using assms smaller_than_small by fastforce 
  have *: "ordermap X r x ≤ ordermap Y r x" for x
    using ‹wf r›
  proof (induction x rule: wf_induct_rule)
    case (less x)
    have "ordermap X r z < ordermap Y r x" if "z ∈ X" and zx: "(z,x) ∈ r" for z
      using less [OF zx] assms
      by (meson Ord_linear2 OrdmemD wf_Ord_ordermap ordermap_mono in_mono leD that(1) vsubsetD zx)
    then show ?case
      by (auto simp add: ordermap [of _ X x] ‹small X› 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 ‹small Y› elts_of_set replacement)
    then have "ordertype Y r ∉ ordermap X r ` X"
      using "*" ‹X ⊆ Y› by fastforce
    then show ?thesis
      by (metis Ord_linear2 Ord_mem_iff_lt ordertype_def wf_Ord_ordertype ‹small X› elts_of_set replacement r)
  qed
qed

corollary ordertype_VWF_mono:
  assumes "X ⊆ Y" "small Y"
  shows "ordertype X VWF ≤ ordertype Y VWF"
  using assms by (simp add: ordertype_mono)

lemma ordertype_UNION_ge:
  assumes "A ∈ 𝒜" "wf r" "trans r" "𝒜 ⊆ Collect small" "small 𝒜"
  shows "ordertype A r ≤ ordertype (⋃𝒜) r" 
  by (rule ordertype_mono) (use assms in auto)

lemma inv_ordermap_mono_less:
  assumes "(inv_into M (ordermap M r) α, inv_into M (ordermap M r) β) ∈ r" 
    and "small M" and α: "α ∈ elts (ordertype M r)" and β: "β ∈ elts (ordertype M r)"
    and "wf r" "trans r"
  shows "α < β"
proof -
  have "α = ordermap M r (inv_into M (ordermap M r) α)"
    by (metis α f_inv_into_f ordermap_surj subset_eq)
  also have "… < ordermap M r (inv_into M (ordermap M r) β)"
    by (meson α β assms in_mono inv_into_into ordermap_mono_less ordermap_surj)
  also have "… = β"
    by (meson β f_inv_into_f in_mono ordermap_surj)
  finally show ?thesis .
qed

lemma inv_ordermap_mono_eq:
  assumes "inv_into M (ordermap M r) α = inv_into M (ordermap M r) β" 
    and "α ∈ elts (ordertype M r)" "β ∈ elts (ordertype M r)"
  shows "α = β"
  by (metis assms f_inv_into_f ordermap_surj subsetD)

lemma inv_ordermap_VWF_mono_le:
  assumes "inv_into M (ordermap M VWF) α ≤ inv_into M (ordermap M VWF) β" 
    and "M ⊆ ON" "small M" and α: "α ∈ elts (ordertype M VWF)" and β: "β ∈ elts (ordertype M VWF)"
  shows "α ≤ β"
proof -
  have "α = ordermap M VWF (inv_into M (ordermap M VWF) α)"
    by (metis α f_inv_into_f ordermap_surj subset_eq)
  also have "… ≤ ordermap M VWF (inv_into M (ordermap M VWF) β)"
    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 "… = β"
    by (meson β f_inv_into_f in_mono ordermap_surj)
  finally show ?thesis .
qed

lemma inv_ordermap_VWF_mono_iff:
  assumes "M ⊆ ON" "small M" and "α ∈ elts (ordertype M VWF)" and "β ∈ elts (ordertype M VWF)"
  shows "inv_into M (ordermap M VWF) α ≤ inv_into M (ordermap M VWF) β ⟷ α ≤ β"
  by (metis ON_imp_Ord Ord_linear_le assms dual_order.eq_iff inv_into_ordermap inv_ordermap_VWF_mono_le)

lemma inv_ordermap_VWF_strict_mono_iff:
  assumes "M ⊆ ON" "small M" and "α ∈ elts (ordertype M VWF)" and "β ∈ elts (ordertype M VWF)"
  shows "inv_into M (ordermap M VWF) α < inv_into M (ordermap M VWF) β ⟷ α < β"
  by (simp add: assms inv_ordermap_VWF_mono_iff less_le_not_le)

lemma strict_mono_on_ordertype:
  assumes "M ⊆ ON" "small M"
  obtains f where "f ∈ elts (ordertype M VWF) → M" "strict_mono_on (elts (ordertype M VWF)) f"
proof 
  show "inv_into M (ordermap M VWF) ∈ elts (ordertype M VWF) → M"
    by (meson Pi_I' in_mono inv_into_into ordermap_surj)
  show "strict_mono_on (elts (ordertype M VWF)) (inv_into M (ordermap M VWF))"
  proof (clarsimp simp: strict_mono_on_def)
    fix x y
    assume "x ∈ elts (ordertype M VWF)" "y ∈ elts (ordertype M VWF)" "x < y"
    then show "inv_into M (ordermap M VWF) x < inv_into M (ordermap M VWF) y"
      using assms by (meson ON_imp_Ord Ord_linear2 inv_into_into inv_ordermap_VWF_mono_le leD ordermap_surj subsetD)
  qed
qed

lemma ordermap_inc_eq:
  assumes "x ∈ A" "small A"
    and π: "⋀x y. ⟦x∈A; y∈A; (x,y) ∈ r⟧ ⟹ (π x, π y) ∈ s"
    and r: "wf r" "total_on A r" and "wf s" 
  shows "ordermap (π ` A) s (π x) = ordermap A r x"
  using ‹wf r› ‹x ∈ A›
proof (induction x rule: wf_induct_rule)
  case (less x)
  then have 1: "{y ∈ A. (y, x) ∈ r} = A ∩ {y. (y, x) ∈ r}"
    using r by auto
  have 2: "{y ∈ π ` A. (y, π x) ∈ s} = π ` A ∩ {y. (y, π x) ∈ s}"
    by auto
  have invπ: "⋀x y. ⟦x∈A; y∈A; (π x, π y) ∈ s⟧ ⟹ (x, y) ∈ r"
    by (metis π ‹wf s› ‹total_on A r› total_on_def wf_not_sym)
  have eq: "f ` (π ` A ∩ {y. (y, π x) ∈ s}) = (f ∘ π) ` (A ∩ {y. (y, x) ∈ r})" for f :: "'b ⇒ V"
    using less by (auto simp: image_subset_iff invπ π)
  show ?case
    using less
    by (simp add: ordermap [OF ‹wf r›, of _ x] ordermap [OF ‹wf s›, of _ "π x"] 1 2 eq)
qed

lemma ordertype_inc_eq:
  assumes "small A"
    and π: "⋀x y. ⟦x∈A; y∈A; (x,y) ∈ r⟧ ⟹ (π x, π y) ∈ s"
    and r: "wf r" "total_on A r" and "wf s" 
  shows "ordertype (π ` A) s = ordertype A r"
proof -
  have "ordermap (π ` A) s (π x) = ordermap A r x" if "x ∈ 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 π: "⋀x y. ⟦x∈A; y∈A; (x,y) ∈ r⟧ ⟹ (π x, π y) ∈ s"
    and r: "wf r" "total_on A r" and "wf s" "trans s"
    and "π ` A ⊆ B"
  shows "ordertype A r ≤ ordertype B s"
  by (metis assms ordertype_inc_eq ordertype_mono)

corollary ordertype_VWF_inc_eq:
  assumes "A ⊆ ON" "π ` A ⊆ ON" "small A" and "⋀x y. ⟦x∈A; y∈A; x<y⟧ ⟹ π x < π y"
  shows "ordertype (π ` A) VWF = ordertype A VWF"
proof (rule ordertype_inc_eq)
  show "(π x, π y) ∈ VWF"
    if "x ∈ A" "y ∈ A" "(x, y) ∈ 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 ⊆ 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) ∈ VWF"
    if "x ∈ X" "y ∈ X" "(x, y) ∈ r" for x y
    by (meson that wf_Ord_ordermap VWF_iff_Ord_less assms ordermap_mono_less subsetD)
qed (use assms in auto)
    
lemma ordertype_map_image:
  assumes "B ⊆ 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 "… = ordertype (A - B) VWF"
    using ‹small A› 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 ≤ ordertype B s ⟷
         (∃f ∈ A → B. inj_on f A ∧ (∀x ∈ A. ∀y ∈ A. ((x,y) ∈ r ⟶ (f x, f y) ∈ s)))"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  define f where "f ≡ inv_into B (ordermap B s) ∘ ordermap A r"
  show ?rhs
  proof (intro bexI conjI ballI impI)
    have AB: "elts (ordertype A r) ⊆ 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 ‹small A› r by blast
    have "inv_into B (ordermap B s) (ordermap A r i) ∈ B" if "i ∈ A" for i
      by (meson L ‹small A› inv_into_into ordermap_in_ordertype ordermap_surj subsetD that vsubsetD)
    then show "f ∈ A → 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 ∈ A" "y ∈ 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 ‹small A› inv_into_injective ordermap_in_ordertype subsetD)
      then show "x = y"
        by (metis ‹x ∈ A› ‹y ∈ A› bijA bij_betw_inv_into_left)
    qed
  next
    fix x y
    assume "x ∈ A" "y ∈ A" and "(x, y) ∈ r"
    have ‡: "ordermap A r y ∈ ordermap B s ` B"
      by (meson L ‹y ∈ A› ‹small A› in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
    moreover have †: "⋀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 ‡ by (metis f_inv_into_f)
    moreover have "ordermap A r x ∈ ordermap B s ` B"
      by (meson L ‹x ∈ A› ‹small A› in_mono ordermap_in_ordertype ordermap_surj vsubsetD)
    moreover have "ordermap A r x < ordermap A r y"
      using * r s by (metis (no_types) wf_Ord_ordermap OrdmemD ‹(x, y) ∈ r› ‹x ∈ A› ‹small A› ordermap_mono)
    ultimately show "(f x, f y) ∈ s"
      using † 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∈A → B" "inj_on f A" "∀x∈A. ∀y∈A. (x, y) ∈ r ⟶ (f x, f y) ∈ s"
    by blast
  show ?lhs
    by (rule ordertype_inc_le [where π=f]) (use f assms in auto)
qed

lemma iso_imp_ordertype_eq_ordertype:
  assumes iso: "iso r r' f"
    and "wf r"
    and "Total r"
    and sm: "small (Field r)"
  shows "ordertype (Field r) r = ordertype (Field r') r'"
  by (metis (no_types, lifting) iso_forward iso_wf assms iso_Field ordertype_inc_eq sm)

lemma ordertype_infinite_ge_ω:
  assumes "infinite A" "small A"
  shows "ordertype A VWF ≥ ω"
proof -
  have "inj_on (ordermap A VWF) A"
    by (meson ordermap_bij ‹small A› bij_betw_def total_on_VWF wf_VWF)
  then have "infinite (ordermap A VWF ` A)"
    using ‹infinite A› finite_image_iff by blast
  then show ?thesis
    using Ord_ordertype ‹small A› 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" "(∀x ∈ A. ∀y ∈ A. (f x, f y) ∈ s ⟷ (x,y) ∈ 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 α" and x: "x ∈ elts α" 
  shows "ordermap (elts α) VWF x = x" 
  using Ord_in_Ord [OF assms] x 
proof (induction x rule: Ord_induct)
  case (step x)
  have 1: "{y ∈ elts α. (y, x) ∈ VWF} = elts x" (is "?A = _")
  proof
    show "?A ⊆ elts x"
      using ‹Ord α› by clarify (meson Ord_in_Ord Ord_mem_iff_lt VWF_iff_Ord_less step.hyps)
    show "elts x ⊆ ?A"
      using ‹Ord α› 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 _ _ α] step.prems ‹Ord α› cong: image_cong)
qed

lemma ordertype_eq_Ord [simp]:
  assumes "Ord α" 
  shows "ordertype (elts α) VWF = α"
  using assms ordermap_eq_self [OF assms] by (simp add: ordertype_def)


proposition ordertype_eq_iff:
  assumes α: "Ord α" and r: "wf r" and "small A" "total_on A r" "trans r"
  shows "ordertype A r = α ⟷
         (∃f. bij_betw f A (elts α) ∧ (∀x ∈ A. ∀y ∈ A. f x < f y ⟷ (x,y) ∈ r))"
    (is "?lhs = ?rhs")
proof safe
  assume eq: "α = ordertype A r"
  show "∃f. bij_betw f A (elts (ordertype A r)) ∧ (∀x∈A. ∀y∈A. f x < f y ⟷ ((x, y) ∈ 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 ⟷ (x, y) ∈ r"
      if "x ∈ A" "y ∈ 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 α)" "∀x∈A. ∀y∈A. f x < f y ⟷ (x, y) ∈ r"
  have "ordertype A r = ordertype (elts α) VWF"
  proof (rule ordertype_eqI)
    show "∀x∈A. ∀y∈A. ((f x, f y) ∈ VWF) = ((x, y) ∈ r)"
      by (meson Ord_in_Ord VWF_iff_Ord_less α bij_betwE f)
  qed (use assms f in auto)
  then show ?lhs
    by (simp add: α)
qed

corollary ordertype_VWF_eq_iff:
  assumes "Ord α" "small A"
  shows "ordertype A VWF = α ⟷
         (∃f. bij_betw f A (elts α) ∧ (∀x ∈ A. ∀y ∈ A. f x < f y ⟷ (x,y) ∈ VWF))"
  by (metis UNIV_I assms ordertype_eq_iff total_VWF total_on_def trans_VWF wf_VWF)


lemma ordertype_le_Ord:
  assumes "Ord α" "X ⊆ elts α"
  shows "ordertype X VWF ≤ α"
  by (metis assms ordertype_VWF_mono ordertype_eq_Ord small_elts)

lemma ordertype_inc_le_Ord:
  assumes "small A" "Ord α"
    and π: "⋀x y. ⟦x∈A; y∈A; (x,y) ∈ r⟧ ⟹ π x < π y"
    and "wf r" "total_on A r" 
    and sub: "π ` A ⊆ elts α"
  shows "ordertype A r ≤ α"
proof -
  have "⋀x y. ⟦x∈A; y∈A; (x,y) ∈ r⟧ ⟹ (π x, π y) ∈ VWF"
    by (meson Ord_in_Ord VWF_iff_Ord_less π ‹Ord α› 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 α: "β ≤ α" "ordertype H VWF = α" and "small H" "Ord β"
  obtains G where "G ⊆ H" "ordertype G VWF = β" 
proof (intro exI conjI that)
  let ?f = "ordermap H VWF"
  show ‡: "inv_into H ?f ` elts β ⊆ H"
    unfolding image_subset_iff
    by (metis α inv_into_into ordermap_surj subsetD vsubsetD)
  have "∃f. bij_betw f (inv_into H ?f ` elts β) (elts β) ∧ (∀x∈inv_into H ?f ` elts β. ∀y∈inv_into H ?f ` elts β. (f x < f y) = ((x, y) ∈ VWF))"
  proof (intro exI conjI ballI iffI)
    show "bij_betw ?f (inv_into H ?f ` elts β) (elts β)"
      using ordermap_bij [OF wf_VWF total_on_VWF ‹small H›] α 
      by (metis bij_betw_inv_into_RIGHT bij_betw_subset less_eq_V_def ‡)
  next
    fix x y
    assume x: "x ∈ inv_into H ?f ` elts β"
        and y: "y ∈ inv_into H ?f ` elts β"
    show "?f x < ?f y" if "(x,y) ∈ VWF"
      using that ‡ ‹small H› in_mono ordermap_mono_less x y by fastforce
    show "(x,y) ∈ VWF" if "?f x < ?f y"
      using that ‡ ‹small H› 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 β) VWF = β"
    by (subst ordertype_eq_iff) (use assms in auto)
qed

lemma ordertype_infinite_ω:
  assumes "A ⊆ elts ω" "infinite A"
  shows "ordertype A VWF = ω"
proof (rule antisym)
  show "ordertype A VWF ≤ ω"
    by (simp add: assms ordertype_le_Ord)
  show "ω ≤ ordertype A VWF"
    using assms down ordertype_infinite_ge_ω by auto
qed

text ‹For infinite sets of natural numbers›
lemma ordertype_nat_ω:
  assumes "infinite N" shows "ordertype N less_than = ω"
proof -
  have "small N"
    by (meson inj_on_def ord_of_nat_inject small_def small_iff_range small_image_nat_V)
  have "ordertype (ord_of_nat ` N) VWF = ω"
    by (force simp: assms finite_image_iff inj_on_def intro: ordertype_infinite_ω)
  moreover have "ordertype (ord_of_nat ` N) VWF = ordertype N less_than"
    by (auto intro: ordertype_inc_eq ‹small N›)
  ultimately show ?thesis
    by simp
qed

proposition ordertype_eq_ordertype:
  assumes r: "wf r" "total_on A r" "trans r" and "small A"
  assumes s: "wf s" "total_on B s" "trans s" and "small B"
  shows "ordertype A r = ordertype B s ⟷
         (∃f. bij_betw f A B ∧ (∀x ∈ A. ∀y ∈ A. (f x, f y) ∈ s ⟷ (x,y) ∈ r))"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  define γ where "γ = 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 ≡ inv_into B (ordermap B s) ∘ ordermap A r"
  show ?rhs
  proof (intro exI conjI)
    have bijA: "bij_betw (ordermap A r) A (elts γ)"
      unfolding γ_def using ordermap_bij ‹small A› r by blast
    moreover have bijB: "bij_betw (ordermap B s) B (elts γ)"
      by (simp add: L γ_def ordermap_bij ‹small B› 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: "⋀α. α ∈ elts γ ⟹ ordermap B s (inv_into B (ordermap B s) α) = α"
      by (meson bijB bij_betw_inv_into_right)
    have ordermap_A_γ: "⋀a. a ∈ A ⟹ ordermap A r a ∈ elts γ"
      using bijA bij_betwE by auto
    have f_in_B: "⋀a. a ∈ A ⟹ f a ∈ B"
      using bij bij_betwE by fastforce
    show "∀x∈A. ∀y∈A. (f x, f y) ∈ s ⟷ (x, y) ∈ r"
    proof (intro iffI ballI)
      fix x y
      assume "x ∈ A" "y ∈ A" and ins: "(f x, f y) ∈ s"
      then have "ordermap A r x < ordermap A r y"
        unfolding o_def 
        by (metis (mono_tags, lifting) f_def ‹small B› comp_apply f_in_B invB ordermap_A_γ ordermap_mono_less s(1) s(3))
      then show "(x, y) ∈ r"
        by (metis ‹x ∈ A› ‹y ∈ A› ‹small A› order.asym ordermap_mono_less r total_on_def)
    next
      fix x y
      assume "x ∈ A" "y ∈ A" and "(x, y) ∈ r"
      then have "ordermap A r x < ordermap A r y"
        by (simp add: ‹small A› ordermap_mono_less r)
      then have "(f y, f x) ∉ s"
        by (metis (mono_tags, lifting) ‹x ∈ A› ‹y ∈ A› ‹small B› comp_apply f_def f_in_B invB order.asym ordermap_A_γ ordermap_mono_less s(1) s(3))
      moreover have "f y ≠ f x"
        by (metis ‹(x, y) ∈ r› ‹x ∈ A› ‹y ∈ A› bij bij_betw_inv_into_left r(1) wf_not_sym)
      ultimately show "(f x, f y) ∈ s"
        by (meson ‹x ∈ A› ‹y ∈ A› f_in_B s(2) total_on_def)
    qed
  qed
next
  assume ?rhs
  then show ?lhs
    using assms ordertype_eqI  by blast
qed

corollary ordertype_eq_ordertype_iso:
  assumes r: "wf r" "total_on A r" "trans r" and "small A" and FA: "Field r = A"
  assumes s: "wf s" "total_on B s" "trans s" and "small B" and FB: "Field s = B"
  shows "ordertype A r = ordertype B s ⟷ (∃f. iso r s f)"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then obtain f where "bij_betw f A B" "∀x ∈ A. ∀y ∈ A. (f x, f y) ∈ s ⟷ (x,y) ∈ r"
    using assms ordertype_eq_ordertype by blast
  then show ?rhs
    using FA FB iso_iff2 by blast
next
  assume ?rhs
  then show ?lhs
    using FA FB ‹small A› iso_imp_ordertype_eq_ordertype r by blast
qed

lemma Limit_ordertype_imp_Field_Restr:
  assumes Lim: "Limit (ordertype A r)" and r: "wf r" "total_on A r" and "small A"
  shows "Field (Restr r A) = A"
proof -
  have "∃y∈A. (x,y) ∈ r" if "x ∈ A" for x
  proof -
    let ?oy = "succ (ordermap A r x)"
    have §: "?oy ∈ elts (ordertype A r)"
      by (simp add: Lim ‹small A› ordermap_in_ordertype succ_in_Limit_iff that)
    then have A: "inv_into A (ordermap A r) ?oy ∈ A"
      by (simp add: inv_into_ordermap)
    moreover have "(x, inv_into A (ordermap A r) ?oy) ∈ r"
    proof -
      have "ordermap A r x ∈ elts (ordermap A r (inv_into A (ordermap A r) ?oy))"
        by (metis "§" elts_succ f_inv_into_f insert_iff ordermap_surj subsetD)
      then show ?thesis
        by (metis ‹small A› A converse_ordermap_mono r that)
    qed
    ultimately show ?thesis ..
  qed
  then have "A ⊆ Field (Restr r A)"
    by (auto simp: Field_def)
  then show ?thesis
    by (simp add: Field_Restr_subset subset_antisym)
qed

lemma ordertype_Field_Restr:
  assumes "wf r" "total_on A r" "trans r" "small A" "Field (Restr r A) = A"
  shows "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r"
  using assms by (force simp: ordertype_eq_ordertype wf_Int1 total_on_def trans_Restr)

proposition ordertype_eq_ordertype_iso_Restr:
  assumes r: "wf r" "total_on A r" "trans r" and "small A" and FA: "Field (Restr r A) = A"
  assumes s: "wf s" "total_on B s" "trans s" and "small B" and FB: "Field (Restr s B) = B"
  shows "ordertype A r = ordertype B s ⟷ (∃f. iso (Restr r A) (Restr s B) f)"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then obtain f where "bij_betw f A B" "∀x ∈ A. ∀y ∈ A. (f x, f y) ∈ s ⟷ (x,y) ∈ r"
    using assms ordertype_eq_ordertype by blast
  then show ?rhs
    using FA FB bij_betwE unfolding iso_iff2 by fastforce
next
  assume ?rhs
  moreover
  have "ordertype (Field (Restr r A)) (Restr r A) = ordertype A r"
    using FA ‹small A› ordertype_Field_Restr r by blast
  moreover
  have "ordertype (Field (Restr s B)) (Restr s B) = ordertype B s"
    using FB ‹small B› ordertype_Field_Restr s by blast
  ultimately show ?lhs
    using iso_imp_ordertype_eq_ordertype FA FB ‹small A› r
    by (fastforce intro: total_on_imp_Total_Restr trans_Restr wf_Int1)
qed

lemma ordermap_insert:
  assumes "Ord α" and y: "Ord y" "y ≤ α" and U: "U ⊆ elts α"
  shows "ordermap (insert α U) VWF y = ordermap U VWF y"
  using y
proof (induction rule: Ord_induct)
  case (step y)
  then have 1: "{u ∈ U. (u, y) ∈ VWF} = elts y ∩ 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 ∈ insert α U. (u, y) ∈ VWF} = elts y ∩ 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 α" and U: "U ⊆ elts α"
  shows "ordertype (insert α U) VWF = succ (ordertype U VWF)"
proof -
  have †: "{y ∈ insert α U. (y, α) ∈ VWF} = U" "{y ∈ U. (y, α) ∈ VWF} = U"
    using Ord_in_Ord OrdmemD assms by auto
  have eq: "⋀x. x ∈ U ⟹ ordermap (insert α 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 α U) VWF =
        ZFC_in_HOL.set (insert (ordermap U VWF α) (ordermap U VWF ` U))"
    by (simp add: ordertype_def ordermap_insert assms eq)
  also have "… = succ (ZFC_in_HOL.set (ordermap U VWF ` U))"
    using "†" U by (simp add: ordermap [OF wf_VWF, of _ α] down succ_def vinsert_def)
  also have "… = 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 ≤ 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 ‹finite A›)
  moreover have "card (ordermap A r ` A) ≤ card A"
    using ‹finite A› card_image_le by blast
  ultimately show ?thesis
    by (metis Ord_linear_le Ord_ord_of_nat ‹finite A› card_ord_of_nat card_seteq finite_imageI less_eq_V_def)
qed

lemma ordertype_VWF_ω:
  assumes "finite A"
  shows "ordertype A VWF ∈ elts ω"
proof -
  have "finite (ordermap A VWF ` A)"
    using assms by blast
  then have "ordertype A VWF < ω"
    by (meson Ord_ω OrdmemD trans_VWF wf_VWF assms finite_ordertype_le_card le_less_trans ord_of_nat_ω)
  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 ω_def assms bij_betw_same_card card_ord_of_nat elts_of_set f_inv_into_f inf ordertype_VWF_ω)

lemma finite_ordertype_eq_card:
  assumes "small A" "wf r" "trans r" "total_on A r"
  shows "ordertype A r = ord_of_nat m ⟷ finite A ∧ card A = m"
  using ordermap_bij [OF ‹wf r›]
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 ⊆ ON"
  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on {..<card M} h"
proof -
  have bij: "bij_betw (ordermap M VWF) M (elts (card M))"
    using Finite_V ‹finite M› ordermap_bij ordertype_VWF_finite_nat by fastforce
  let ?h = "(inv_into M (ordermap M VWF)) ∘ 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 {..<card M} ?h"
    proof -
      have "?h m < ?h n"
        if "m < n" "n < card M" for m n
      proof (rule ccontr)
        obtain mn: "m ∈ elts (ordertype M VWF)" "n ∈ elts (ordertype M VWF)"
          using ‹m < n› ‹n < card M› ‹finite M› 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 "¬ ?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 ‹m < n› show False by blast 
        next
          case 2
          then have "ord_of_nat n ≤ 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 ‹m < n› by blast
        qed
      qed
      with assms show ?thesis
        by (auto simp: strict_mono_on_def)
    qed
  qed
qed

lemma ordertype_finite_less_than [simp]: 
  assumes "finite A" shows "ordertype A less_than = card A"
proof -
  let ?M = "ord_of_nat ` A"
  obtain M: "finite ?M" "?M ⊆ ON"
    using Ord_ord_of_nat assms by blast
  have "ordertype A less_than = ordertype ?M VWF"
    by (rule ordertype_inc_eq [symmetric]) (use assms finite_imp_small total_on_def in ‹force+›)
  also have "… = card A"
  proof (subst ordertype_eq_iff)
    let ?M = "ord_of_nat ` A"
    obtain h where bijh: "bij_betw h {..<card A} ?M" and smh: "strict_mono_on {..<card A} h"
      by (metis M card_image ex_bij_betw_strict_mono_card inj_on_def ord_of_nat_inject)
    define f where "f ≡ ord_of_nat ∘ inv_into {..<card A} h"
    show "∃f. bij_betw f ?M (elts (card A)) ∧ (∀x∈?M. ∀y∈?M. f x < f y ⟷ ((x, y) ∈ VWF))"
    proof (intro exI conjI ballI)
      have "bij_betw (ord_of_nat ∘ inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})"
        by (meson UNIV_I bijh bij_betw_def bij_betw_inv_into bij_betw_subset bij_betw_trans inj_ord_of_nat subsetI)
      then show "bij_betw f ?M (elts (card A))"
        by (metis elts_ord_of_nat f_def)
    next
      fix x y
      assume xy: "x ∈ ?M" "y ∈ ?M"
      then obtain m n where "x = ord_of_nat m" "y = ord_of_nat n"
        by auto
      have "(f x < f y) ⟷ ((h ∘ inv_into {..<card A} h) x < (h ∘ inv_into {..<card A} h) y)"
        unfolding f_def using smh bij_betw_imp_surj_on [OF bijh] 
        apply simp
        by (metis (mono_tags, lifting) inv_into_into not_less_iff_gr_or_eq order.asym strict_mono_onD xy)
      also have "… = (x < y)"
        using bijh
        by (simp add: bij_betw_inv_into_right xy)
      also have "… ⟷ ((x, y) ∈ VWF)"
        using M(2) ON_imp_Ord xy by auto
      finally show "(f x < f y) ⟷ ((x, y) ∈ VWF)" . 
    qed 
  qed auto
  finally show ?thesis .
qed


subsection ‹Cardinality of an arbitrary HOL set›

definition gcard :: "'a set ⇒ V" 
  where "gcard X ≡ if small X then (LEAST i. Ord i ∧ elts i ≈ X) else 0"

subsection‹Cardinality of a set›

definition vcard :: "V⇒V"
  where "vcard a ≡ (LEAST i. Ord i ∧ elts i ≈ elts a)"

lemma gcard_eq_vcard [simp]: "gcard (elts x) = vcard x"
  by (simp add: vcard_def gcard_def)

definition Card:: "V⇒bool"
  where "Card i ≡ i = vcard i"

abbreviation CARD where "CARD ≡ Collect Card"

lemma cardinal_cong: "elts x ≈ elts y ⟹ vcard x = vcard y"
  unfolding vcard_def by (meson eqpoll_sym eqpoll_trans)

lemma gcardinal_cong:
  assumes "X ≈ Y" shows "gcard X = gcard Y"
proof -
  have "(LEAST i. Ord i ∧ elts i ≈ X) = (LEAST i. Ord i ∧ elts i ≈ Y)"
    by (meson eqpoll_sym eqpoll_trans assms)
  then show ?thesis
    unfolding gcard_def
    by (meson eqpoll_sym small_eqcong assms)
qed

lemma vcard_set_image: "inj_on f (elts x) ⟹ vcard (set (f ` elts x)) = vcard x"
  by (simp add: cardinal_cong)

lemma gcard_image: "inj_on f X ⟹ gcard (f ` X) = gcard X"
  by (simp add: gcardinal_cong)

lemma Card_cardinal_eq: "Card κ ⟹ vcard κ = κ"
  by (simp add: Card_def)

lemma Card_is_Ord:
  assumes "Card κ" shows "Ord κ"
proof -
  obtain α where "Ord α" "elts α ≈ elts κ"
    using Ord_ordertype ordertype_eqpoll by blast
  then have "Ord (LEAST i. Ord i ∧ elts i ≈ elts κ)"
    by (metis Ord_Least)
  then show ?thesis
    using Card_def vcard_def assms by auto
qed

lemma cardinal_eqpoll: "elts (vcard a) ≈ 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 ∈ elts A → 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

lemma subset_smaller_vcard:
  assumes "κ ≤ vcard x" "Card κ"
  obtains y where "y ≤ x" "vcard y = κ"
proof -
  obtain φ where φ: "bij_betw φ (elts (vcard x)) (elts x)"
    using cardinal_eqpoll eqpoll_def by blast
  show thesis
  proof
    let ?y = "ZFC_in_HOL.set (φ ` elts κ)"
    show "?y ≤ x"
      by (meson φ assms bij_betwE set_image_le_iff small_elts vsubsetD) 
    show "vcard ?y = κ"
      by (metis vcard_set_image Card_def assms bij_betw_def bij_betw_subset φ less_eq_V_def)
  qed
qed

text‹every natural number is a (finite) cardinal›
lemma nat_into_Card:
  assumes "α ∈ elts ω" shows "Card(α)"
proof (unfold Card_def vcard_def, rule sym)
  obtain n where n: "α = ord_of_nat n"
    by (metis ω_def assms elts_of_set imageE inf)
  have "Ord(α)" using assms by auto
  moreover
  { fix β
    assume "β < α" "Ord β" "elts β ≈ elts α"
    with n have "elts β ≈ {..<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  ‹Ord β› ‹β < α› ‹Ord(α)›
      by (metis ‹elts β ≈ elts α› 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 ∧ elts i ≈ elts α) = α"
      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: ω_def nat_into_Card)

lemma Card_0 [iff]: "Card 0"
  by (simp add: nat_into_Card)

lemma CardI: "⟦Ord i; ⋀j. ⟦j < i; Ord j⟧ ⟹ ¬ elts j ≈ elts i⟧ ⟹ 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)

lemma gcard_big_0: "¬ small X ⟹ gcard X = 0"
  by (simp add: gcard_def)

lemma gcard_eq_card:
  assumes "finite X" shows "gcard X = ord_of_nat (card X)"
proof -
  have "⋀y. Ord y ∧ elts y ≈ X ⟹ ord_of_nat (card X) ≤ y"
    by (metis assms eqpoll_finite_iff eqpoll_iff_card order_le_less ordertype_VWF_finite_nat ordertype_eq_Ord)
  then have "(LEAST i. Ord i ∧ elts i ≈ X) = ord_of_nat (card X)"
    by (simp add: assms eqpoll_iff_card finite_Ord_omega Least_equality)
  with assms show ?thesis
    by (simp add: finite_imp_small gcard_def)
qed

lemma gcard_empty_0 [simp]: "gcard {} = 0"
  by (simp add: gcard_eq_card) 

lemma gcard_single_1 [simp]: "gcard {x} = 1"
  by (simp add: gcard_eq_card one_V_def)

lemma Card_gcard [iff]: "Card (gcard X)"
  by (metis Card_0 Card_def cardinal_idem gcard_big_0 gcardinal_cong small_eqpoll gcard_eq_vcard)

lemma gcard_eqpoll: "small X ⟹ elts (gcard X) ≈ X"
  by (metis cardinal_eqpoll eqpoll_trans gcard_eq_vcard gcardinal_cong small_eqpoll)

lemma lepoll_imp_gcard_le:
  assumes "A ≲ B" "small B"
  shows "gcard A ≤ gcard B"
proof -
  have "elts (gcard A) ≈ A" "elts (gcard B) ≈ B"
    by (meson assms gcard_eqpoll lepoll_small)+
  with ‹A ≲ B› show ?thesis
    by (metis Ord_cardinal Ord_linear2 eqpoll_sym gcard_eq_vcard gcardinal_cong lepoll_antisym
              lepoll_trans2 less_V_def less_eq_V_def subset_imp_lepoll)
qed

lemma gcard_image_le:
  assumes "small A" shows "gcard (f ` A) ≤ gcard A"
  using assms image_lepoll lepoll_imp_gcard_le by blast

lemma subset_imp_gcard_le:
  assumes "A ⊆ B" "small B"
  shows "gcard A ≤ gcard B"
  by (simp add: assms lepoll_imp_gcard_le subset_imp_lepoll)

lemma gcard_le_lepoll: "⟦gcard A ≤ α; small A⟧ ⟹ A ≲ elts α"
  by (meson eqpoll_sym gcard_eqpoll lepoll_trans1 less_eq_V_def subset_imp_lepoll)

subsection‹Cardinality of a set›

text‹The cardinals are the initial ordinals.›
lemma Card_iff_initial: "Card κ ⟷ Ord κ ∧ (∀α. Ord α ∧ α < κ ⟶ ~ elts α ≈ elts κ)"
  by (metis CardI Card_def Card_is_Ord not_less_Ord_Least vcard_def)

lemma Card_ω [iff]: "Card ω"
  by (meson CardI Ord_ω eqpoll_finite_iff infinite_Ord_omega infinite_ω leD)

lemma lt_Card_imp_lesspoll: "⟦i < a; Card a; Ord i⟧ ⟹ elts i ≺ 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 ≲ elts b" shows "vcard a ≤ vcard b"
  using assms lepoll_imp_gcard_le by fastforce

lemma lepoll_cardinal_le: "⟦elts A ≲ elts i; Ord i⟧ ⟹ vcard A ≤ 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 ≤ α ⟹ elts A ≲ elts α"
  by (meson cardinal_eqpoll eqpoll_sym lepoll_trans1 less_eq_V_def subset_imp_lepoll)

lemma lesspoll_imp_Card_less:
  assumes "elts a ≺ elts b" shows "vcard a < vcard b"
  by (metis assms cardinal_eqpoll eqpoll_sym eqpoll_trans lepoll_imp_Card_le less_V_def lesspoll_def)


lemma Card_Union [simp,intro]:
  assumes A: "⋀x. x ∈ A ⟹ Card(x)" shows "Card(⨆A)"
proof (rule CardI)
  show "Ord(⨆A)" using A
    by (simp add: Card_is_Ord Ord_Sup)
next
  fix j
  assume j: "j < ⨆A" "Ord j"
  hence "∃c∈A. j < c ∧ Card(c)" using A
    by (meson Card_is_Ord Ord_linear2 ZFC_in_HOL.Sup_least leD)
  then obtain c where c: "c∈A" "j < c" "Card(c)"
    by blast
  hence jls: "elts j ≺ elts c"
    using j(2) lt_Card_imp_lesspoll by blast
  { assume eqp: "elts j ≈ elts (⨆A)"
    have  "elts c ≲ elts (⨆A)" using c
      by (metis Card_def Sup_V_def ZFC_in_HOL.Sup_upper cardinal_le_lepoll j(1) not_less_0)
    also have "... ≈ elts j"  by (rule eqpoll_sym [OF eqp])
    also have "... ≺ elts c"  by (rule jls)
    finally have "elts c ≺ elts c" .
    hence False
      by auto
  } thus "¬ elts j ≈ elts (⨆A)" by blast
qed

lemma Card_UN: "(⋀x. x ∈ A ⟹ Card(K x)) ==> Card(Sup (K ` A))"
  by blast

subsection‹Transfinite recursion for definitions based on the three cases of ordinals›

definition
  transrec3 :: "[V, [V,V]⇒V, [V,V⇒V]⇒V, V] ⇒ V" where
    "transrec3 a b c ≡
       transrec (λr x.
         if x=0 then a
         else if Limit x then c x (λy ∈ 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 ⟹  transrec3 a b c i = c i (λj ∈ elts i. transrec3 a b c j)"
  unfolding transrec3_def
  by (subst transrec) auto


subsection ‹Cardinal Addition›

definition cadd :: "[V,V]⇒V"       (infixl ‹⊕› 65)
  where "κ ⊕ μ ≡ vcard (κ ⨄ μ)"

subsubsection‹Cardinal addition is commutative›

lemma vsum_commute_eqpoll: "elts (a⨄b) ≈ elts (b⨄a)"
proof -
  have "bij_betw (λz ∈ elts (a⨄b). sum_case Inr Inl z) (elts (a⨄b)) (elts (b⨄a))"
    unfolding bij_betw_def
  proof (intro conjI inj_onI)
    show "restrict (sum_case Inr Inl) (elts (a ⨄ b)) ` elts (a ⨄ b) = elts (b ⨄ 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 ⊕ j = j ⊕ i"
  by (simp add: cadd_def cardinal_cong vsum_commute_eqpoll)

subsubsection‹Cardinal addition is associative›

lemma sum_assoc_bij:
  "bij_betw (λz ∈ elts ((a⨄b)⨄c). sum_case(sum_case Inl (λy. Inr(Inl y))) (λy. Inr(Inr y)) z)
      (elts ((a⨄b)⨄c)) (elts (a⨄(b⨄c)))"
  by (rule_tac f' = "sum_case (λx. Inl (Inl x)) (sum_case (λx. Inl (Inr x)) Inr)"
      in bij_betw_byWitness) auto

lemma sum_assoc_eqpoll: "elts ((a⨄b)⨄c) ≈ elts (a⨄(b⨄c))"
  unfolding eqpoll_def by (metis sum_assoc_bij)

lemma elts_vcard_vsum_eqpoll: "elts (vcard (i ⨄ j)) ≈ Inl ` elts i ∪ Inr ` elts j"
proof -
  have "elts (i ⨄ j) ≈ Inl ` elts i ∪ Inr ` elts j"
    by (simp add: elts_vsum)
  then show ?thesis
    using cardinal_eqpoll eqpoll_trans by blast
qed

lemma cadd_assoc: "(i ⊕ j) ⊕ k = i ⊕ (j ⊕ k)"
proof (unfold cadd_def, rule cardinal_cong)
  have "elts (vcard(i ⨄ j) ⨄ k) ≈ elts ((i ⨄ j) ⨄ k)"
    by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll intro: Un_eqpoll_cong)
  also have "…  ≈ elts (i ⨄ (j ⨄ k))"
    by (rule sum_assoc_eqpoll)
  also have "…  ≈ elts (i ⨄ vcard(j ⨄ k))"
    by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll [THEN eqpoll_sym] intro: Un_eqpoll_cong)
  finally show "elts (vcard (i ⨄ j) ⨄ k) ≈ elts (i ⨄ vcard (j ⨄ k))" .
qed

lemma cadd_left_commute: "j ⊕ (i ⊕ k) = i ⊕ (j ⊕ k)"
  using cadd_assoc cadd_commute by force

lemmas cadd_ac = cadd_assoc cadd_commute cadd_left_commute

text‹0 is the identity for addition›
lemma vsum_0_eqpoll: "elts (0⨄a) ≈ elts a"
  by (simp add: elts_vsum)

lemma cadd_0 [simp]: "Card κ ⟹ 0 ⊕ κ = κ"
  by (metis Card_def cadd_def cardinal_cong vsum_0_eqpoll)

lemma cadd_0_right [simp]: "Card κ ⟹ κ ⊕ 0 = κ"
  by (simp add: cadd_commute)

lemma vsum_lepoll_self: "elts a ≲ elts (a⨄b)"
  unfolding elts_vsum  by (meson Inl_iff Un_upper1 inj_onI lepoll_def)

lemma cadd_le_self:
  assumes κ: "Card κ" shows "κ ≤ κ ⊕ a"
proof (unfold cadd_def)
  have "κ ≤ vcard κ"
    using Card_def κ by auto
  also have "… ≤ vcard (κ ⨄ a)"
    by (simp add: lepoll_imp_Card_le vsum_lepoll_self)
  finally show "κ ≤ vcard (κ ⨄ a)" .
qed

text‹Monotonicity of addition›
lemma cadd_le_mono: "⟦κ' ≤ κ; μ' ≤ μ⟧ ⟹ κ' ⊕ μ' ≤ κ ⊕ μ"
  unfolding cadd_def
  by (metis (no_types) lepoll_imp_Card_le less_eq_V_def subset_imp_lepoll sum_subset_iff)

subsection‹Cardinal multiplication›

definition cmult :: "[V,V]⇒V"       (infixl ‹⊗› 70)
  where "κ ⊗ μ ≡ vcard (VSigma κ (λz. μ))"

subsubsection‹Cardinal multiplication is commutative›

lemma prod_bij: "⟦bij_betw f A C; bij_betw g B D⟧
             ⟹ bij_betw (λ(x, y). (f x, g y)) (A × B) (C × D)"
  apply (rule bij_betw_byWitness [where f' = "λ(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 ⊗ j = j ⊗ i"
proof -
  have "(λ(x, y). ⟨x, y⟩) ` (elts i × elts j) ≈ (λ(x, y). ⟨x, y⟩) ` (elts j × elts i)"
    by (simp add: times_commute_eqpoll)
  then show ?thesis
    unfolding cmult_def
    using cardinal_cong elts_VSigma by auto
qed

subsubsection‹Cardinal multiplication is associative›

lemma elts_vcard_VSigma_eqpoll: "elts (vcard (vtimes i j)) ≈ elts i × elts j"
proof -
  have "elts (vtimes i j) ≈ elts i × elts j"
    by (simp add: elts_VSigma)
  then show ?thesis
    using cardinal_eqpoll eqpoll_trans by blast
qed

lemma elts_cmult: "elts (κ' ⊗ κ) ≈ elts κ' × elts κ"
  by (simp add: cmult_def elts_vcard_VSigma_eqpoll)

lemma cmult_assoc: "(i ⊗ j) ⊗ k = i ⊗ (j ⊗ k)"
  unfolding cmult_def
proof (rule cardinal_cong)
  have "elts (vcard (vtimes i j)) × elts k ≈ (elts i × elts j) × elts k"
    by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll)
  also have "…  ≈ elts i × (elts j × elts k)"
    by (rule times_assoc_eqpoll)
  also have "…  ≈ elts i × 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)) (λz. k)) ≈ elts (VSigma i (λz. vcard (vtimes j k)))"
    by (simp add: elts_VSigma)
qed

subsubsection‹Cardinal multiplication distributes over addition›

lemma cadd_cmult_distrib: "(i ⊕ j) ⊗ k = (i ⊗ k) ⊕ (j ⊗ k)"
  unfolding cadd_def cmult_def
proof (rule cardinal_cong)
have "elts (vtimes (vcard (i ⨄ j)) k) ≈ elts (vcard (vsum i j)) × elts k"
  using cardinal_eqpoll elts_vcard_VSigma_eqpoll eqpoll_sym eqpoll_trans by blast
  also have "… ≈ (Inl ` elts i ∪ Inr ` elts j) × elts k"
    using elts_vcard_vsum_eqpoll times_eqpoll_cong by blast
  also have "… ≈ (Inl ` elts i) × elts k ∪ (Inr ` elts j) × elts k"
    by (simp add: Sigma_Un_distrib1)
  also have "…  ≈ elts (vtimes i k ⨄ vtimes j k)"
    unfolding Plus_def
    by (auto simp: elts_vsum elts_VSigma disjnt_iff intro!: Un_eqpoll_cong times_eqpoll_cong)
  also have "…  ≈ elts (vcard (vtimes i k ⨄ vtimes j k))"
    by (simp add: cardinal_eqpoll eqpoll_sym)
  also have "…  ≈ elts (vcard (vtimes i k) ⨄ 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 ⨄ j)) (λz. k))
             ≈ elts (vcard (vtimes i k) ⨄ vcard (vtimes j k))" .
qed

text‹Multiplication by 0 yields 0›
lemma cmult_0 [simp]: "0 ⊗ i = 0"
  using Card_0 Card_def cmult_def by auto

text‹1 is the identity for multiplication›
lemma cmult_1 [simp]: assumes "Card κ" shows "1 ⊗ κ = κ"
proof -
  have "elts (vtimes (set {0}) κ) ≈ elts κ"
    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‹Some inequalities for multiplication›

lemma cmult_square_le: assumes "Card κ" shows "κ ≤ κ ⊗ κ"
proof -
  have "elts κ ≲ elts (κ ⊗ κ)"
    using times_square_lepoll [of "elts κ"] 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‹Multiplication by a non-empty set›
lemma cmult_le_self: assumes "Card κ" "α ≠ 0" shows "κ ≤ κ ⊗ α"
proof -
  have "κ = vcard κ"
    using Card_def ‹Card κ› by blast
  also have "… ≤ vcard (vtimes κ α)"
    apply (rule lepoll_imp_Card_le)
    apply (simp add: elts_VSigma)
    by (metis ZFC_in_HOL.ext ‹α ≠ 0› elts_0 lepoll_times1)
  also have "… = κ ⊗ α"
    by (simp add: cmult_def)
  finally show ?thesis .
qed


text‹Monotonicity of multiplication›
lemma cmult_le_mono: "⟦κ' ≤ κ; μ' ≤ μ⟧ ⟹ κ' ⊗ μ' ≤ κ ⊗ μ"
  unfolding cmult_def
  by (auto simp: elts_VSigma intro!: lepoll_imp_Card_le times_lepoll_mono subset_imp_lepoll)

lemma vcard_Sup_le_cmult:
  assumes "small U" and κ: "⋀x. x ∈ U ⟹ vcard x ≤ κ"
  shows "vcard (⨆U) ≤ vcard (set U) ⊗ κ"
proof -
  have "∃f. f ∈ elts x → elts κ ∧ inj_on f (elts x)" if "x ∈ U" for x
    using κ [OF that] by (metis cardinal_le_lepoll image_subset_iff_funcset lepoll_def)
  then obtain φ where φ: "⋀x. x ∈ U ⟹ (φ x) ∈ elts x → elts κ ∧ inj_on (φ x) (elts x)"
    by metis
  define u where "u ≡ λy. @x. x ∈ U ∧ y ∈ elts x"
  have u: "u y ∈ U ∧ y ∈ elts (u y)" if "y ∈ ⋃(elts ` U)" for y
    unfolding u_def by (metis (mono_tags, lifting)that someI2_ex UN_iff)  
  define ψ where "ψ ≡ λy. (u y, φ (u y) y)"
  have U: "elts (vcard (set U)) ≈ U"
    by (metis ‹small U› cardinal_eqpoll elts_of_set)
  have "elts (⨆U) = ⋃(elts ` U)"
    using ‹small U› by blast
  also have "… ≲ U × elts κ"
    unfolding lepoll_def
  proof (intro exI conjI)
    show "inj_on ψ (⋃ (elts ` U))"
      using φ u by (smt (verit) ψ_def inj_on_def prod.inject)
    show "ψ ` ⋃ (elts ` U) ⊆ U × elts κ"
      using φ u by (auto simp: ψ_def)
  qed
  also have "…  ≈ elts (vcard (set U) ⊗ κ)"
    using U elts_cmult eqpoll_sym eqpoll_trans times_eqpoll_cong by blast
  finally have "elts (⨆ U) ≲ elts (vcard (set U) ⊗ κ)" .
  then show ?thesis
    by (simp add: cmult_def lepoll_cardinal_le)
qed

subsection‹The finite cardinals›

lemma succ_lepoll_succD: "elts (succ(m)) ≲ elts (succ(n)) ⟹ elts m ≲ elts n"
  by (simp add: insert_lepoll_insertD)


text‹Congruence law for @{text succ} under equipollence›
lemma succ_eqpoll_cong: "elts a ≈ elts b ⟹ elts (succ(a)) ≈ elts (succ(b))"
  by (simp add: succ_def insert_eqpoll_cong)

lemma sum_succ_eqpoll: "elts (succ a ⨄ b) ≈ elts (succ(a⨄b))"
  unfolding eqpoll_def
proof (rule exI)
  let ?f = "λz. if z=Inl a then a⨄b else z"
  let ?g = "λz. if z=a⨄b then Inl a else z"
  show "bij_betw ?f (elts (succ a ⨄ b)) (elts (succ (a ⨄ 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 ⊕ n = vcard (succ(m ⊕ n))"
proof (unfold cadd_def)
  have [intro]: "elts (m ⨄ n) ≈ elts (vcard (m ⨄ n))"
    using cardinal_eqpoll eqpoll_sym by blast
  have "vcard (succ m ⨄ n) = vcard (succ(m ⨄ n))"
    by (rule sum_succ_eqpoll [THEN cardinal_cong])
  also have "… = vcard (succ(vcard (m ⨄ n)))"
    by (blast intro: succ_eqpoll_cong cardinal_cong)
  finally show "vcard (succ m ⨄ n) = vcard (succ(vcard (m ⨄ n)))" .
qed

lemma nat_cadd_eq_add: "ord_of_nat m ⊕ 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 ⊓ y = 0" shows "vcard (x ⊔ y) = vcard x ⊕ vcard y"
proof -
  have "elts (x ⊔ y) ≈ elts (x ⨄ y)"
    unfolding eqpoll_def
  proof (rule exI)
    let ?f = "λz. if z ∈ elts x then Inl z else Inr z"
    let ?g = "sum_case id id"
    show "bij_betw ?f (elts (x ⊔ y)) (elts (x ⨄ 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

lemma vcard_sup: "vcard (x ⊔ y) ≤ vcard x ⊕ vcard y"
proof -
  have "elts (x ⊔ y) ≲ elts (x ⨄ y)"
    unfolding lepoll_def
  proof (intro exI conjI)
    let ?f = "λz. if z ∈ elts x then Inl z else Inr z"
    show "inj_on ?f (elts (x ⊔ y))"
      by (simp add: inj_on_def)
    show "?f ` elts (x ⊔ y) ⊆ elts (x ⨄ y)"
      by force
  qed
  then show ?thesis
    using cadd_ac
    by (metis cadd_def cardinal_cong cardinal_idem lepoll_imp_Card_le vsum_0_eqpoll)
qed

subsection‹Infinite cardinals›

definition InfCard :: "V⇒bool"
  where "InfCard κ ≡ Card κ ∧ ω ≤ κ"

lemma InfCard_iff: "InfCard κ ⟷ Card κ ∧ infinite (elts κ)"
proof (cases "ω ≤ κ")
  case True
  then show ?thesis
    using inj_ord_of_nat lepoll_def less_eq_V_def
    by (auto simp: InfCard_def ω_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 κ" shows "ord_of_nat n ≤ κ"
  using InfCard_def assms ord_of_nat_le_omega by blast

lemma InfCard_not_0[iff]: "¬ InfCard 0"
  by (simp add: InfCard_iff)

definition csucc :: "V⇒V"
  where "csucc κ ≡ LEAST κ'. Ord κ' ∧ (Card κ' ∧ κ < κ')"


lemma less_vcard_VPow: "vcard A < vcard (VPow A)"
proof (rule lesspoll_imp_Card_less)
  show "elts A ≺ elts (VPow A)"
    by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self)
qed

lemma greater_Card:
  assumes "Card κ" shows "κ < vcard (VPow κ)"
proof -
  have "κ = vcard κ"
    using Card_def assms by blast
  also have "… < vcard (VPow κ)"
  proof (rule lesspoll_imp_Card_less)
    show "elts κ ≺ elts (VPow κ)"
      by (simp add: elts_VPow down inj_on_def lesspoll_Pow_self)
  qed
  finally show ?thesis .
qed

lemma
  assumes "Card κ"
  shows Card_csucc [simp]: "Card (csucc κ)" and less_csucc [simp]: "κ < csucc κ"
proof -
  have "Card (csucc κ) ∧ κ < csucc κ"
    unfolding csucc_def
  proof (rule Ord_LeastI2)
    show "Card (vcard (VPow κ)) ∧ κ < (vcard (VPow κ))"
      using Card_def assms greater_Card by auto
  qed auto
  then show "Card (csucc κ)" "κ < csucc κ"
    by auto
qed

lemma le_csucc:
  assumes "Card κ" shows "κ ≤ csucc κ"
  by (simp add: assms less_csucc less_imp_le)


lemma csucc_le: "⟦Card μ; κ ∈ elts μ⟧ ⟹ csucc κ ≤ μ"
  unfolding csucc_def
  by (simp add: Card_is_Ord Ord_Least_le OrdmemD)

lemma finite_csucc: "a ∈ elts ω ⟹ csucc a = succ a"
  unfolding csucc_def
  proof (rule Least_equality)
  show "Ord (ZFC_in_HOL.succ a) ∧ Card (ZFC_in_HOL.succ a) ∧ a < ZFC_in_HOL.succ a"
    if "a ∈ elts ω"
    using that by (auto simp: less_V_def less_eq_V_def nat_into_Card)
  show "ZFC_in_HOL.succ a ≤ y"
    if "a ∈ elts ω"
      and "Ord y ∧ Card y ∧ 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 ∉ 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 "¬ elts (set A) ≈ 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))) ∧ Card (vcard (set (insert a A))) ∧ 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)) ≤ i"
      if "Ord i ∧ Card i ∧ vcard (set A) < i" for i
    proof -
      have "elts (vcard (set A)) ≈ A"
        by (metis FA finite_imp_small cardinal_eqpoll elts_of_set)
      then have less: "A ≺ 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 ⟹ vcard (set A) = ord_of_nat (card A)"
  by (induction A rule: finite_induct) (auto simp: set_empty ω_def finite_csucc)

lemma lt_csucc_iff:
  assumes "Ord α" "Card κ"
  shows "α < csucc κ ⟷ vcard α ≤ κ"
proof
  show "vcard α ≤ κ" if "α < csucc κ"
  proof -
    have "vcard α ≤ csucc κ"
      by (meson ‹Ord α› 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 "α < csucc κ" if "vcard α ≤ κ"
  proof -
    have "¬ csucc κ ≤ α"
      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: "⟦Card κ'; Card κ⟧ ⟹ (κ' < csucc κ) = (κ' ≤ κ)"
  by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)

lemma csucc_lt_csucc_iff: "⟦Card κ'; Card κ⟧ ⟹ (csucc κ' < csucc κ) = (κ' < κ)"
  by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_less)

lemma csucc_le_csucc_iff: "⟦Card κ'; Card κ⟧ ⟹ (csucc κ' ≤ csucc κ) = (κ' ≤ κ)"
  by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_less)

lemma csucc_0 [simp]: "csucc 0 = 1"
  by (simp add: finite_csucc one_V_def)

lemma Card_Un [simp,intro]:
  assumes "Card x" "Card y" shows "Card(x ⊔ y)"
  by (metis Card_is_Ord Ord_linear_le assms sup.absorb2 sup.orderE)

lemma InfCard_csucc: "InfCard κ ⟹ InfCard (csucc κ)"
  using InfCard_def le_csucc by auto

text‹Kunen's Lemma 10.11›
lemma InfCard_is_Limit:
  assumes "InfCard κ" shows "Limit κ"
  proof (rule non_succ_LimitI)
  show "κ ≠ 0"
    using InfCard_def assms mem_not_refl by blast
  show "Ord κ"
    using Card_is_Ord InfCard_def assms by blast
  show "ZFC_in_HOL.succ y ≠ κ" for y
  proof
    assume "succ y = κ"
    then have "Card (succ y)"
      using InfCard_def assms by auto
    moreover have "ω ≤ y"
      by (metis InfCard_iff Ord_in_Ord ‹Ord κ› ‹ZFC_in_HOL.succ y = κ› assms elts_succ finite_insert infinite_Ord_omega insertI1)
    moreover have "elts y ≈ elts (succ y)"
      using InfCard_iff ‹ZFC_in_HOL.succ y = κ› 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‹Toward's Kunen's Corollary 10.13 (1)›

text‹Kunen's Theorem 10.12›
lemma InfCard_csquare_eq:
  assumes "InfCard(κ)" shows "κ ⊗ κ = κ"
  using infinite_times_eqpoll_self [of "elts κ"] 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 κ" "μ ≤ κ" "μ ≠ 0"
  shows "κ ⊗ μ = κ"
proof (rule order_antisym)
  have "κ ⊗ μ ≤ κ ⊗ κ"
    by (simp add: assms(2) cmult_le_mono)
  also have "… ≤ κ"
    by (simp add: InfCard_csquare_eq assms(1))
  finally show "κ ⊗ μ ≤ κ" .
  show "κ ≤ κ ⊗ μ"
    using InfCard_def assms(1) assms(3) cmult_le_self by auto
qed

text‹Kunen's Corollary 10.13 (1), for cardinal multiplication›
lemma InfCard_cmult_eq: "⟦InfCard κ; InfCard μ⟧ ⟹ κ ⊗ μ = κ ⊔ μ"
  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) ⊗ n = n ⊕ (m ⊗ n)"
  unfolding cmult_def cadd_def
proof (rule cardinal_cong)
  have "elts (vtimes (ZFC_in_HOL.succ m) n) ≈ elts n <+> elts m × elts n"
    by (simp add: elts_VSigma prod_insert_eqpoll)
  also have "… ≈ elts (n ⨄ vcard (vtimes m n))"
    unfolding elts_VSigma elts_vsum Plus_def
  proof (rule Un_eqpoll_cong)
    show "(Sum_Type.Inr ` (elts m × elts n)::(V + V × V) set) ≈ 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) ≈ elts (n ⨄ vcard (vtimes m n))" .
qed

lemma cmult_2:
  assumes "Card n" shows "ord_of_nat 2 ⊗ n = n ⊕ 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 κ" shows "κ ⊕ κ = κ"
proof -
  have "κ ⊕ κ = κ ⊗ ord_of_nat 2"
    using InfCard_def assms cmult_2 cmult_commute by auto
  also have "… = κ"
    by (simp add: InfCard_le_cmult_eq InfCard_ge_ord_of_nat assms)
  finally show ?thesis .
qed

text‹Corollary 10.13 (1), for cardinal addition›
lemma InfCard_le_cadd_eq: "⟦InfCard κ; μ ≤ κ⟧ ⟹ κ ⊕ μ = κ"
  by (metis InfCard_cdouble_eq InfCard_def antisym cadd_le_mono cadd_le_self)

lemma InfCard_cadd_eq: "⟦InfCard κ; InfCard μ⟧ ⟹ κ ⊕ μ = κ ⊔ μ"
  by (metis Card_iff_initial InfCard_def InfCard_le_cadd_eq Ord_linear_le cadd_commute sup.absorb2 sup.orderE)

lemma csucc_le_Card_iff: "⟦Card κ'; Card κ⟧ ⟹ csucc κ' ≤ κ ⟷ κ' < κ"
  by (metis Card_csucc Card_is_Ord Card_lt_csucc_iff Ord_not_le)

lemma cadd_InfCard_le:
  assumes "α ≤ κ" "β ≤ κ" "InfCard κ"
  shows "α ⊕ β ≤ κ"
  using assms by (metis InfCard_cdouble_eq cadd_le_mono)

lemma cmult_InfCard_le:
  assumes "α ≤ κ" "β ≤ κ" "InfCard κ"
  shows "α ⊗ β ≤ κ"
  using assms
  by (metis InfCard_csquare_eq cmult_le_mono)

subsection ‹The Aleph-seqence›

text ‹This is the well-known transfinite enumeration of the cardinal numbers.›

definition Aleph :: "V ⇒ V"    (‹ℵ_› [90] 90)
  where "Aleph ≡ transrec (λf x. ω ⊔ ⨆((λy. csucc(f y)) ` elts x))"

lemma Aleph: "Aleph α = ω ⊔ (⨆y∈elts α. csucc (Aleph y))"
  by (simp add: Aleph_def transrec[of _ α])

lemma InfCard_Aleph [simp, intro]: "InfCard(Aleph x)"
proof (induction x rule: eps_induct)
  case (step x)
  then show ?case
    by (simp add: Aleph [of x] InfCard_def Card_UN step)
qed

lemma Card_Aleph [simp, intro]: "Card(Aleph x)"
  using InfCard_def by auto

lemma Aleph_0 [simp]: "ℵ0 = ω"
  by (simp add: Aleph [of 0])

lemma mem_Aleph_succ: "ℵα ∈ elts (Aleph (succ α))"
  apply (simp add: Aleph [of "succ α"])
  by (meson InfCard_Aleph Card_csucc Card_is_Ord InfCard_def Ord_mem_iff_lt less_csucc)

lemma Aleph_lt_succD [simp]: "ℵα < Aleph (succ α)"
  by (simp add: InfCard_is_Limit Limit_is_Ord OrdmemD mem_Aleph_succ)

lemma Aleph_succ [simp]: "Aleph (succ x) = csucc (Aleph x)"
proof (rule antisym)
  show "Aleph (ZFC_in_HOL.succ x) ≤ csucc (Aleph x)"
    apply (simp add: Aleph [of "succ x"])
    by (metis Aleph InfCard_Aleph InfCard_def Sup_V_insert le_csucc le_sup_iff order_refl 
         replacement small_elts)
  show "csucc (Aleph x) ≤ Aleph (ZFC_in_HOL.succ x)"
    by (force simp add: Aleph [of "succ x"])
qed

lemma csucc_Aleph_le_Aleph: "α ∈ elts β ⟹ csucc (ℵα) ≤ ℵβ"
  by (metis Aleph ZFC_in_HOL.SUP_le_iff replacement small_elts sup_ge2)

lemma Aleph_in_Aleph: "α ∈ elts β ⟹ ℵα ∈ elts (ℵβ)"
  using csucc_Aleph_le_Aleph mem_Aleph_succ by auto

lemma Aleph_Limit:
  assumes "Limit γ"
  shows "Aleph γ = ⨆ (Aleph ` elts γ)"
proof -
  have [simp]: "γ ≠ 0"
    using assms by auto 
  show ?thesis
  proof (rule antisym)
    show "Aleph γ ≤ ⨆ (Aleph ` elts γ)"
      apply (simp add: Aleph [of γ])
      by (metis (mono_tags, lifting) Aleph_0 Aleph_succ Limit_def ZFC_in_HOL.SUP_le_iff 
           ZFC_in_HOL.Sup_upper assms imageI replacement small_elts)
    show "⨆ (Aleph ` elts γ) ≤ Aleph γ"
      apply (simp add: cSup_le_iff)
      by (meson InfCard_Aleph InfCard_def csucc_Aleph_le_Aleph le_csucc order_trans)
  qed
qed

lemma Aleph_increasing:
  assumes ab: "α < β" "Ord α" "Ord β" shows "ℵα < ℵβ"
  by (meson Aleph_in_Aleph InfCard_Aleph Card_iff_initial InfCard_def Ord_mem_iff_lt assms)

lemma countable_iff_le_Aleph0: "countable (elts A) ⟷ vcard A ≤ ℵ0"
proof
  show "vcard A ≤ ℵ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 ω ≈ elts A"
      using countableE_infinite [OF that]     
      by (simp add: eqpoll_def ω_def) 
         (meson bij_betw_def bij_betw_inv bij_betw_trans inj_ord_of_nat)
    then show ?thesis
      using Card_ω Card_def cardinal_cong vcard_def by auto
  qed
  show "countable (elts A)"
    if "vcard A ≤ Aleph 0"
  proof -
    have "elts A ≲ elts ω"
      using cardinal_le_lepoll [OF that] by simp
    then show ?thesis
      by (simp add: countable_iff_lepoll ω_def inj_ord_of_nat)
  qed
qed

lemma Aleph_csquare_eq [simp]: "ℵα ⊗ ℵα = ℵα"
  using InfCard_csquare_eq by auto

lemma vcard_Aleph [simp]: "vcard (ℵα) = ℵα"
  using Card_def InfCard_Aleph InfCard_def by auto

lemma omega_le_Aleph [simp]: "ω ≤ ℵα"
  using InfCard_def by auto

lemma finite_iff_less_Aleph0: "finite (elts x) ⟷ vcard x < ω"
proof
  show "finite (elts x) ⟹ vcard x < ω"
    by (metis Card_ω Card_def finite_lesspoll_infinite infinite_ω lesspoll_imp_Card_less)
  show "vcard x < ω ⟹ finite (elts x)"
    by (meson Ord_cardinal cardinal_eqpoll eqpoll_finite_iff infinite_Ord_omega less_le_not_le)
qed

lemma countable_iff_vcard_less1: "countable (elts x) ⟷ vcard x < ℵ1"
  by (simp add: countable_iff_le_Aleph0 lt_csucc_iff one_V_def)

lemma countable_infinite_vcard: "countable (elts x) ∧ infinite (elts x) ⟷ vcard x = ℵ0"
  by (metis Aleph_0 countable_iff_le_Aleph0 dual_order.refl finite_iff_less_Aleph0 less_V_def)

subsection ‹The ordinal @{term "ω1"}›

abbreviation "ω1 ≡ Aleph 1"

lemma Ord_ω1 [simp]: "Ord ω1"
  by (metis Ord_cardinal vcard_Aleph)

lemma omega_ω1 [iff]: "ω ∈ elts ω1"
  by (metis Aleph_0 mem_Aleph_succ one_V_def)

lemma ord_of_nat_ω1 [iff]: "ord_of_nat n ∈ elts ω1"
  using Ord_ω1 Ord_trans by blast

lemma countable_iff_less_ω1:
  assumes "Ord α"
  shows "countable (elts α) ⟷ α < ω1"
  by (simp add: assms countable_iff_le_Aleph0 lt_csucc_iff one_V_def)

lemma less_ω1_imp_countable:
  assumes "α ∈ elts ω1"
  shows "countable (elts α)"
  using Ord_ω1 Ord_in_Ord OrdmemD assms countable_iff_less_ω1 by blast

lemma ω1_gt0 [simp]: "ω1 > 0"
  using Ord_ω1 Ord_trans OrdmemD by blast

lemma ω1_gt1 [simp]: "ω1 > 1"
  using Ord_ω1 OrdmemD ω_gt1 less_trans by blast

lemma Limit_ω1 [simp]: "Limit ω1"
  by (simp add: InfCard_def InfCard_is_Limit le_csucc one_V_def)

end