Theory ZFC_in_HOL

section ‹The ZF Axioms, Ordinals and Transfinite Recursion›

theory ZFC_in_HOL
  imports ZFC_Library


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 {}"
  by (simp add: small_def down_raw)

lemma small_iff_range: "small X  X  range elts"
  apply (simp add: small_def)
  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"
  by (simp add: down_raw small_iff_range)

lemma Union [intro]: "small X  small (Union (elts ` X))"
  by (simp add: Union_raw small_iff_range)

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"
    by (simp add: image_subsetI inv_into_into)
  have inj: "inj_on f ?A"
    by (simp add: f_inv_into_f inj_on_def)
  have injo: "inj_on (inv_into X f) (f ` X)"
    using inj_on_inv_into by blast
  have "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)
  then show ?thesis
    using assms by (auto simp: small_def)

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))"
  by (simp add: inf_raw small_iff_range)

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
    by (simp add: Finite_V)
  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)

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 (xX. 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
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)"
  by (simp add: succ_def)

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

lemma small_insert:
  assumes "small X"
  shows "small (insert a X)"
proof (cases "finite X")
  case True
  then show ?thesis
    by (simp add: finite_imp_small)
  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)

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)"
  by (simp add: ZFC_in_HOL.finite_imp_small)

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

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
definition zero_V where "0  set {}"
instance ..

lemma elts_0 [simp]: "elts 0 = {}"
  by (simp add: zero_V_def)

lemma set_empty [simp]: "set {} = 0"
  by (simp add: zero_V_def)

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

lemma elts_1 [simp]: "elts 1 = {0}"
  by (simp add: one_V_def)

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

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

  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
    by (simp add: less_eq_V_def)
  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
  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)

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"
  by (simp add: less_eq_V_def subsetI)

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  (xA. 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}"
  by (simp add: smaller_than_small)

lemma small_Union_iff: "small ((elts ` X))  small X"
  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 auto

lemma not_less_0 [iff]:
  fixes x::V shows "¬ x < 0"
  by (simp add: less_eq_V_def less_le_not_le)

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

lemma min_0L [simp]: "min 0 n = 0" for n :: V
  by (simp add: min_absorb1)

lemma min_0R [simp]: "min n 0 = 0" for n :: V
  by (simp add: min_absorb2)

lemma neq0_conv: "n::V. n  0  0 < n"
  by (simp add: less_V_def)

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

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"
  by (simp add: sup_V_def)

lemma trad_foundation:
  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
definition Sup_V where "Sup_V X  if small X then set (Union (elts ` X)) else 0"
instance ..

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

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"
  show "small X" if "bdd_above X"
  proof -
    obtain a where "xX. x  a"
      using that bdd_above X bdd_above_def by blast
    then show "small X"
      by (meson VPow_iff xX. x  a down subsetI)
  show "bdd_above X"
    if "small X"
  proof -
    have "xX. x   X"
      by (simp add: SUP_upper Sup_V_def Union less_eq_V_def that)
    then show ?thesis
      by (meson bdd_above_def)

instantiation "V" :: conditionally_complete_lattice

definition bdd_below_V where "bdd_below_V X  X  {}"

  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)

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"
  by (simp add: assms cSup_insert_If)

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  (xA. 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)"
  by (simp add: SUP_subset_mono)

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 (xA. f ` B x)"
  shows "(f ` (xA. 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 ` (xA. 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 ` (xA. 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)

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  (xA. x  a)" for A::"V set"
  by auto

lemma SUP_le_iff: "small (f ` A)  (f ` A)  u  (xA. 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. xA  small (f x)"
  shows " (xA. f x) = (xA.  (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 "yB. u  elts y"
    if "x  A" "u  elts x" for u x
    using that "*" by blast
  moreover have "xA. 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

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
  by intro_classes (metis elts_0 elts_succ empty_iff insert_iff one_V_def set_of_elts)

instantiation V :: zero_less_one
  by intro_classes (simp add: less_V_def)

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"
  by (simp add: dual_order.antisym le_succE)

lemma inj_succ: "inj succ"
  by (simp add: inj_def)

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"
  by (simp add: pred_def)

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)
qed (simp add: Sup_V_def)

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)"
  by (simp add: Transset_def rev_vsubsetD)

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)
qed (simp add: Sup_V_def)

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)  (yelts x  elts y. Transset y)"
    if "Transset x" "Transset y" "yelts x. Transset y" "yelts y. Transset y"
    using Ord_def Transset_sup assms by auto

lemma big_ON [simp]: "¬ small ON"
  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)

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"
  by (simp add: Ord_def)

lemma Ord_is_Transset: "Ord i  Transset i"
  by (simp add: Ord_def)

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

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)

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)

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

corollary inj_ord_of_nat: "inj ord_of_nat"
  by (simp add: linorder_injI)

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

corollary infinite_ω: "infinite (elts ω)"
  using range_inj_infinite [of ord_of_nat]
  by (simp add: ω_def inj_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"
  by (simp add: less_le_not_le)

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

lemma finite_Ord_omega: "α  elts ω  finite (elts α)"
  proof (clarsimp simp add: ω_def)
  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])

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 ω"
  by (simp add: ω_def)

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"
  by (simp add: OrdmemD)

lemma ω_gt1 [simp]: "ω > 1"
  by (simp add: OrdmemD one_V_def)

subsubsection‹Limit ordinals›

definition Limit :: "Vbool"
  where "Limit i  Ord i  0  elts i  (y. y  elts i  succ y  elts i)"

lemma zero_not_Limit [iff]: "¬ Limit 0"
  by (simp add: Limit_def)

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 ξ"
  by (simp add: Limit_def)

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 < β"
  by (simp add: Limit_def OrdmemD)

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 ω"
  by (simp add: Limit_def)

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

subsubsection‹Properties of LEAST for ordinals›

  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
      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
  then show "P (LEAST i. Ord i  P i)" and "(LEAST i. Ord i  P i)  k" by auto

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

― ‹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
  fix y assume "Ord y  P y" thus "(LEAST i. Ord i  P i)  y"
    by (simp add: Ord_Least_le)
  fix x assume "Ord x  P x" "y. Ord y  P y  x  y" thus "Q x"
    by (simp add: assms(3))

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")
  assume ?rhs thus ?lhs by blast
  assume H: ?lhs then obtain α where α: "Ord α" "P α" by blast
  let ?x = "LEAST α. Ord α  P α"
  have "Ord ?x"
    by (metis Ord_Least α)
  { 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

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 μ"
    by (simp add: μ_def Ord_Least_le)
  then show False
    using μ by blast

lemma le_Sup_iff:
  assumes "A  ON" "Ord x" "small A" shows "x  A  (y  ON. y<x  (aA. y < a))"
proof (intro iffI ballI impI)
  show "aA. 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)
  show "x   A"
    if "yON. y < x  (aA. y < a)"
    using that assms
    by (metis Ord_Sup Ord_linear_le Sup_upper less_le_not_le mem_Collect_eq subsetD)

lemma le_SUP_iff: "f ` A  ON; Ord x; small A  x  (f ` A)  (y  ON. y<x  (iA. y < f i))"
  by (simp add: le_Sup_iff)

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)
      = (λxelts a. wfrec {(x, y). x  elts y} H x)"
    by (force simp: cut_def)
  then show ?thesis
    unfolding transrec_def
    by (simp add: foundation wfrec)

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  (jelts i. VPow (Vfrom a j))  b  (jelts i. VPow (Vfrom b j))"
    by (intro sup_mono cSUP_subset_mono a  b) auto
  then show ?case
    by (metis Vfrom)

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

lemma Vfrom_mono: "Ord i; ab; ij  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)

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

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)

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"])
  case False
  have *: "(xelts 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)
  show ?thesis
  proof (rule Vfrom [THEN trans])
    show "a  (jelts (succ i). VPow (Vfrom a j)) = a  VPow (Vfrom a i)"
      using assms
      by (intro sup_mono order_antisym) (auto simp: Sup_V_insert *)

lemma Vset_succ: "Ord i  Vset(succ(i)) = VPow(Vset(i))"
  by (simp add: Vfrom_succ_Ord)

lemma Vfrom_Sup:
  assumes "X  {}" "small X"
  shows "Vfrom a (Sup X) = (yX. Vfrom a y)"
proof (rule order_antisym)
  have "Vfrom a ( X) = a  (jelts ( 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 "(jelts ( 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 .
      then show ?thesis
        by (simp add: SUP_le_iff small X)
    ultimately show ?thesis
      by auto
  finally show "Vfrom a ( X)   (Vfrom a ` X)" .
  have "x. x  X 
         a  (jelts x. VPow (Vfrom a j))
          a  (jelts ( 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)

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)