Theory ZFC_in_HOL.Ordinal_Exp

section ‹Exponentiation of ordinals›

theory Ordinal_Exp
  imports Kirby

begin

text ‹Source: Schlöder, Julian.  Ordinal Arithmetic; available online at
    \url{http://www.math.uni-bonn.de/ag/logik/teaching/2012WS/Set%20theory/oa.pdf}›

definition oexp :: "[V,V] ⇒ V" (infixr "↑" 80)
  where "oexp a b ≡ transrec (λf x. if x=0 then 1
                                    else if Limit x then if a=0 then 0 else ⨆ξ ∈ elts x. f ξ
                                    else f (⨆(elts x)) * a)  b"

text ‹@{term "0↑ω = 1"} if we don't make a special case for Limit ordinals and zero›


lemma oexp_0_right [simp]: "α↑0 = 1"
  by (simp add: def_transrec [OF oexp_def])

lemma oexp_succ [simp]: "Ord β ⟹ α↑(succ β) = α↑β * α"
  by (simp add: def_transrec [OF oexp_def])

lemma oexp_Limit: "Limit β ⟹ α↑β = (if α=0 then 0 else ⨆ξ ∈ elts β. α↑ξ)"
  by (auto simp: def_transrec [OF oexp_def, of _ β])

lemma oexp_1_right [simp]: "α↑1 = α"
  using one_V_def oexp_succ by fastforce

lemma oexp_1 [simp]: "Ord α ⟹ 1↑α = 1"
  by (induction rule: Ord_induct3) (use Limit_def oexp_Limit in auto)

lemma oexp_0 [simp]: "Ord α ⟹ 0↑α = (if α = 0 then 1 else 0)"
  by (induction rule: Ord_induct3) (use Limit_def oexp_Limit in auto)

lemma oexp_eq_0_iff [simp]:
  assumes "Ord β" shows "α↑β = 0 ⟷ α=0 ∧ β≠0"
  using ‹Ord β›
proof (induction rule: Ord_induct3)
  case (Limit μ)
  then show ?case
    using Limit_def oexp_Limit by auto
qed auto

lemma oexp_gt_0_iff [simp]:
  assumes "Ord β" shows "α↑β > 0 ⟷ α>0 ∨ β=0"
  by (simp add: assms less_V_def)

lemma ord_of_nat_oexp: "ord_of_nat (m^n) = ord_of_nat m↑ord_of_nat n"
proof (induction n)
  case (Suc n)
  then show ?case
    by (simp add: mult.commute [of m]) (simp add: ord_of_nat_mult)
qed auto

lemma omega_closed_oexp [intro]:
  assumes "α ∈ elts ω" "β ∈ elts ω" shows "α↑β ∈ elts ω"
proof -
  obtain m n where "α = ord_of_nat m" "β = ord_of_nat n"
    using assms elts_ω by auto
  then have "α↑β = ord_of_nat (m^n)"
    by (simp add: ord_of_nat_oexp)
  then show ?thesis
    by (simp add: ω_def)
qed


lemma Ord_oexp [simp]:
  assumes "Ord α" "Ord β" shows "Ord (α↑β)"
  using ‹Ord β›
proof (induction rule: Ord_induct3)
  case (Limit α)
  then show ?case
    by (auto simp: oexp_Limit image_iff intro: Ord_Sup)
qed (auto intro: Ord_mult assms)

text ‹Lemma 3.19›
lemma le_oexp:
  assumes "Ord α" "Ord β" "β ≠ 0" shows "α ≤ α↑β"
  using ‹Ord β› ‹β ≠ 0›
proof (induction rule: Ord_induct3)
  case (succ β)
  then show ?case
    by simp (metis ‹Ord α› le_0 le_mult mult.left_neutral oexp_0_right order_refl order_trans)
next
  case (Limit μ)
  then show ?case
    by (metis Limit_def Limit_eq_Sup_self ZFC_in_HOL.Sup_upper eq_iff image_eqI image_ident oexp_1_right oexp_Limit replacement small_elts one_V_def)
qed auto


text ‹Lemma 3.20›
lemma le_oexp':
  assumes "Ord α" "1 < α" "Ord β" shows "β ≤ α↑β"
proof (cases "β = 0")
  case True
  then show ?thesis
    by auto
next
  case False
  show ?thesis
    using ‹Ord β›
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ γ)
    then have "α↑γ * 1 < α↑γ * α"
      using ‹Ord α› ‹1 < α›
      by (metis le_mult less_V_def mult.right_neutral mult_cancellation not_less_0 oexp_eq_0_iff succ.hyps)
    then have " γ < α↑succ γ"
      using succ.IH succ.hyps by auto
    then show ?case
      using False ‹Ord α› ‹1 < α› succ
      by (metis Ord_mem_iff_lt Ord_oexp Ord_succ elts_succ insert_subset less_eq_V_def less_imp_le)
  next
    case (Limit μ)
    with False ‹1 < α› show ?case
      by (force simp: Limit_def oexp_Limit intro: elts_succ)
  qed
qed


lemma oexp_Limit_le:
  assumes "β < γ" "Limit γ" "Ord β" "α > 0" shows "α↑β ≤ α↑γ"
proof -
  have "Ord γ"
    using Limit_def assms(2) by blast
  with assms show ?thesis
    using Ord_mem_iff_lt ZFC_in_HOL.Sup_upper oexp_Limit by auto
qed

proposition oexp_less:
  assumes β: "β ∈ elts γ" and "Ord γ" and α: "α > 1" "Ord α" shows "α↑β < α↑γ"
proof -
  obtain "β < γ" "Ord β"
    using Ord_in_Ord OrdmemD assms by auto
  have gt0: "α↑β > 0"
    using ‹Ord β› α dual_order.order_iff_strict by auto
  show ?thesis
    using ‹Ord γ› β
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ δ)
    then consider "β = δ" | "β < δ"
      using OrdmemD elts_succ by blast
    then show ?case
    proof cases
      case 1
      then have "(α↑β) * 1 < (α↑δ) * α"
        using Ord_1 Ord_oexp α gt0 mult_cancel_less_iff succ.hyps by metis
      then show ?thesis
        by (simp add: succ.hyps)
    next
      case 2
      then have "(α↑δ) * 1 < (α↑δ) * α"
        by (meson Ord_1 Ord_mem_iff_lt Ord_oexp ‹Ord β› α gt0 less_trans mult_cancel_less_iff succ)
      with 2 show ?thesis
        using Ord_mem_iff_lt ‹Ord β› succ by auto
    qed
  next
    case (Limit γ)
    then obtain "Ord γ" "succ β < γ"
      using Limit_def Ord_in_Ord OrdmemD assms by auto
    have "α↑β = (α↑β) * 1"
      by simp
    also have "… < (α↑β) * α"
      using Ord_oexp ‹Ord β› assms gt0 mult_cancel_less_iff by blast
    also have "… = α↑succ β"
      by (simp add: ‹Ord β›)
    also have "… ≤ (⨆ξ ∈ elts γ. α↑ξ)"
    proof -
      have "succ β ∈ elts γ"
        using Limit.hyps Limit.prems Limit_def by auto
      then show ?thesis
        by (simp add: ZFC_in_HOL.Sup_upper)
    qed
    finally
    have "α↑β < (⨆ξ ∈ elts γ. α↑ξ)" .
    then show ?case
      using Limit.hyps oexp_Limit ‹α > 1› by auto
  qed
qed

corollary oexp_less_iff:
  assumes "α > 0" "Ord α" "Ord β" "Ord γ" shows "α↑β < α↑γ ⟷ β ∈ elts γ ∧ α > 1"
proof safe
  show "β ∈ elts γ" "1 < α"
    if "α↑β < α↑γ"
  proof -
    show "α > 1"
    proof (rule ccontr)
      assume "¬ α > 1"
      then consider "α=0" | "α=1"
        using ‹Ord α› less_V_def mem_0_Ord by fastforce
      then show False
        by cases (use that ‹α > 0› ‹Ord β› ‹Ord γ› in ‹auto split: if_split_asm›)
    qed
    show β: "β ∈ elts γ"
    proof (rule ccontr)
      assume "β ∉ elts γ"
      then have "γ ≤ β"
        by (meson Ord_linear_le Ord_mem_iff_lt assms less_le_not_le)
      then consider "γ = β" | "γ < β"
        using less_V_def by blast
      then show False
      proof cases
        case 1
        then show ?thesis
          using that by blast
      next
        case 2
        with ‹α > 1› have "α↑γ < α↑β"
          by (simp add: Ord_mem_iff_lt assms oexp_less)
        with that show ?thesis
          by auto
      qed
    qed
  qed
  show "α↑β < α↑γ" if "β ∈ elts γ" "1 < α"
    using that by (simp add: assms oexp_less)
qed

lemma ω_oexp_iff [simp]: "⟦Ord α; Ord β⟧ ⟹ ω↑α = ω↑β ⟷ α=β"
  by (metis Ord_ω Ord_linear ω_gt1 less_irrefl oexp_less)

lemma Limit_oexp:
  assumes "Limit γ" "Ord α" "α > 1" shows "Limit (α↑γ)"
  unfolding Limit_def
proof safe
  show Oαγ: "Ord (α↑γ)"
    using Limit_def Ord_oexp ‹Limit γ› assms(2) by blast
  show 0: "0 ∈ elts (α↑γ)"
    using Limit_def oexp_Limit ‹Limit γ› ‹α > 1› by fastforce
  have "Ord γ"
    using Limit_def ‹Limit γ› by blast
  fix x
  assume x: "x ∈ elts (α↑γ)"
  with ‹Limit γ› ‹α > 1›
  obtain β where "β < γ" "Ord β" "Ord x" and xβ: "x ∈ elts (α↑β)"
    apply (simp add: oexp_Limit split: if_split_asm)
    using Ord_in_Ord OrdmemD ‹Ord γ› Oαγ x by blast
  then have Oαβ: "Ord (α↑β)"
    using Ord_oexp assms(2) by blast
  have "β ∈ elts γ"
    by (simp add: Ord_mem_iff_lt ‹Ord β› ‹Ord γ› ‹β < γ›)
  moreover have "α ≠ 0"
    using ‹α > 1› by blast
  ultimately have αβγ: "α↑β ≤ α↑γ"
    by (simp add: Sup_upper oexp_Limit ‹Limit γ›)
  have "succ x ≤ α↑β"
    by (simp add: OrdmemD Oαβ ‹Ord x› succ_le_iff xβ)
  then consider "succ x < α↑β" | "succ x = α↑β"
    using le_neq_trans by blast
  then show "succ x ∈ elts (α↑γ)"
  proof cases
    case 1
    with αβγ show ?thesis
      using Oαβ Ord_mem_iff_lt ‹Ord x› by blast
  next
    case 2
    then have "succ β < γ"
      using Limit_def OrdmemD ‹β ∈ elts γ› assms(1) by auto
    have ge1: "1 ≤ α↑β"
      by (metis "2" Ord_0 ‹Ord x› le_0 le_succ_iff one_V_def)
    have "succ x < succ (α↑β)"
      using "2" Oαβ succ_le_iff by auto
    also have "… ≤ (α↑β) + (α↑β)"
      using ge1 by (simp add: succ_eq_add1)
    also have "… = (α↑β) * succ (succ 0)"
      by (simp add: mult_succ)
    also have "… ≤ (α↑β) * α"
      using Oαβ Ord_succ assms(2) assms(3) one_V_def succ_le_iff by auto
    also have "… = α↑succ β"
      by (simp add: ‹Ord β›)
    also have "… ≤ α↑γ"
      by (meson Limit_def ‹β ∈ elts γ› assms dual_order.order_iff_strict oexp_less)
  finally show ?thesis
    by (simp add: "2" Oαβ Oαγ Ord_mem_iff_lt)
  qed
qed



lemma oexp_mono:
  assumes α: "Ord α" "α ≠ 0" and β: "Ord β" "γ ⊑ β" shows "α↑γ ≤ α↑β"
  using β
proof (induction rule: Ord_induct3)
  case 0
  then show ?case
    by simp
next
  case (succ β)
  with α le_mult show ?case
    by (auto simp: le_TC_succ)
next
  case (Limit μ)
  then have "α↑γ ≤ ⨆ ((↑) α ` elts μ)"
    using Limit.hyps Ord_less_TC_mem ‹α ≠ 0› le_TC_def by (auto simp: oexp_Limit Limit_def)
  then show ?case
    using α by (simp add: oexp_Limit Limit.hyps)
qed

lemma oexp_mono_le:
  assumes "γ ≤ β" "α ≠ 0" "Ord α" "Ord β" "Ord γ" shows "α↑γ ≤ α↑β"
  by (simp add: assms oexp_mono vle2 vle_iff_le_Ord)

lemma oexp_sup:
  assumes "α ≠ 0" "Ord α" "Ord β" "Ord γ" shows "α↑(β ⊔ γ) = α↑β ⊔ α↑γ"
  by (metis Ord_linear_le assms oexp_mono_le sup.absorb2 sup.orderE)

lemma oexp_Sup:
  assumes α: "α ≠ 0" "Ord α" and X: "X ⊆ ON" "small X" "X ≠ {}" shows "α↑⨆ X = ⨆ ((↑) α ` X)"
proof (rule order_antisym)
  show "⨆ ((↑) α ` X) ≤ α↑⨆ X"
    by (metis ON_imp_Ord Ord_Sup ZFC_in_HOL.Sup_upper assms cSUP_least oexp_mono_le)
next
  have "Ord (Sup X)"
    using Ord_Sup X by auto
  then show "α↑⨆ X ≤ ⨆ ((↑) α ` X)"
  proof (cases rule: Ord_cases)
    case 0
    then show ?thesis
      using X dual_order.antisym by fastforce
  next
    case (succ β)
    then show ?thesis
      using ZFC_in_HOL.Sup_upper X succ_in_Sup_Ord by auto
  next
    case limit
    show ?thesis
    proof (clarsimp simp: assms oexp_Limit limit)
      fix x y z
      assume x: "x ∈ elts (α ↑ y)" and "z ∈ X" "y ∈ elts z"
      then have "α ↑ y ≤ α ↑ z"
        by (meson ON_imp_Ord Ord_in_Ord OrdmemD α ‹X ⊆ ON› le_less oexp_mono_le)
      with x have "x ∈ elts (α ↑ z)" by blast
      then show "∃u∈X. x ∈ elts (α ↑ u)"
        using ‹z ∈ X› by blast
    qed
  qed
qed


lemma omega_le_Limit:
  assumes "Limit μ" shows "ω ≤ μ"
proof
  fix ρ
  assume "ρ ∈ elts ω"
  then obtain n where "ρ = ord_of_nat n"
    using elts_ω by auto
  have "ord_of_nat n ∈ elts μ"
    by (induction n) (use Limit_def assms in auto)
  then show "ρ ∈ elts μ"
    using ‹ρ = ord_of_nat n› by auto
qed

lemma finite_omega_power [simp]:
  assumes "1 < n" "n ∈ elts ω" shows "n↑ω = ω"
proof (rule order_antisym)
  have "⨆ ((↑) (ord_of_nat k) ` elts ω) ≤ ω" for k
  proof (induction k)
    case 0
    then show ?case
      by auto
  next
    case (Suc k)
    then show ?case
      by (metis Ord_ω OrdmemD Sup_eq_0_iff ZFC_in_HOL.SUP_le_iff le_0 le_less omega_closed_oexp ord_of_nat_ω)
  qed
  then show "n↑ω ≤ ω"
    using assms
    by (simp add: elts_ω oexp_Limit) metis
  show "ω ≤ n↑ω"
    using Ord_in_Ord assms le_oexp' by blast
qed


proposition oexp_add:
  assumes "Ord α" "Ord β" "Ord γ" shows "α↑(β + γ) = α↑β * α↑γ"
proof (cases ‹α = 0›)
  case True
  then show ?thesis
    using assms by simp
next
  case False
  show ?thesis
    using ‹Ord γ›
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case (succ ξ)
    then show ?case
      using ‹Ord β› by (auto simp: plus_V_succ_right mult.assoc)
  next
    case (Limit μ)
    have "α↑(β + (⨆ξ∈elts μ. ξ)) = (⨆ξ∈elts (β + μ). α↑ξ)"
      by (simp add: Limit.hyps oexp_Limit assms False)
    also have "… = (⨆ξ ∈ {ξ. Ord ξ ∧ β + ξ < β + μ}. α↑(β + ξ))"
    proof (rule Sup_eq_Sup)
      show "(λξ. α↑(β + ξ)) ` {ξ. Ord ξ ∧ β + ξ < β + μ} ⊆ (↑) α ` elts (β + μ)"
        using Limit.hyps Limit_def Ord_mem_iff_lt imageI by blast
      fix x
      assume "x ∈ (↑) α ` elts (β + μ)"
      then obtain ξ where ξ: "ξ ∈ elts (β + μ)" and x: "x = α↑ξ"
        by auto
      have "∃γ. Ord γ ∧ γ < μ ∧ α↑ξ ≤ α↑(β + γ)"
      proof (rule mem_plus_V_E [OF ξ])
        assume "ξ ∈ elts β"
        then have "α↑ξ ≤ α↑β"
          by (meson arg_subset_TC assms False le_TC_def less_TC_def oexp_mono vsubsetD)
        with zero_less_Limit [OF ‹Limit μ›]
        show "∃γ. Ord γ ∧ γ < μ ∧ α↑ξ ≤ α↑(β + γ)"
          by force
      next
        fix δ
        assume "δ ∈ elts μ" and "ξ = β + δ"
        have "Ord δ"
          using Limit.hyps Limit_def Ord_in_Ord ‹δ ∈ elts μ› by blast
        moreover have "δ < μ"
          using Limit.hyps Limit_def OrdmemD ‹δ ∈ elts μ› by auto
        ultimately show "∃γ. Ord γ ∧ γ < μ ∧ α↑ξ ≤ α↑(β + γ)"
          using ‹ξ = β + δ› by blast
      qed
      then show "∃y∈(λξ. α↑(β + ξ)) ` {ξ. Ord ξ ∧ β + ξ < β + μ}. x ≤ y"
        using x by auto
    qed auto
    also have "… = (⨆ξ∈elts μ. α↑(β + ξ))"
      using ‹Limit μ›
      by (simp add: Ord_Collect_lt Limit_def)
    also have "… = (⨆ξ∈elts μ. α↑β * α↑ξ)"
      using Limit.IH by auto
    also have "… = α↑β * α↑(⨆ξ∈elts μ. ξ)"
      using ‹α ≠ 0› Limit.hyps
      by (simp add: image_image oexp_Limit mult_Sup_distrib)
    finally show ?case .
  qed
qed

proposition oexp_mult:
  assumes "Ord α" "Ord β" "Ord γ" shows "α↑(β * γ) = (α↑β)↑γ"
proof (cases "α = 0 ∨ β = 0")
  case True
  then show ?thesis
    by (auto simp: ‹Ord β› ‹Ord γ›)
next
  case False
  show ?thesis
    using ‹Ord γ›
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by auto
  next
    case succ
    then show ?case
      using assms by (auto simp: mult_succ oexp_add)
  next
    case (Limit μ)
    have Lim: "Limit (⨆ ((*) β ` elts μ))"
      unfolding Limit_def
    proof (intro conjI allI impI)
      show "Ord (⨆ ((*) β ` elts μ))"
        using Limit.hyps Limit_def Ord_in_Ord ‹Ord β› by (auto intro: Ord_Sup)
      have "succ 0 ∈ elts μ"
        using Limit.hyps Limit_def by blast
      then show "0 ∈ elts (⨆ ((*) β ` elts μ))"
        using False ‹Ord β› mem_0_Ord by force
      show "succ y ∈ elts (⨆ ((*) β ` elts μ))"
        if "y ∈ elts (⨆ ((*) β ` elts μ))" for y
        using that False Limit.hyps
        apply (clarsimp simp: Limit_def)
        by (metis Ord_in_Ord Ord_linear Ord_mem_iff_lt Ord_mult Ord_succ assms(2) less_V_def mult_cancellation mult_succ not_add_mem_right succ_le_iff succ_ne_self)
    qed
    have "α↑(β * (⨆ξ∈elts μ. ξ)) = α↑⨆ ((*) β ` elts μ)"
      by (simp add: mult_Sup_distrib)
    also have "… = ⨆ (⋃x∈elts μ. (↑) α ` elts (β * x))"
      using False Lim oexp_Limit by fastforce
    also have "… = (⨆x∈elts μ. α↑(β * x))"
    proof (rule Sup_eq_Sup)
      show "(λx. α↑(β * x)) ` elts μ ⊆ (⋃x∈elts μ. (↑) α ` elts (β * x))"
        using ‹Ord α› ‹Ord β› False Limit
        apply clarsimp
        by (metis Limit_def elts_succ imageI insertI1 mem_0_Ord mult_add_mem_0)
      show "∃y∈(λx. α↑(β * x)) ` elts μ. x ≤ y"
        if "x ∈ (⋃x∈elts μ. (↑) α ` elts (β * x))" for x
        using that ‹Ord α› ‹Ord β› False Limit
        by clarsimp (metis Limit_def Ord_in_Ord Ord_mult VWO_TC_le mem_imp_VWO oexp_mono)
    qed auto
    also have "… = ⨆ ((↑) (α↑β) ` elts (⨆ξ∈elts μ. ξ))"
      using Limit.IH Limit.hyps by auto
    also have "… = (α↑β)↑(⨆ξ∈elts μ. ξ)"
      using False Limit.hyps oexp_Limit ‹Ord β› by auto
    finally show ?case .
  qed
qed

lemma Limit_omega_oexp:
  assumes "Ord δ" "δ ≠ 0"
  shows "Limit (ω↑δ)"
  using assms
proof (cases δ rule: Ord_cases)
  case 0
  then show ?thesis
    using assms(2) by blast
next
  case (succ l)
  have *: "succ β ∈ elts (ω↑l * n + ω↑l)"
    if n: "n ∈ elts ω" and β: "β ∈ elts (ω↑l * n)" for n β
  proof -
    obtain "Ord n" "Ord β"
      by (meson Ord_ω Ord_in_Ord Ord_mult Ord_oexp β n succ(1))
    obtain oo: "Ord (ω↑l)" "Ord (ω↑l * n)"
      by (simp add: ‹Ord n› succ(1))
    moreover have f4: "β < ω↑l * n"
      using oo Ord_mem_iff_lt ‹Ord β› ‹β ∈ elts (ω↑l * n)› by blast
    moreover have f5: "Ord (succ β)"
      using ‹Ord β› by blast
    moreover have "ω↑l ≠ 0"
      using oexp_eq_0_iff omega_nonzero succ(1) by blast
    ultimately show ?thesis
      by (metis add_less_cancel_left Ord_ω Ord_add Ord_mem_iff_lt OrdmemD ‹Ord β› add.right_neutral dual_order.strict_trans2 oexp_gt_0_iff succ(1) succ_le_iff zero_in_omega)
  qed
  show ?thesis
    using succ
    apply (clarsimp simp: Limit_def mem_0_Ord)
    apply (simp add: mult_Limit)
    by (metis * mult_succ succ_in_omega)
next
  case limit
  then show ?thesis
    by (metis Limit_oexp Ord_ω OrdmemD one_V_def succ_in_omega zero_in_omega)
qed

lemma oexp_mult_commute:
  fixes j::nat
  assumes "Ord α"
  shows "(α ↑ j) * α = α * (α ↑ j)"
proof -
  have "(α ↑ j) * α = α ↑ (1 + ord_of_nat j)"
    by (simp add: one_V_def)
  also have "... = α * (α ↑ j)"
    by (simp add: assms oexp_add)
  finally show ?thesis .
qed

lemma oexp_ω_Limit: "Limit β ⟹ ω↑β = (⨆ξ ∈ elts β. ω↑ξ)"
  by (simp add: oexp_Limit)

lemma ω_power_succ_gtr: "Ord α ⟹ ω ↑ α * ord_of_nat n < ω ↑ succ α"
  by (simp add: OrdmemD)

lemma countable_oexp:
  assumes ν: "α ∈ elts ω1" 
  shows "ω ↑ α ∈ elts ω1"
proof -
  have "Ord α"
    using Ord_ω1 Ord_in_Ord assms by blast
  then show ?thesis
    using assms
  proof (induction rule: Ord_induct3)
    case 0
    then show ?case
      by (simp add: Ord_mem_iff_lt)
  next
    case (succ α)
    then have "countable (elts (ω ↑ α * ω))"
      by (simp add: succ_in_Limit_iff countable_mult less_ω1_imp_countable)
    then show ?case
      using Ord_mem_iff_lt countable_iff_less_ω1 succ.hyps by auto
  next
    case (Limit α)
    with Ord_ω1 have "countable (⋃β∈elts α. elts (ω ↑ β))" "Ord (ω ↑ ⨆ (elts α))"
      by (force simp: Limit_def intro: Ord_trans less_ω1_imp_countable)+
    then have "ω ↑ ⨆ (elts α) < ω1"
      using Limit.hyps countable_iff_less_ω1 oexp_Limit by fastforce
    then show ?case
      using Limit.hyps Limit_def Ord_mem_iff_lt by auto
  qed
qed

end