# Theory ZFC_in_HOL

```section ‹The ZF Axioms, Ordinals and Transfinite Recursion›

theory ZFC_in_HOL
imports ZFC_Library

begin

subsection‹Syntax and axioms›

hide_const (open) list.set Sum subset

unbundle lattice_syntax

typedecl V

text‹Presentation refined by Dmitriy Traytel›
axiomatization elts :: "V ⇒ V set"
where ext [intro?]:    "elts x = elts y ⟹ x=y"
and down_raw:        "Y ⊆ elts x ⟹ Y ∈ range elts"
and Union_raw:       "X ∈ range elts ⟹ Union (elts ` X) ∈ range elts"
and Pow_raw:         "X ∈ range elts ⟹ inv elts ` Pow X ∈ range elts"
and replacement_raw: "X ∈ range elts ⟹ f ` X ∈ range elts"
and inf_raw:         "range (g :: nat ⇒ V) ∈ range elts"
and foundation:      "wf {(x,y). x ∈ elts y}"

lemma mem_not_refl [simp]: "i ∉ elts i"
using wf_not_refl [OF foundation] by force

lemma mem_not_sym: "¬ (x ∈ elts y ∧ y ∈ elts x)"
using wf_not_sym [OF foundation] by force

text ‹A set is small if it can be injected into the extension of a V-set.›
definition small :: "'a set ⇒ bool"
where "small X ≡ ∃V_of :: 'a ⇒ V. inj_on V_of X ∧ V_of ` X ∈ range elts"

lemma small_empty [iff]: "small {}"

lemma small_iff_range: "small X ⟷ X ∈ range elts"
by (metis inj_on_id2 replacement_raw the_inv_into_onto)

lemma small_eqpoll: "small A ⟷ (∃x. elts x ≈ A)"
unfolding small_def by (metis UNIV_I bij_betw_def eqpoll_def eqpoll_sym imageE image_eqI)

text‹Small classes can be mapped to sets.›
definition set :: "V set ⇒ V"
where "set X ≡ (if small X then inv elts X else inv elts {})"

lemma set_of_elts [simp]: "set (elts x) = x"
by (force simp add: ext set_def f_inv_into_f small_def)

lemma elts_of_set [simp]: "elts (set X) = (if small X then X else {})"
by (simp add: ZFC_in_HOL.set_def down_raw f_inv_into_f small_iff_range)

lemma down: "Y ⊆ elts x ⟹ small Y"

lemma Union [intro]: "small X ⟹ small (Union (elts ` X))"

lemma Pow: "small X ⟹ small (set ` Pow X)"
unfolding small_iff_range using Pow_raw set_def down by force

declare replacement_raw [intro,simp]

lemma replacement [intro,simp]:
assumes "small X"
shows "small (f ` X)"
proof -
let ?A = "inv_into X f ` (f ` X)"
have AX: "?A ⊆ X"
have inj: "inj_on f ?A"
have injo: "inj_on (inv_into X f) (f ` X)"
using inj_on_inv_into by blast
have "∃V_of. inj_on V_of (f ` X) ∧ V_of ` f ` X ∈ range elts"
if "inj_on V_of X" and "V_of ` X = elts x"
for V_of :: "'a ⇒ V" and x
proof (intro exI conjI)
show "inj_on (V_of ∘ inv_into X f) (f ` X)"
by (meson ‹inv_into X f ` f ` X ⊆ X› comp_inj_on inj_on_subset injo that)
have "(λx. V_of (inv_into X f (f x))) ` X = elts (set (V_of ` ?A))"
by (metis AX down elts_of_set image_image image_mono that(2))
then show "(V_of ∘ inv_into X f) ` f ` X ∈ range elts"
by (metis image_comp image_image rangeI)
qed
then show ?thesis
using assms by (auto simp: small_def)
qed

lemma small_image_iff [simp]: "inj_on f A ⟹ small (f ` A) ⟷ small A"
by (metis replacement the_inv_into_onto)

text ‹A little bootstrapping is needed to characterise @{term small} for sets of arbitrary type.›

lemma inf: "small (range (g :: nat ⇒ V))"

lemma small_image_nat_V [simp]: "small (g ` N)" for g :: "nat ⇒ V"
by (metis (mono_tags, opaque_lifting) down elts_of_set image_iff inf rangeI subsetI)

lemma Finite_V:
fixes X :: "V set"
assumes "finite X" shows "small X"
using ex_bij_betw_nat_finite [OF assms] unfolding bij_betw_def by (metis small_image_nat_V)

lemma small_insert_V:
fixes X :: "V set"
assumes "small X"
shows "small (insert a X)"
proof (cases "finite X")
case True
then show ?thesis
next
case False
show ?thesis
using infinite_imp_bij_betw2 [OF False]
by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral)
qed

lemma small_UN_V [simp,intro]:
fixes B :: "'a ⇒ V set"
assumes X: "small X" and B: "⋀x. x ∈ X ⟹ small (B x)"
shows "small (⋃x∈X. B x)"
proof -
have "(⋃ (elts ` (λx. ZFC_in_HOL.set (B x)) ` X)) = (⋃ (B ` X))"
using B by force
then show ?thesis
using Union [OF replacement [OF X, of "λx. ZFC_in_HOL.set (B x)"]] by simp
qed

definition vinsert where "vinsert x y ≡ set (insert x (elts y))"

lemma elts_vinsert [simp]: "elts (vinsert x y) = insert x (elts y)"
using down small_insert_V vinsert_def by auto

definition succ where "succ x ≡ vinsert x x"

lemma elts_succ [simp]: "elts (succ x) = insert x (elts x)"

lemma finite_imp_small:
assumes "finite X" shows "small X"
using assms
proof induction
case empty
then show ?case
by simp
next
case (insert a X)
then obtain V_of u where u: "inj_on V_of X" "V_of ` X = elts u"
by (meson small_def image_iff)
show ?case
unfolding small_def
proof (intro exI conjI)
show "inj_on (V_of(a:=u)) (insert a X)"
using u
by (metis image_eqI mem_not_refl)
have "(V_of(a:=u)) ` insert a X = elts (vinsert u u)"
using insert.hyps(2) u(2) by auto
then show "(V_of(a:=u)) ` insert a X ∈ range elts"
by (blast intro:  elim: )
qed
qed

lemma small_insert:
assumes "small X"
shows "small (insert a X)"
proof (cases "finite X")
case True
then show ?thesis
next
case False
show ?thesis
using infinite_imp_bij_betw2 [OF False]
by (metis replacement Un_insert_right assms bij_betw_imp_surj_on sup_bot.right_neutral)
qed

lemma smaller_than_small:
assumes "small A" "B ⊆ A" shows "small B"
using assms
by (metis down elts_of_set image_mono small_def small_iff_range subset_inj_on)

lemma small_insert_iff [iff]: "small (insert a X) ⟷ small X"
by (meson small_insert smaller_than_small subset_insertI)

lemma small_iff: "small X ⟷ (∃x. X = elts x)"
by (metis down elts_of_set subset_refl)

lemma small_elts [iff]: "small (elts x)"
by (auto simp: small_iff)

lemma small_diff [iff]: "small (elts a - X)"
by (meson Diff_subset down)

lemma small_set [simp]: "small (list.set xs)"

lemma small_upair: "small {x,y}"
by simp

lemma small_Un_elts: "small (elts x ∪ elts y)"
using Union [OF small_upair] by auto

lemma small_eqcong: "⟦small X; X ≈ Y⟧ ⟹ small Y"
by (metis bij_betw_imp_surj_on eqpoll_def replacement)

lemma lepoll_small: "⟦small Y; X ≲ Y⟧ ⟹ small X"
by (meson lepoll_iff replacement smaller_than_small)

lemma big_UNIV [simp]: "¬ small (UNIV::V set)" (is  "¬ small ?U")
proof
assume "small ?U"
then have "small A" for A :: "V set"
by (metis (full_types) UNIV_I down small_iff subsetI)
then have "range elts = UNIV"
by (meson small_iff surj_def)
then show False
by (metis Cantors_theorem Pow_UNIV)
qed

lemma inj_on_set: "inj_on set (Collect small)"
by (metis elts_of_set inj_onI mem_Collect_eq)

lemma set_injective [simp]: "⟦small X; small Y⟧ ⟹ set X = set Y ⟷ X=Y"
by (metis elts_of_set)

subsection‹Type classes and other basic setup›

instantiation V :: zero
begin
definition zero_V where "0 ≡ set {}"
instance ..
end

lemma elts_0 [simp]: "elts 0 = {}"

lemma set_empty [simp]: "set {} = 0"

instantiation V :: one
begin
definition one_V where "1 ≡ succ 0"
instance ..
end

lemma elts_1 [simp]: "elts 1 = {0}"

lemma insert_neq_0 [simp]: "set (insert a X) = 0 ⟷ ¬ small X"
unfolding zero_V_def
by (metis elts_of_set empty_not_insert set_of_elts small_insert_iff)

lemma elts_eq_empty_iff [simp]: "elts x = {} ⟷ x=0"
by (auto simp: ZFC_in_HOL.ext)

instantiation V :: distrib_lattice
begin

definition inf_V where "inf_V x y ≡ set (elts x ∩ elts y)"

definition sup_V where "sup_V x y ≡ set (elts x ∪ elts y)"

definition less_eq_V where "less_eq_V x y ≡ elts x ⊆ elts y"

definition less_V where "less_V x y ≡ less_eq x y ∧ x ≠ (y::V)"

instance
proof
show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" for x :: V and y :: V
using ext less_V_def less_eq_V_def by auto
show "x ≤ x" for x :: V
show "x ≤ z" if "x ≤ y" "y ≤ z" for x y z :: V
using that by (auto simp: less_eq_V_def)
show "x = y" if "x ≤ y" "y ≤ x" for x y :: V
using that by (simp add: ext less_eq_V_def)
show "inf x y ≤ x" for x y :: V
by (metis down elts_of_set inf_V_def inf_sup_ord(1) less_eq_V_def)
show "inf x y ≤ y" for x y :: V
by (metis Int_lower2 down elts_of_set inf_V_def less_eq_V_def)
show "x ≤ inf y z" if "x ≤ y" "x ≤ z" for x y z :: V
proof -
have "small (elts y ∩ elts z)"
by (meson down inf.cobounded1)
then show ?thesis
using elts_of_set inf_V_def less_eq_V_def that by auto
qed
show "x ≤ x ⊔ y" "y ≤ x ⊔ y" for x y :: V
by (simp_all add: less_eq_V_def small_Un_elts sup_V_def)
show "sup y z ≤ x" if "y ≤ x" "z ≤ x" for x y z :: V
using less_eq_V_def sup_V_def that by auto
show "sup x (inf y z) = inf (x ⊔ y) (sup x z)" for x y z :: V
proof -
have "small (elts y ∩ elts z)"
by (meson down inf.cobounded2)
then show ?thesis
by (simp add: Un_Int_distrib inf_V_def small_Un_elts sup_V_def)
qed
qed
end

lemma V_equalityI [intro]: "(⋀x. x ∈ elts a ⟷ x ∈ elts b) ⟹ a = b"
by (meson dual_order.antisym less_eq_V_def subsetI)

lemma vsubsetI [intro!]: "(⋀x. x ∈ elts a ⟹ x ∈ elts b) ⟹ a ≤ b"

lemma vsubsetD [elim, intro?]: "a ≤ b ⟹ c ∈ elts a ⟹ c ∈ elts b"
using less_eq_V_def by auto

lemma rev_vsubsetD: "c ∈ elts a ⟹ a ≤ b ⟹ c ∈ elts b"
― ‹The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.›
by (rule vsubsetD)

lemma vsubsetCE [elim,no_atp]: "a ≤ b ⟹ (c ∉ elts a ⟹ P) ⟹ (c ∈ elts b ⟹ P) ⟹ P"
― ‹Classical elimination rule.›
using vsubsetD by blast

lemma set_image_le_iff: "small A ⟹ set (f ` A) ≤ B ⟷ (∀x∈A. f x ∈ elts B)"
by auto

lemma eq0_iff: "x = 0 ⟷ (∀y. y ∉ elts x)"
by auto

lemma less_eq_V_0_iff [simp]: "x ≤ 0 ⟷ x = 0" for x::V
by auto

lemma subset_iff_less_eq_V:
assumes "small B" shows "A ⊆ B ⟷ set A ≤ set B ∧ small A"
using assms down small_iff by auto

lemma small_Collect [simp]: "small A ⟹ small {x ∈ A. P x}"

lemma small_Union_iff: "small (⋃(elts ` X)) ⟷ small X"
proof
show "small X"
if "small (⋃ (elts ` X))"
proof -
have "X ⊆ set ` Pow (⋃ (elts ` X))"
by fastforce
then show ?thesis
using Pow subset_iff_less_eq_V that by auto
qed
qed auto

lemma not_less_0 [iff]:
fixes x::V shows "¬ x < 0"

lemma le_0 [iff]:
fixes x::V shows "0 ≤ x"
by auto

lemma min_0L [simp]: "min 0 n = 0" for n :: V

lemma min_0R [simp]: "min n 0 = 0" for n :: V

lemma neq0_conv: "⋀n::V. n ≠ 0 ⟷ 0 < n"

definition VPow :: "V ⇒ V"
where "VPow x ≡ set (set ` Pow (elts x))"

lemma VPow_iff [iff]: "y ∈ elts (VPow x) ⟷ y ≤ x"
using down Pow
apply (auto simp: VPow_def less_eq_V_def)
using less_eq_V_def apply fastforce
done

lemma VPow_le_VPow_iff [simp]: "VPow a ≤ VPow b ⟷ a ≤ b"
by auto

lemma elts_VPow: "elts (VPow x) = set ` Pow (elts x)"
by (auto simp: VPow_def Pow)

lemma small_sup_iff [simp]: "small (X ∪ Y) ⟷ small X ∧ small Y" for X::"V set"
by (metis down elts_of_set small_Un_elts sup_ge1 sup_ge2)

lemma elts_sup_iff [simp]: "elts (x ⊔ y) = elts x ∪ elts y"

assumes z: "z ≠ 0" shows "∃w. w ∈ elts z ∧ w ⊓ z = 0"
using foundation assms
by (simp add: wf_eq_minimal) (metis Int_emptyI equals0I inf_V_def set_of_elts zero_V_def)

instantiation "V" :: Sup
begin
definition Sup_V where "Sup_V X ≡ if small X then set (Union (elts ` X)) else 0"
instance ..
end

instantiation "V" :: Inf
begin
definition Inf_V where "Inf_V X ≡ if X = {} then 0 else set (Inter (elts ` X))"
instance ..
end

lemma V_disjoint_iff: "x ⊓ y = 0 ⟷ elts x ∩ elts y = {}"
by (metis down elts_of_set inf_V_def inf_le1 zero_V_def)

text‹I've no idea why @{term bdd_above} is treated differently from @{term bdd_below}, but anyway›
lemma bdd_above_iff_small [simp]: "bdd_above X = small X" for X::"V set"
proof
show "small X" if "bdd_above X"
proof -
obtain a where "∀x∈X. x ≤ a"
using that ‹bdd_above X› bdd_above_def by blast
then show "small X"
by (meson VPow_iff ‹∀x∈X. x ≤ a› down subsetI)
qed
show "bdd_above X"
if "small X"
proof -
have "∀x∈X. x ≤ ⨆ X"
by (simp add: SUP_upper Sup_V_def Union less_eq_V_def that)
then show ?thesis
by (meson bdd_above_def)
qed
qed

instantiation "V" :: conditionally_complete_lattice
begin

definition bdd_below_V where "bdd_below_V X ≡ X ≠ {}"

instance
proof
show "⨅ X ≤ x" if "x ∈ X" "bdd_below X"
for x :: V and X :: "V set"
using that by (auto simp: bdd_below_V_def Inf_V_def split: if_split_asm)
show "z ≤ ⨅ X"
if "X ≠ {}" "⋀x. x ∈ X ⟹ z ≤ x"
for X :: "V set" and z :: V
using that
apply (clarsimp simp add: bdd_below_V_def Inf_V_def less_eq_V_def split: if_split_asm)
by (meson INT_subset_iff down eq_refl equals0I)
show "x ≤ ⨆ X" if "x ∈ X" and "bdd_above X" for x :: V and X :: "V set"
using that Sup_V_def by auto
show "⨆ X ≤ (z::V)" if "X ≠ {}" "⋀x. x ∈ X ⟹ x ≤ z" for X :: "V set" and z :: V
using that  by (simp add: SUP_least Sup_V_def less_eq_V_def)
qed
end

lemma Sup_upper: "⟦x ∈ A; small A⟧ ⟹ x ≤ ⨆A" for A::"V set"
by (auto simp: Sup_V_def SUP_upper Union less_eq_V_def)

lemma Sup_least:
fixes z::V shows "(⋀x. x ∈ A ⟹ x ≤ z) ⟹ ⨆A ≤ z"
by (auto simp: Sup_V_def SUP_least less_eq_V_def)

lemma Sup_empty [simp]: "⨆{} = (0::V)"
using Sup_V_def by auto

lemma elts_Sup [simp]: "small X ⟹ elts (⨆ X) = ⋃(elts ` X)"
by (auto simp: Sup_V_def)

lemma sup_V_0_left [simp]: "0 ⊔ a = a" and sup_V_0_right [simp]: "a ⊔ 0 = a" for a::V
by auto

lemma Sup_V_insert:
fixes x::V assumes "small A" shows "⨆(insert x A) = x ⊔ ⨆A"

lemma Sup_Un_distrib: "⟦small A; small B⟧ ⟹ ⨆(A ∪ B) = ⨆A ⊔ ⨆B" for A::"V set"
by auto

lemma SUP_sup_distrib:
fixes f :: "V ⇒ V"
shows "small A ⟹ (⨆x∈A. f x ⊔ g x) = ⨆ (f ` A) ⊔ ⨆ (g ` A)"
by (force simp:)

lemma SUP_const [simp]: "(⨆y ∈ A. a) = (if A = {} then (0::V) else a)"
by simp

lemma cSUP_subset_mono:
fixes f :: "'a ⇒ V set" and g :: "'a ⇒ V set"
shows "⟦A ⊆ B; ⋀x. x ∈ A ⟹ f x ≤ g x⟧ ⟹ ⨆ (f ` A) ≤ ⨆ (g ` B)"

lemma mem_Sup_iff [iff]: "x ∈ elts (⨆X) ⟷ x ∈ ⋃ (elts ` X) ∧ small X"
using Sup_V_def by auto

lemma cSUP_UNION:
fixes B :: "V ⇒ V set" and f :: "V ⇒ V"
assumes ne: "small A" and bdd_UN: "small (⋃x∈A. f ` B x)"
shows "⨆(f ` (⋃x∈A. B x)) = ⨆((λx. ⨆(f ` B x)) ` A)"
proof -
have bdd: "⋀x. x ∈ A ⟹ small (f ` B x)"
using bdd_UN subset_iff_less_eq_V
by (meson SUP_upper smaller_than_small)
then have bdd2: "small ((λx. ⨆(f ` B x)) ` A)"
using ne(1) by blast
have "⨆(f ` (⋃x∈A. B x)) ≤ ⨆((λx. ⨆(f ` B x)) ` A)"
using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd)
moreover have "⨆((λx. ⨆(f ` B x)) ` A) ≤ ⨆(f ` (⋃x∈A. B x))"
using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN)
ultimately show ?thesis
by (rule order_antisym)
qed

lemma Sup_subset_mono: "small B ⟹ A ⊆ B ⟹ Sup A ≤ Sup B" for A::"V set"
by auto

lemma Sup_le_iff: "small A ⟹ Sup A ≤ a ⟷ (∀x∈A. x ≤ a)" for A::"V set"
by auto

lemma SUP_le_iff: "small (f ` A) ⟹ ⨆(f ` A) ≤ u ⟷ (∀x∈A. f x ≤ u)" for f :: "V ⇒ V"
by blast

lemma Sup_eq_0_iff [simp]: "⨆A = 0 ⟷ A ⊆ {0} ∨ ¬ small A" for A :: "V set"
using Sup_upper by fastforce

lemma Sup_Union_commute:
fixes f :: "V ⇒ V set"
assumes "small A" "⋀x. x∈A ⟹ small (f x)"
shows "⨆ (⋃x∈A. f x) = (⨆x∈A. ⨆ (f x))"
using assms
by (force simp: subset_iff_less_eq_V intro!: antisym)

lemma Sup_eq_Sup:
fixes B :: "V set"
assumes "B ⊆ A" "small A" and *: "⋀x. x ∈ A ⟹ ∃y ∈ B. x ≤ y"
shows "Sup A = Sup B"
proof -
have "small B"
using assms subset_iff_less_eq_V by auto
moreover have "∃y∈B. u ∈ elts y"
if "x ∈ A" "u ∈ elts x" for u x
using that "*" by blast
moreover have "∃x∈A. v ∈ elts x"
if "y ∈ B" "v ∈ elts y" for v y
using that ‹B ⊆ A› by blast
ultimately show ?thesis
using assms by auto
qed

subsection‹Successor function›

lemma vinsert_not_empty [simp]: "vinsert a A ≠ 0"
and empty_not_vinsert [simp]: "0 ≠ vinsert a A"
by (auto simp: vinsert_def)

lemma succ_not_0 [simp]: "succ n ≠ 0" and zero_not_succ [simp]: "0 ≠ succ n"
by (auto simp: succ_def)

instantiation V :: zero_neq_one
begin
instance
by intro_classes (metis elts_0 elts_succ empty_iff insert_iff one_V_def set_of_elts)
end

instantiation V :: zero_less_one
begin
instance
end

lemma succ_ne_self [simp]: "i ≠ succ i"
by (metis elts_succ insertI1 mem_not_refl)

lemma succ_notin_self: "succ i ∉ elts i"
using elts_succ mem_not_refl by blast

lemma le_succE: "succ i ≤ succ j ⟹ i ≤ j"
using less_eq_V_def mem_not_sym by auto

lemma succ_inject_iff [iff]: "succ i = succ j ⟷ i = j"

lemma inj_succ: "inj succ"

lemma succ_neq_zero: "succ x ≠ 0"
by (metis elts_0 elts_succ insert_not_empty)

definition pred where "pred i ≡ THE j. i = succ j"

lemma pred_succ [simp]: "pred (succ i) = i"

subsection ‹Ordinals›

definition Transset where "Transset x ≡ ∀y ∈ elts x. y ≤ x"

definition Ord where "Ord x ≡ Transset x ∧ (∀y ∈ elts x. Transset y)"

abbreviation ON where "ON ≡ Collect Ord"

subsubsection ‹Transitive sets›

lemma Transset_0 [iff]: "Transset 0"
by (auto simp: Transset_def)

lemma Transset_succ [intro]:
assumes "Transset x" shows "Transset (succ x)"
using assms
by (auto simp: Transset_def succ_def less_eq_V_def)

lemma Transset_Sup:
assumes "⋀x. x ∈ X ⟹ Transset x" shows "Transset (⨆X)"
proof (cases "small X")
case True
with assms show ?thesis
by (simp add: Transset_def) (meson Sup_upper assms dual_order.trans)

lemma Transset_sup:
assumes "Transset x" "Transset y" shows "Transset (x ⊔ y)"
using Transset_def assms by fastforce

lemma Transset_inf: "⟦Transset i; Transset j⟧ ⟹ Transset (i ⊓ j)"

lemma Transset_VPow: "Transset(i) ⟹ Transset(VPow(i))"
by (auto simp: Transset_def)

lemma Transset_Inf: "(⋀i. i ∈ A ⟹ Transset i) ⟹ Transset (⨅ A)"
by (force simp: Transset_def Inf_V_def)

lemma Transset_SUP: "(⋀x. x ∈ A ⟹ Transset (B x)) ⟹ Transset (⨆ (B ` A))"
by (metis Transset_Sup imageE)

lemma Transset_INT: "(⋀x. x ∈ A ⟹ Transset (B x)) ⟹ Transset (⨅ (B ` A))"
by (metis Transset_Inf imageE)

subsubsection ‹Zero, successor, sups›

lemma Ord_0 [iff]: "Ord 0"
by (auto simp: Ord_def)

lemma Ord_succ [intro]:
assumes "Ord x" shows "Ord (succ x)"
using assms by (auto simp: Ord_def)

lemma Ord_Sup:
assumes "⋀x. x ∈ X ⟹ Ord x" shows "Ord (⨆X)"
proof (cases "small X")
case True
with assms show ?thesis
by (auto simp: Ord_def Transset_Sup)

lemma Ord_Union:
assumes "⋀x. x ∈ X ⟹ Ord x" "small X" shows "Ord (set (⋃ (elts ` X)))"
by (metis Ord_Sup Sup_V_def assms)

lemma Ord_sup:
assumes "Ord x" "Ord y" shows "Ord (x ⊔ y)"
using assms
proof (clarsimp simp: Ord_def)
show "Transset (x ⊔ y) ∧ (∀y∈elts x ∪ elts y. Transset y)"
if "Transset x" "Transset y" "∀y∈elts x. Transset y" "∀y∈elts y. Transset y"
using Ord_def Transset_sup assms by auto
qed

lemma big_ON [simp]: "¬ small ON"
proof
assume "small ON"
then have "set ON ∈ ON"
by (metis Ord_Union Ord_succ Sup_upper elts_Sup elts_succ insertI1 mem_Collect_eq mem_not_refl set_of_elts vsubsetD)
then show False
by (metis ‹small ON› elts_of_set mem_not_refl)
qed

lemma Ord_1 [iff]: "Ord 1"
using Ord_succ one_V_def succ_def vinsert_def by fastforce

lemma OrdmemD: "Ord k ⟹ j ∈ elts k ⟹ j < k"
using Ord_def Transset_def less_V_def by auto

lemma Ord_trans: "⟦ i ∈ elts j;  j ∈ elts k;  Ord k ⟧  ⟹ i ∈ elts k"
using Ord_def Transset_def by blast

lemma mem_0_Ord:
assumes k: "Ord k" and knz: "k ≠ 0" shows "0 ∈ elts k"
by (metis Ord_def Transset_def inf.orderE k knz trad_foundation)

lemma Ord_in_Ord: "⟦ Ord k;  m ∈ elts k ⟧  ⟹ Ord m"
using Ord_def Ord_trans by blast

lemma OrdI: "⟦Transset i; ⋀x. x ∈ elts i ⟹ Transset x⟧ ⟹ Ord i"

lemma Ord_is_Transset: "Ord i ⟹ Transset i"

lemma Ord_contains_Transset: "⟦Ord i; j ∈ elts i⟧ ⟹ Transset j"
using Ord_def by blast

lemma ON_imp_Ord:
assumes "H ⊆ ON" "x ∈ H"
shows "Ord x"
using assms by blast

lemma elts_subset_ON: "Ord α ⟹ elts α ⊆ ON"
using Ord_in_Ord by blast

lemma Transset_pred [simp]: "Transset x ⟹ ⨆(elts (succ x)) = x"
by (fastforce simp: Transset_def)

lemma Ord_pred [simp]: "Ord β ⟹ ⨆ (insert β (elts β)) = β"
using Ord_def Transset_pred by auto

subsubsection ‹Induction, Linearity, etc.›

lemma Ord_induct [consumes 1, case_names step]:
assumes k: "Ord k"
and step: "⋀x.⟦ Ord x; ⋀y. y ∈ elts x ⟹ P y ⟧  ⟹ P x"
shows "P k"
using foundation k
proof (induction k rule: wf_induct_rule)
case (less x)
then show ?case
using Ord_in_Ord local.step by auto
qed

text ‹Comparability of ordinals›
lemma Ord_linear: "Ord k ⟹ Ord l ⟹ k ∈ elts l ∨ k=l ∨ l ∈ elts k"
proof (induct k arbitrary: l rule: Ord_induct)
case (step k)
note step_k = step
show ?case using ‹Ord l›
proof (induct l rule: Ord_induct)
case (step l)
thus ?case using step_k
by (metis Ord_trans V_equalityI)
qed
qed

text ‹The trichotomy law for ordinals›
lemma Ord_linear_lt:
assumes "Ord k" "Ord l"
obtains (lt) "k < l" | (eq) "k=l" | (gt) "l < k"
using Ord_linear OrdmemD assms by blast

lemma Ord_linear2:
assumes "Ord k" "Ord l"
obtains (lt) "k < l" | (ge) "l ≤ k"
by (metis Ord_linear_lt eq_refl assms order.strict_implies_order)

lemma Ord_linear_le:
assumes "Ord k" "Ord l"
obtains (le) "k ≤ l" | (ge) "l ≤ k"
by (meson Ord_linear2 le_less assms)

lemma union_less_iff [simp]: "⟦Ord i; Ord j⟧ ⟹ i ⊔ j < k ⟷ i<k ∧ j<k"
by (metis Ord_linear_le le_iff_sup sup.order_iff sup.strict_boundedE)

lemma Ord_mem_iff_lt: "Ord k ⟹ Ord l ⟹ k ∈ elts l ⟷ k < l"
by (metis Ord_linear OrdmemD less_le_not_le)

lemma Ord_Collect_lt: "Ord α ⟹ {ξ. Ord ξ ∧ ξ < α} = elts α"
by (auto simp flip: Ord_mem_iff_lt elim: Ord_in_Ord OrdmemD)

lemma Ord_not_less: "⟦Ord x; Ord y⟧ ⟹ ¬ x < y ⟷ y ≤ x"
by (metis (no_types) Ord_linear2 leD)

lemma Ord_not_le: "⟦Ord x; Ord y⟧ ⟹ ¬ x ≤ y ⟷ y < x"
by (metis (no_types) Ord_linear2 leD)

lemma le_succ_iff: "Ord i ⟹ Ord j ⟹ succ i ≤ succ j ⟷ i ≤ j"
by (metis Ord_linear_le Ord_succ le_succE order_antisym)

lemma succ_le_iff: "Ord i ⟹ Ord j ⟹ succ i ≤ j ⟷ i < j"
using Ord_mem_iff_lt dual_order.strict_implies_order less_eq_V_def by fastforce

lemma succ_in_Sup_Ord:
assumes eq: "succ β = ⨆A" and "small A" "A ⊆ ON" "Ord β"
shows "succ β ∈ A"
proof -
have "¬ ⨆A ≤ β"
using eq ‹Ord β› succ_le_iff by fastforce
then show ?thesis
using assms by (metis Ord_linear2 Sup_least Sup_upper eq_iff mem_Collect_eq subsetD succ_le_iff)
qed

lemma in_succ_iff: "Ord i ⟹ j ∈ elts (ZFC_in_HOL.succ i) ⟷ Ord j ∧ j ≤ i"
by (metis Ord_in_Ord Ord_mem_iff_lt Ord_not_le Ord_succ succ_le_iff)

lemma zero_in_succ [simp,intro]: "Ord i ⟹ 0 ∈ elts (succ i)"
using mem_0_Ord by auto

lemma less_succ_self: "x < succ x"
by (simp add: less_eq_V_def order_neq_le_trans subset_insertI)

lemma Ord_finite_Sup: "⟦finite A; A ⊆ ON; A ≠ {}⟧ ⟹ ⨆A ∈ A"
proof (induction A rule: finite_induct)
case (insert x A)
then have *: "small A" "A ⊆ ON" "Ord x"
by (auto simp add: ZFC_in_HOL.finite_imp_small insert.hyps)
show ?case
proof (cases "A = {}")
case False
then have "⨆A ∈ A"
using insert by blast
then have "⨆A ≤ x" if "x ⊔ ⨆A ∉ A"
using * by (metis ON_imp_Ord Ord_linear_le sup.absorb2 that)
then show ?thesis
by (fastforce simp: ‹small A› Sup_V_insert)
qed auto
qed auto

subsubsection ‹The natural numbers›

primrec ord_of_nat :: "nat ⇒ V" where
"ord_of_nat 0 = 0"
| "ord_of_nat (Suc n) = succ (ord_of_nat n)"

lemma ord_of_nat_eq_initial: "ord_of_nat n = set (ord_of_nat ` {..<n})"
by (induction n) (auto simp: lessThan_Suc succ_def)

lemma mem_ord_of_nat_iff [simp]: "x ∈ elts (ord_of_nat n) ⟷ (∃m<n. x = ord_of_nat m)"
by (subst ord_of_nat_eq_initial) auto

lemma elts_ord_of_nat: "elts (ord_of_nat k) = ord_of_nat ` {..<k}"
by auto

lemma Ord_equality: "Ord i ⟹ i = ⨆ (succ ` elts i)"
by (force intro: Ord_trans)

lemma Ord_ord_of_nat [simp]: "Ord (ord_of_nat k)"
by (induct k, auto)

lemma ord_of_nat_equality: "ord_of_nat n = ⨆ ((succ ∘ ord_of_nat) ` {..<n})"
by (metis Ord_equality Ord_ord_of_nat elts_of_set image_comp small_image_nat_V ord_of_nat_eq_initial)

definition ω :: V where "ω ≡ set (range ord_of_nat)"

lemma elts_ω: "elts ω = {α. ∃n. α = ord_of_nat n}"
by (auto simp: ω_def image_iff)

lemma nat_into_Ord [simp]: "n ∈ elts ω ⟹ Ord n"
by (metis Ord_ord_of_nat ω_def elts_of_set image_iff inf)

lemma Sup_ω: "⨆(elts ω) = ω"
unfolding ω_def by force

lemma Ord_ω [iff]: "Ord ω"
by (metis Ord_Sup Sup_ω nat_into_Ord)

lemma zero_in_omega [iff]: "0 ∈ elts ω"
by (metis ω_def elts_of_set inf ord_of_nat.simps(1) rangeI)

lemma succ_in_omega [simp]: "n ∈ elts ω ⟹ succ n ∈ elts ω"
by (metis ω_def elts_of_set image_iff small_image_nat_V ord_of_nat.simps(2) rangeI)

lemma ord_of_eq_0: "ord_of_nat j = 0 ⟹ j = 0"
by (induct j) (auto simp: succ_neq_zero)

lemma ord_of_nat_le_omega: "ord_of_nat n ≤ ω"
by (metis Sup_ω ZFC_in_HOL.Sup_upper ω_def elts_of_set inf rangeI)

lemma ord_of_eq_0_iff [simp]: "ord_of_nat n = 0 ⟷ n=0"
by (auto simp: ord_of_eq_0)

lemma ord_of_nat_inject [iff]: "ord_of_nat i = ord_of_nat j ⟷ i=j"
proof (induct i arbitrary: j)
case 0 show ?case
using ord_of_eq_0 by auto
next
case (Suc i) then show ?case
by auto (metis elts_0 elts_succ insert_not_empty not0_implies_Suc ord_of_nat.simps succ_inject_iff)
qed

corollary inj_ord_of_nat: "inj ord_of_nat"

corollary countable:
assumes "countable X" shows "small X"
proof -
have "X ⊆ range (from_nat_into X)"
then show ?thesis
by (meson inf_raw inj_ord_of_nat replacement small_def smaller_than_small)
qed

corollary infinite_ω: "infinite (elts ω)"
using range_inj_infinite [of ord_of_nat]

corollary ord_of_nat_mono_iff [iff]: "ord_of_nat i ≤ ord_of_nat j ⟷ i ≤ j"
by (metis Ord_def Ord_ord_of_nat Transset_def eq_iff mem_ord_of_nat_iff not_less ord_of_nat_inject)

corollary ord_of_nat_strict_mono_iff [iff]: "ord_of_nat i < ord_of_nat j ⟷ i < j"

lemma small_image_nat [simp]:
fixes N :: "nat set" shows "small (g ` N)"

lemma finite_Ord_omega: "α ∈ elts ω ⟹ finite (elts α)"
show "finite (elts (ord_of_nat n))" if "α = ord_of_nat n" for n
using that by (simp add: ord_of_nat_eq_initial [of n])
qed

lemma infinite_Ord_omega: "Ord α ⟹ infinite (elts α) ⟹ ω ≤ α"
by (meson Ord_ω Ord_linear2 Ord_mem_iff_lt finite_Ord_omega)

lemma ord_of_minus_1: "n > 0 ⟹ ord_of_nat n = succ (ord_of_nat (n - 1))"
by (metis Suc_diff_1 ord_of_nat.simps(2))

lemma card_ord_of_nat [simp]: "card (elts (ord_of_nat m)) = m"
by (induction m) (auto simp: ω_def finite_Ord_omega)

lemma ord_of_nat_ω [iff]:"ord_of_nat n ∈ elts ω"

lemma succ_ω_iff [iff]: "succ n ∈ elts ω ⟷ n ∈ elts ω"
by (metis Ord_ω OrdmemD elts_vinsert insert_iff less_V_def succ_def succ_in_omega vsubsetD)

lemma ω_gt0 [simp]: "ω > 0"

lemma ω_gt1 [simp]: "ω > 1"

subsubsection‹Limit ordinals›

definition Limit :: "V⇒bool"
where "Limit i ≡ Ord i ∧ 0 ∈ elts i ∧ (∀y. y ∈ elts i ⟶ succ y ∈ elts i)"

lemma zero_not_Limit [iff]: "¬ Limit 0"

lemma not_succ_Limit [simp]: "¬ Limit(succ i)"
by (metis Limit_def Ord_mem_iff_lt elts_succ insertI1 less_irrefl)

lemma Limit_is_Ord: "Limit ξ ⟹ Ord ξ"

lemma succ_in_Limit_iff: "Limit ξ ⟹ succ α ∈ elts ξ ⟷ α ∈ elts ξ"
by (metis Limit_def OrdmemD elts_succ insertI1 less_V_def vsubsetD)

lemma Limit_eq_Sup_self [simp]: "Limit i ⟹ Sup (elts i) = i"
apply (rule order_antisym)
apply (simp add: Limit_def Ord_def Transset_def Sup_least)
by (metis Limit_def Ord_equality Sup_V_def SUP_le_iff Sup_upper small_elts)

lemma zero_less_Limit: "Limit β ⟹ 0 < β"

lemma non_Limit_ord_of_nat [iff]: "¬ Limit (ord_of_nat m)"
by (metis Limit_def mem_ord_of_nat_iff not_succ_Limit ord_of_eq_0_iff ord_of_minus_1)

lemma Limit_omega [iff]: "Limit ω"

lemma omega_nonzero [simp]: "ω ≠ 0"
using Limit_omega by fastforce

lemma Ord_cases_lemma:
assumes "Ord k" shows "k = 0 ∨ (∃j. k = succ j) ∨ Limit k"
proof (cases "Limit k")
case False
have "succ j ∈ elts k" if  "∀j. k ≠ succ j" "j ∈ elts k" for j
by (metis Ord_in_Ord Ord_linear Ord_succ assms elts_succ insertE mem_not_sym that)
with assms show ?thesis
by (auto simp: Limit_def mem_0_Ord)
qed auto

lemma Ord_cases [cases type: V, case_names 0 succ limit]:
assumes "Ord k"
obtains "k = 0" | l where "Ord l" "succ l = k" | "Limit k"
by (metis assms Ord_cases_lemma Ord_in_Ord elts_succ insertI1)

lemma non_succ_LimitI:
assumes "i≠0" "Ord(i)" "⋀y. succ(y) ≠ i"
shows "Limit(i)"
using Ord_cases_lemma assms by blast

lemma Ord_induct3 [consumes 1, case_names 0 succ Limit, induct type: V]:
assumes α: "Ord α"
and P: "P 0" "⋀α. ⟦Ord α; P α⟧ ⟹ P (succ α)"
"⋀α. ⟦Limit α; ⋀ξ. ξ ∈ elts α ⟹ P ξ⟧ ⟹ P (⨆ξ ∈ elts α. ξ)"
shows "P α"
using α
proof (induction α rule: Ord_induct)
case (step α)
then show ?case
by (metis Limit_eq_Sup_self Ord_cases P elts_succ image_ident insertI1)
qed

subsubsection‹Properties of LEAST for ordinals›

lemma
assumes "Ord k" "P k"
shows Ord_LeastI: "P (LEAST i. Ord i ∧ P i)" and Ord_Least_le: "(LEAST i. Ord i ∧ P i) ≤ k"
proof -
have "P (LEAST i. Ord i ∧ P i) ∧ (LEAST i. Ord i ∧ P i) ≤ k"
using assms
proof (induct k rule: Ord_induct)
case (step x) then have "P x" by simp
show ?case proof (rule classical)
assume assm: "¬ (P (LEAST a. Ord a ∧ P a) ∧ (LEAST a. Ord a ∧ P a) ≤ x)"
have "⋀y. Ord y ∧ P y ⟹ x ≤ y"
proof (rule classical)
fix y
assume y: "Ord y ∧ P y" "¬ x ≤ y"
with step obtain "P (LEAST a. Ord a ∧ P a)" and le: "(LEAST a. Ord a ∧ P a) ≤ y"
by (meson Ord_linear2 Ord_mem_iff_lt)
with assm have "x < (LEAST a. Ord a ∧ P a)"
by (meson Ord_linear_le y order.trans ‹Ord x›)
then show "x ≤ y"
using le by auto
qed
then have Least: "(LEAST a. Ord a ∧ P a) = x"
by (simp add: Least_equality ‹Ord x› step.prems)
with ‹P x› show ?thesis by simp
qed
qed
then show "P (LEAST i. Ord i ∧ P i)" and "(LEAST i. Ord i ∧ P i) ≤ k" by auto
qed

lemma Ord_Least:
assumes "Ord k" "P k"
shows "Ord (LEAST i. Ord i ∧ P i)"
proof -
have "Ord (LEAST i. Ord i ∧ (Ord i ∧ P i))"
using Ord_LeastI [where P = "λi. Ord i ∧ P i"] assms by blast
then show ?thesis
by simp
qed

― ‹The following 3 lemmas are due to Brian Huffman›
lemma Ord_LeastI_ex: "∃i. Ord i ∧ P i ⟹ P (LEAST i. Ord i ∧ P i)"
using Ord_LeastI by blast

lemma Ord_LeastI2:
"⟦Ord a; P a; ⋀x. ⟦Ord x; P x⟧ ⟹ Q x⟧ ⟹ Q (LEAST i. Ord i ∧ P i)"
by (blast intro: Ord_LeastI Ord_Least)

lemma Ord_LeastI2_ex:
"∃a. Ord a ∧ P a ⟹ (⋀x. ⟦Ord x; P x⟧ ⟹ Q x) ⟹ Q (LEAST i. Ord i ∧ P i)"
by (blast intro: Ord_LeastI_ex Ord_Least)

lemma Ord_LeastI2_wellorder:
assumes "Ord a" "P a"
and "⋀a. ⟦ P a; ∀b. Ord b ∧ P b ⟶ a ≤ b ⟧ ⟹ Q a"
shows "Q (LEAST i. Ord i ∧ P i)"
proof (rule LeastI2_order)
show "Ord (LEAST i. Ord i ∧ P i) ∧ P (LEAST i. Ord i ∧ P i)"
using Ord_Least Ord_LeastI assms by auto
next
fix y assume "Ord y ∧ P y" thus "(LEAST i. Ord i ∧ P i) ≤ y"
next
fix x assume "Ord x ∧ P x" "∀y. Ord y ∧ P y ⟶ x ≤ y" thus "Q x"
qed

lemma Ord_LeastI2_wellorder_ex:
assumes "∃x. Ord x ∧ P x"
and "⋀a. ⟦ P a; ∀b. Ord b ∧ P b ⟶ a ≤ b ⟧ ⟹ Q a"
shows "Q (LEAST i. Ord i ∧ P i)"
using assms by clarify (blast intro!: Ord_LeastI2_wellorder)

lemma not_less_Ord_Least: "⟦k < (LEAST x. Ord x ∧ P x); Ord k⟧ ⟹ ¬ P k"
using Ord_Least_le less_le_not_le by auto

lemma exists_Ord_Least_iff: "(∃α. Ord α ∧ P α) ⟷ (∃α. Ord α ∧ P α ∧ (∀β < α. Ord β ⟶ ¬ P β))" (is "?lhs ⟷ ?rhs")
proof
assume ?rhs thus ?lhs by blast
next
assume H: ?lhs then obtain α where α: "Ord α" "P α" by blast
let ?x = "LEAST α. Ord α ∧ P α"
have "Ord ?x"
by (metis Ord_Least α)
moreover
{ fix β assume m: "β < ?x" "Ord β"
from not_less_Ord_Least[OF m] have "¬ P β" . }
ultimately show ?rhs
using Ord_LeastI_ex[OF H] by blast
qed

lemma Ord_mono_imp_increasing:
assumes fun_hD: "h ∈ D → D"
and mono_h: "strict_mono_on D h"
and "D ⊆ ON" and ν: "ν ∈ D"
shows "ν ≤ h ν"
proof (rule ccontr)
assume non: "¬ ν ≤ h ν"
define μ where "μ ≡ LEAST μ. Ord μ ∧ ¬ μ ≤ h μ ∧ μ ∈ D"
have "Ord ν"
using ν ‹D ⊆ ON› by blast
then have μ: "¬ μ ≤ h μ ∧ μ ∈ D"
unfolding μ_def by (rule Ord_LeastI) (simp add: ν non)
have "Ord (h ν)"
using assms by auto
then have "Ord (h (h ν))"
by (meson ON_imp_Ord ν assms funcset_mem)
have "Ord μ"
using μ ‹D ⊆ ON› by blast
then have "h μ < μ"
by (metis ON_imp_Ord Ord_linear2 PiE μ ‹D ⊆ ON› fun_hD)
then have "¬ h μ ≤ h (h μ)"
using μ fun_hD mono_h by (force simp: strict_mono_on_def)
moreover have *: "h μ ∈ D"
using μ fun_hD by auto
moreover have "Ord (h μ)"
using ‹D ⊆ ON› * by blast
ultimately have "μ ≤ h μ"
then show False
using μ by blast
qed

lemma le_Sup_iff:
assumes "A ⊆ ON" "Ord x" "small A" shows "x ≤ ⨆A ⟷ (∀y ∈ ON. y<x ⟶ (∃a∈A. y < a))"
proof (intro iffI ballI impI)
show "∃a∈A. y < a"
if "x ≤ ⨆ A" "y ∈ ON" "y < x"
for y
proof -
have "¬ ⨆ A ≤ y" "Ord y"
using that by auto
then show ?thesis
by (metis Ord_linear2 Sup_least ‹A ⊆ ON› mem_Collect_eq subset_eq)
qed
show "x ≤ ⨆ A"
if "∀y∈ON. y < x ⟶ (∃a∈A. y < a)"
using that assms
by (metis Ord_Sup Ord_linear_le Sup_upper less_le_not_le mem_Collect_eq subsetD)
qed

lemma le_SUP_iff: "⟦f ` A ⊆ ON; Ord x; small A⟧ ⟹ x ≤ ⨆(f ` A) ⟷ (∀y ∈ ON. y<x ⟶ (∃i∈A. y < f i))"

subsection‹Transfinite Recursion and the V-levels›

definition transrec :: "((V ⇒ 'a) ⇒ V ⇒ 'a) ⇒ V ⇒ 'a"
where "transrec H a ≡ wfrec {(x,y). x ∈ elts y} H a"

lemma transrec: "transrec H a = H (λx ∈ elts a. transrec H x) a"
proof -
have "(cut (wfrec {(x, y). x ∈ elts y} H) {(x, y). x ∈ elts y} a)
= (λx∈elts a. wfrec {(x, y). x ∈ elts y} H x)"
by (force simp: cut_def)
then show ?thesis
unfolding transrec_def
qed

text‹Avoids explosions in proofs; resolve it with a meta-level definition›
lemma def_transrec:
"⟦⋀x. f x ≡ transrec H x⟧ ⟹ f a = H(λx ∈ elts a. f x) a"
by (metis restrict_ext transrec)

lemma eps_induct [case_names step]:
assumes "⋀x. (⋀y. y ∈ elts x ⟹ P y) ⟹ P x"
shows "P a"
using wf_induct [OF foundation] assms by auto

definition Vfrom :: "[V,V] ⇒ V"
where "Vfrom a ≡ transrec (λf x. a ⊔ ⨆((λy. VPow(f y)) ` elts x))"

abbreviation Vset :: "V ⇒ V" where "Vset ≡ Vfrom 0"

lemma Vfrom: "Vfrom a i = a ⊔ ⨆((λj. VPow(Vfrom a j)) ` elts i)"
apply (subst Vfrom_def)
apply (subst transrec)
using Vfrom_def by auto

lemma Vfrom_0 [simp]: "Vfrom a 0 = a"
by (subst Vfrom) auto

lemma Vset: "Vset i = ⨆((λj. VPow(Vset j)) ` elts i)"
by (subst Vfrom) auto

lemma Vfrom_mono1:
assumes "a ≤ b" shows "Vfrom a i ≤ Vfrom b i"
proof (induction i rule: eps_induct)
case (step i)
then have "a ⊔ (⨆j∈elts i. VPow (Vfrom a j)) ≤ b ⊔ (⨆j∈elts i. VPow (Vfrom b j))"
by (intro sup_mono cSUP_subset_mono ‹a ≤ b›) auto
then show ?case
by (metis Vfrom)
qed

lemma Vfrom_mono2: "Vfrom a i ≤ Vfrom a (i ⊔ j)"
proof (induction arbitrary: j rule: eps_induct)
case (step i)
then have "a ⊔ (⨆j∈elts i. VPow (Vfrom a j))
≤ a ⊔ (⨆j∈elts (i ⊔ j). VPow (Vfrom a j))"
by (intro sup_mono cSUP_subset_mono order_refl) auto
then show ?case
by (metis Vfrom)
qed

lemma Vfrom_mono: "⟦Ord i; a≤b; i≤j⟧ ⟹ Vfrom a i ≤ Vfrom b j"
by (metis (no_types) Vfrom_mono1 Vfrom_mono2 dual_order.trans sup.absorb_iff2)

lemma Transset_Vfrom: "Transset(A) ⟹ Transset(Vfrom A i)"
proof (induction i rule: eps_induct)
case (step i)
then show ?case
by (metis Transset_SUP Transset_VPow Transset_sup Vfrom)
qed

lemma Transset_Vset [simp]: "Transset(Vset i)"

lemma Vfrom_sup: "Vfrom a (i ⊔ j) = Vfrom a i ⊔ Vfrom a j"
proof (rule order_antisym)
show "Vfrom a (i ⊔ j) ≤ Vfrom a i ⊔ Vfrom a j"
by (simp add: Vfrom [of a "i ⊔ j"] Vfrom [of a i] Vfrom [of a j] Sup_Un_distrib image_Un sup.assoc sup.left_commute)
show "Vfrom a i ⊔ Vfrom a j ≤ Vfrom a (i ⊔ j)"
by (metis Vfrom_mono2 le_supI sup_commute)
qed

lemma Vfrom_succ_Ord:
assumes "Ord i" shows "Vfrom a (succ i) = a ⊔ VPow(Vfrom a i)"
proof (cases "i = 0")
case True
then show ?thesis
by (simp add: Vfrom [of _ "succ 0"])
next
case False
have *: "(⨆x∈elts i. VPow (Vfrom a x)) ≤ VPow (Vfrom a i)"
proof (rule cSup_least)
show "(λx. VPow (Vfrom a x)) ` elts i ≠ {}"
using False by auto
show "x ≤ VPow (Vfrom a i)" if "x ∈ (λx. VPow (Vfrom a x)) ` elts i" for x
using that
by clarsimp (meson Ord_in_Ord Ord_linear_le Vfrom_mono assms mem_not_refl order_refl vsubsetD)
qed
show ?thesis
proof (rule Vfrom [THEN trans])
show "a ⊔ (⨆j∈elts (succ i). VPow (Vfrom a j)) = a ⊔ VPow (Vfrom a i)"
using assms
by (intro sup_mono order_antisym) (auto simp: Sup_V_insert *)
qed
qed

lemma Vset_succ: "Ord i ⟹ Vset(succ(i)) = VPow(Vset(i))"

lemma Vfrom_Sup:
assumes "X ≠ {}" "small X"
shows "Vfrom a (Sup X) = (⨆y∈X. Vfrom a y)"
proof (rule order_antisym)
have "Vfrom a (⨆ X) = a ⊔ (⨆j∈elts (⨆ X). VPow (Vfrom a j))"
by (metis Vfrom)
also have "… ≤ ⨆ (Vfrom a ` X)"
proof -
have "a ≤ ⨆ (Vfrom a ` X)"
by (metis Vfrom all_not_in_conv assms bdd_above_iff_small cSUP_upper2 replacement sup_ge1)
moreover have "(⨆j∈elts (⨆ X). VPow (Vfrom a j)) ≤ ⨆ (Vfrom a ` X)"
proof -
have "VPow (Vfrom a x) ≤ ⨆ (Vfrom a ` X)"
if "y ∈ X" "x ∈ elts y" for x y
proof -
have "VPow (Vfrom a x) ≤ Vfrom a y"
by (metis Vfrom bdd_above_iff_small cSUP_upper2 le_supI2 order_refl replacement small_elts that(2))
also have "… ≤ ⨆ (Vfrom a ` X)"
using assms that by (force intro: cSUP_upper)
finally show ?thesis .
qed
then show ?thesis
by (simp add: SUP_le_iff ‹small X›)
qed
ultimately show ?thesis
by auto
qed
finally show "Vfrom a (⨆ X) ≤ ⨆ (Vfrom a ` X)" .
have "⋀x. x ∈ X ⟹
a ⊔ (⨆j∈elts x. VPow (Vfrom a j))
≤ a ⊔ (⨆j∈elts (⨆ X). VPow (Vfrom a j))"
using cSUP_subset_mono ‹small X› by auto
then show "⨆ (Vfrom a ` X) ≤ Vfrom a (⨆ X)"
by (metis Vfrom assms(1) cSUP_least)
qed

lemma Limit_Vfrom_eq:
"Limit(i) ⟹ Vfrom a i = (⨆y ∈ elts i. Vfrom a y)"
by (metis Limit_def Limit_eq_Sup_self Vfrom_Sup ex_in_conv small_elts)

end
```