# 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)"

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"   ("⟨_,/ _⟩")
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}}"

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"

lemma vsnd_conv [simp]: "vsnd ⟨a,b⟩ = b"

lemma vsplit [simp]: "vsplit c ⟨a,b⟩ = c a b"

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"

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)"

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"

lemma Inr_iff [iff]: "Inr a=Inr b ⟷ a=b"

lemma inj_on_Inl [simp]: "inj_on Inl A"

lemma inj_on_Inr [simp]: "inj_on Inr A"

lemma Inl_Inr_iff [iff]: "Inl a=Inr b ⟷ False"

lemma Inr_Inl_iff [iff]: "Inr b=Inl a ⟷ False"

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"

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"

lemma sum_case_Inr [simp]: "sum_case f g (Inr y) = g y"

lemma sum_case_non [simp]: "¬ is_sum a ⟹ sum_case f g a = undefined"

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"

lemma le_TC_refl [iff]: "x ⊑ x"

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"
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
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"]]
qed

lemma TC_rank_mem: "x ⊏ y ⟹ rank x ∈ elts (rank y)"

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)"

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"

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 β"

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"

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"

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 ⟷ α < β"

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)"

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

lemma ordermap: "wf r ⟹ ordermap A r a = set (ordermap A r ` {y ∈ A. (y,a) ∈ r})"
unfolding ordermap_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}))"
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"
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

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"

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"
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))"
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
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 ≤ ω"