Theory CZH_Sets_VNHS

(* Copyright 2021 (C) Mihails Milehins *)

section‹Further results related to the von Neumann hierarchy of sets›
theory CZH_Sets_VNHS
  imports 
    CZH_Sets_FBRelations
    CZH_Sets_Ordinals
begin



subsection‹Background›


text‹
The subsection presents several further auxiliary results about the 
von Neumann hierarchy of sets. The primary general reference for this section
is cite‹"takeuti_introduction_1971"›.
›



subsection‹Further properties of ‹Vfrom››


text‹Reusable patterns.›

lemma Vfrom_Ord_bundle:
  assumes "A = A" and "i = i"
  shows "Vfrom A i = Vfrom A (rank i)" and "Ord (rank i)"
  by (simp_all add: Vfrom_rank_eq )

lemma Vfrom_in_bundle:
  assumes "i ∈∘ j" and "A = A" and "B = B"
  shows "Vfrom A i = Vfrom A (rank i)"
    and "Ord (rank i)"
    and "Vfrom B j = Vfrom B (rank j)"
    and "Ord (rank j)"
    and "rank i ∈∘ rank j"
  by (simp_all add: assms(1) Vfrom_rank_eq Ord_mem_iff_lt rank_lt)


text‹Elementary corollaries.›

lemma Ord_Vset_in_Vset_succI[intro]:
  assumes "Ord α" 
  shows "Vset α ∈∘ Vset (succ α)"
  by (simp add: Vset_succ assms)

lemma Ord_in_in_VsetI[intro]:
  assumes "Ord α" and "a ∈∘ α"
  shows "a ∈∘ Vset α"
  by (metis assms Ord_VsetI Ord_iff_rank rank_lt)


text‹Transitivity of the constant const‹Vfrom›.›

lemma Vfrom_trans[intro]:
  assumes "Transset A" and "x ∈∘ X" and "X ∈∘ Vfrom A i" 
  shows "x ∈∘ Vfrom A i"
  using Transset_def by (blast intro: assms Transset_Vfrom)

lemma Vset_trans[intro]:
  assumes "x ∈∘ X" and "X ∈∘ Vset i" 
  shows "x ∈∘ Vset i"
  by (auto intro: assms)


text‹Monotonicity of the constant const‹Vfrom›.›

lemma Vfrom_in_mono:
  assumes "A ⊆∘ B" and "i ∈∘ j"
  shows "Vfrom A i ∈∘ Vfrom B j"
proof-
  define i' where "i' = rank i"
  define j' where "j' = rank j"
  note rank_conv = 
    Vfrom_in_bundle[
      OF assms(2) HOL.refl[of A] HOL.refl[of B], folded i'_def j'_def
      ]
  show ?thesis
    unfolding rank_conv using rank_conv(4,5)
  proof induction
    case (succ j')
    from succ have "Ord (succ j')" by auto
    from succ(3) succ.hyps have "i' ⊆∘ j'" by (auto simp: Ord_def Transset_def)
    from Vfrom_mono[OF ‹Ord i'› assms(1) this] show ?case 
      unfolding Vfrom_succ_Ord[OF ‹Ord j'›, of B] by simp
  next
    case (Limit j')
    from Limit(3) obtain ξ where "i' ∈∘ ξ" and "ξ ∈∘ j'" by auto
    with vifunionI have "Vfrom A i' ∈∘ (⋃∘ξ∈∘j'. Vfrom B ξ)" 
      by (auto simp: Limit.IH)
    then show "Vfrom A i' ∈∘ Vfrom B (⋃∘ξ∈∘j'. ξ)"
      unfolding Limit_Vfrom_eq[symmetric, OF Limit(1)] 
      by (simp add: SUP_vifunion[symmetric] Limit.hyps)
  qed auto
qed

lemmas Vset_in_mono = Vfrom_in_mono[OF order_refl, of _ _ 0]

lemma Vfrom_vsubset_mono:
  assumes "A ⊆∘ B" and "i ⊆∘ j"
  shows "Vfrom A i ⊆∘ Vfrom B j"
  by (metis assms Vfrom_Ord_bundle(1,2) Vfrom_mono rank_mono)

lemmas Vset_vsubset_mono = Vfrom_vsubset_mono[OF order_refl, of _ _ 0]

lemma arg1_vsubset_Vfrom: "a ⊆∘ Vfrom a i" using Vfrom by blast
                                                     
lemma VPow_vsubset_Vset:
  ―‹Based on Theorem 9.10 from \cite{takeuti_introduction_1971}›
  assumes "X ∈∘ Vset i" 
  shows "VPow X ⊆∘ Vset i"
proof-
  define i' where "i' = rank i"
  note rank_conv = Vfrom_Ord_bundle[OF refl[of 0] refl[of i], folded i'_def]
  show ?thesis 
    using rank_conv(2) assms unfolding rank_conv
  proof induction
    case (Limit α)
    from Limit have "X ∈∘ (⋃∘i∈∘α. Vset i)"
      by (simp add: SUP_vifunion[symmetric] Limit_Vfrom_eq)
    then have "VPow X ⊆∘ (⋃∘i∈∘α. Vset i)"
      by (intro vsubsetI) (metis Limit.IH vifunionE vifunionI vsubsetE)
    then show ?case 
      by (simp add: SUP_vifunion[symmetric] Limit.hyps Limit_Vfrom_eq)
  qed (simp_all add: Vset_succ)
qed

lemma Vfrom_vsubset_VPow_Vfrom:
  assumes "Transset A"
  shows "Vfrom A i ⊆∘ VPow (Vfrom A i)"
  using assms Transset_VPow Transset_Vfrom by (auto simp: Transset_def)

lemma arg1_vsubset_VPow_Vfrom:
  assumes "Transset A"
  shows "A ⊆∘ VPow (Vfrom A i)"
  by (meson assms Vfrom_vsubset_VPow_Vfrom arg1_vsubset_Vfrom dual_order.trans)



subsection‹Operations closed with respect to const‹Vset››


text‹Empty set.›

lemma Limit_vempty_in_VsetI:
  assumes "Limit α"
  shows "0 ∈∘ Vset α"
  using assms by (auto simp: Limit_def)


text‹Subset.›

lemma vsubset_in_VsetI[intro]:
  assumes "a ⊆∘ A" and "A ∈∘ Vset i" 
  shows "a ∈∘ Vset i"
  using assms by (auto dest: VPow_vsubset_Vset)

lemma Ord_vsubset_in_Vset_succI:
  assumes "Ord α" and "A ⊆∘ Vset α"
  shows "A ∈∘ Vset (succ α)"
  using assms Ord_Vset_in_Vset_succI by auto


text‹Power set.›

lemma Limit_VPow_in_VsetI[intro]:
  assumes "Limit α" and "A ∈∘ Vset α" 
  shows "VPow A ∈∘ Vset α"
proof-
  from assms(1) have "Ord α" by auto
  with assms obtain i where "A ∈∘ Vset i" and "i ∈∘ α" and "Ord i"
    by (fastforce simp: Ord_in_Ord Limit_Vfrom_eq)
  have "Vset i ∈∘ Vset α" by (rule Vset_in_mono) (auto intro: ‹i ∈∘ α›)
  from VPow_vsubset_Vset[OF ‹A ∈∘ Vset i›] this show ?thesis
    by (rule vsubset_in_VsetI)
qed

lemma VPow_in_Vset_revD:
  assumes "VPow A ∈∘ Vset i"
  shows "A ∈∘ Vset i"
  using assms Vset_trans by blast

lemma Ord_VPow_in_Vset_succI:
  assumes "Ord α" and "a ∈∘ Vset α"
  shows "VPow a ∈∘ Vset (succ α)"
  using VPow_vsubset_Vset[OF assms(2)] 
  by (auto intro: Ord_Vset_in_Vset_succI[OF assms(1)])

lemma Ord_VPow_in_Vset_succD:
  assumes "Ord α" and "VPow a ∈∘ Vset (succ α)"
  shows "a ∈∘ Vset α"
  using assms by (fastforce dest: Vset_succ)


text‹Union of elements.›

lemma VUnion_in_VsetI[intro]:
  assumes "A ∈∘ Vset i"
  shows "⋃∘A ∈∘ Vset i"
proof-
  define i' where "i' = rank i"
  note rank_conv = Vfrom_Ord_bundle[OF refl[of 0] refl[of i], folded i'_def]
  from rank_conv(2) assms show ?thesis 
    unfolding rank_conv
  proof induction
    case (succ α)
    show "⋃∘A ∈∘ Vset (succ α)"
      by (metis succ(1,3) VPow_iff VUnion_least Vset_trans Vset_succ)
  qed (auto simp: vrange_VLambda vimage_VLambda_vrange_rep Limit_Vfrom_eq)
qed

lemma Limit_VUnion_in_VsetD:
  assumes "Limit α" and "⋃∘A ∈∘ Vset α"
  shows "A ∈∘ Vset α"
proof-
  have "A ⊆∘ VPow (⋃∘A)" by auto
  moreover from assms have "VPow (⋃∘A) ∈∘ Vset α" by (rule Limit_VPow_in_VsetI)
  ultimately show ?thesis using assms(1) by auto
qed


text‹Intersection of elements.›

lemma VInter_in_VsetI[intro]:
  assumes "A ∈∘ Vset α"
  shows "⋂∘A ∈∘ Vset α"
proof-
  have subset: "⋂∘A ⊆∘ ⋃∘A" by auto
  moreover from assms have "⋃∘A ∈∘ Vset α" by (rule VUnion_in_VsetI)
  ultimately show ?thesis by (rule vsubset_in_VsetI)
qed


text‹Singleton.›

lemma Limit_vsingleton_in_VsetI[intro]:
  assumes "Limit α" and "a ∈∘ Vset α"
  shows "set {a} ∈∘ Vset α"
proof-
  have aa: "set {a} ⊆∘ VPow a" by auto
  from assms(1) have "Ord α" by auto
  from vsubset_in_VsetI[OF aa Limit_VPow_in_VsetI[OF assms(1)]] show ?thesis
    by (simp add: Limit_is_Ord assms(2))
qed

lemma Limit_vsingleton_in_VsetD:
  assumes "set {a} ∈∘ Vset α"
  shows "a ∈∘ Vset α"
  using assms by auto

lemma Ord_vsingleton_in_Vset_succI:
  assumes "Ord α" and "a ∈∘ Vset α"
  shows "set {a} ∈∘ Vset (succ α)"
  using assms by (simp add: Vset_succ vsubset_vsingleton_leftI)


text‹Doubleton.›

lemma Limit_vdoubleton_in_VsetI[intro]:
  assumes "Limit α" and "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "set {a, b} ∈∘ Vset α"
proof-
  from assms(1) have "Ord α" by auto
  from assms have "a ∈∘ (⋃∘ξ∈∘α. Vset ξ)" and "b ∈∘ (⋃∘ξ∈∘α. Vset ξ)" 
    by (simp_all add: SUP_vifunion[symmetric] Limit_Vfrom_eq)
  then obtain A B 
    where a: "a ∈∘ Vset A" and "A ∈∘ α" and b: "b ∈∘ Vset B" and "B ∈∘ α"
    by blast
  moreover with assms have "Ord A" and "Ord B" by auto
  ultimately have "A ∪∘ B ∈∘ α" 
    by (metis Ord_linear_le le_iff_sup sup.order_iff)
  then have "Vset (A ∪∘ B) ∈∘ Vset α" 
    by (simp add: assms Limit_is_Ord Vset_in_mono)
  moreover from a b have "set {a, b} ⊆∘ Vset (A ∪∘ B)" 
    by (simp add: Vfrom_sup vsubset_vdoubleton_leftI)
  ultimately show "set {a, b} ∈∘ Vset α" by (rule vsubset_in_VsetI[rotated 1])
qed

lemma vdoubleton_in_VsetD:
  assumes "set {a, b} ∈∘ Vset α"
  shows "a ∈∘ Vset α" and "b ∈∘ Vset α"
  using assms by (auto intro!: Vset_trans[of _ ‹set {a, b}›])

lemma Ord_vdoubleton_in_Vset_succI:
  assumes "Ord α" and "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "set {a, b} ∈∘ Vset (succ α)"
  by 
    (
      meson 
        assms Ord_Vset_in_Vset_succI vsubset_in_VsetI vsubset_vdoubleton_leftI
    )


text‹Pairwise union.›

lemma vunion_in_VsetI[intro]:
  assumes "a ∈∘ Vset i" and "b ∈∘ Vset i"
  shows "a ∪∘ b ∈∘ Vset i"
proof-
  define i' where "i' = rank i"
  note rank_conv = Vfrom_Ord_bundle[OF refl[of 0] refl[of i], folded i'_def]
  show ?thesis 
    using rank_conv(2) assms unfolding rank_conv
  proof induction
    case (Limit α)
    from Limit have "set {a, b} ∈∘ Vset α"  
      by (intro Limit_vdoubleton_in_VsetI; unfold SUP_vifunion[symmetric]) 
        simp_all
    then have "⋃∘(set {a, b}) ∈∘ Vset α" by (blast intro: Limit.hyps)
    with Limit.hyps VUnion_vdoubleton have "a ∪∘ b ∈∘ (⋃∘ξ∈∘α. Vset ξ)"
      by (auto simp: Limit_Vfrom_eq)
    then show "a ∪∘ b ∈∘ Vset (⋃∘ξ∈∘α. ξ)" 
      by (simp add: ‹Limit α› Limit_Vfrom_eq)
  qed (auto simp add: Vset_succ)
qed

lemma vunion_in_VsetD:
  assumes "a ∪∘ b ∈∘ Vset α"
  shows "a ∈∘ Vset α" and "b ∈∘ Vset α"
  using assms by (meson vsubset_in_VsetI inf_sup_ord(3,4))+


text‹Pairwise intersection.›

lemma vintersection_in_VsetI[intro]:
  assumes "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "a ∩∘ b ∈∘ Vset α"
  using assms by (meson vsubset_in_VsetI inf_sup_ord(2))


text‹Set difference.›

lemma vdiff_in_VsetI[intro]:
  assumes "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "a -∘ b ∈∘ Vset α"
  using assms by auto


text‹const‹vinsert›.›

lemma vinsert_in_VsetI[intro]:
  assumes "Limit α" and "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "vinsert a b ∈∘ Vset α"
proof-
  have ab: "vinsert a b = set {a} ∪∘ b" by simp
  from assms(2) have "set {a} ∈∘ Vset α"
    by (simp add: Limit_vsingleton_in_VsetI assms(1))
  from this assms(1,3) show "vinsert a b ∈∘ Vset α"
    unfolding ab by blast
qed

lemma vinsert_in_Vset_succI[intro]:
  assumes "Ord α" and "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "vinsert a b ∈∘ Vset (succ α)"
  using assms by blast

lemma vinsert_in_Vset_succI'[intro]:
  assumes "Ord α" and "a ∈∘ Vset α" and "b ∈∘ Vset (succ α)"
  shows "vinsert a b ∈∘ Vset (succ α)"
proof-
  have ab: "vinsert a b = set {a} ∪∘ b" by simp
  show ?thesis
    unfolding ab by (intro vunion_in_VsetI Ord_vsingleton_in_Vset_succI assms)
qed

lemma vinsert_in_VsetD:
  assumes "vinsert a b ∈∘ Vset α"
  shows "a ∈∘ Vset α" and "b ∈∘ Vset α"
  using assms Vset_trans by blast+

lemma Limit_insert_in_VsetI:
  assumes [intro]: "Limit α" 
    and [simp]: "small x" 
    and "set x ∈∘ Vset α"
    and [intro]: "a ∈∘ Vset α"
  shows "set (insert a x) ∈∘ Vset α"
proof-
  have ax: "set (insert a x) = vinsert a (set x)" by auto
  from assms show ?thesis unfolding ax by auto
qed


text‹Pair.›

lemma Limit_vpair_in_VsetI[intro]:
  assumes "Limit α" and "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "⟨a, b⟩ ∈∘ Vset α"
  using assms Limit_vdoubleton_in_VsetI Limit_vsingleton_in_VsetI 
  unfolding vpair_def
  by simp

lemma vpair_in_VsetD[intro]:
  assumes "⟨a, b⟩ ∈∘ Vset α"
  shows "a ∈∘ Vset α" and "b ∈∘ Vset α"
  using assms unfolding vpair_def by (meson vdoubleton_in_VsetD)+


text‹Cartesian product.›

lemma Limit_vtimes_in_VsetI[intro]:  
  assumes "Limit α" and "A ∈∘ Vset α" and "B ∈∘ Vset α"
  shows "A ×∘ B ∈∘ Vset α"
proof-
  from assms(1) have "Ord α" by auto
  have "VPow (VPow (A ∪∘ B)) ∈∘ Vset α"
    by (simp add: assms Limit_VPow_in_VsetI Limit_is_Ord vunion_in_VsetI)
  from assms(1) vsubset_in_VsetI[OF vtimes_vsubset_VPowVPow this] show ?thesis 
    by auto
qed


text‹Binary relations.›

lemma (in vbrelation) vbrelation_Limit_in_VsetI[intro]: 
  assumes "Limit α" and "𝒟∘ r ∈∘ Vset α" and "ℛ∘ r ∈∘ Vset α"
  shows "r ∈∘ Vset α"  
  using assms vdomain_vrange_vtimes by auto

lemma 
  assumes "r ∈∘ Vset α"
  shows vdomain_in_VsetI: "𝒟∘ r ∈∘ Vset α" 
    and vrange_in_VsetI: "ℛ∘ r ∈∘ Vset α" 
    and vfield_in_VsetI: "ℱ∘ r ∈∘ Vset α"
proof-
  from assms have "⋃∘r ∈∘ Vset α" by auto
  with assms(1) have r: "⋃∘(⋃∘r) ∈∘ Vset α" by blast
  from r assms(1) vfield_vsubset_VUnion2 show "ℱ∘ r ∈∘ Vset α" by auto
  from r assms(1) vdomain_vsubset_VUnion2 vrange_vsubset_VUnion2 show 
    "𝒟∘ r ∈∘ Vset α" "ℛ∘ r ∈∘ Vset α"
    by auto
qed

lemma (in vbrelation) vbrelation_Limit_vsubset_VsetI:
  assumes "Limit α" and "𝒟∘ r ⊆∘ Vset α" and "ℛ∘ r ⊆∘ Vset α"
  shows "r ⊆∘ Vset α"
proof(intro vsubsetI)
  fix x assume "x ∈∘ r"
  moreover then obtain a b where x_def: "x = ⟨a, b⟩" by (elim vbrelation_vinE)
  ultimately have "a ∈∘ 𝒟∘ r" and "b ∈∘ ℛ∘ r" by auto
  with assms show "x ∈∘ Vset α" unfolding x_def by auto
qed

lemma 
  assumes "r ∈∘ Vset α"
  shows fdomain_in_VsetI: "𝒟∙ r ∈∘ Vset α" 
    and frange_in_VsetI: "ℛ∙ r ∈∘ Vset α" 
    and ffield_in_VsetI: "ℱ∙ r ∈∘ Vset α"
proof-
  from assms have "⋃∘r ∈∘ Vset α" by auto
  with assms have r: "⋃∘(⋃∘(⋃∘r)) ∈∘ Vset α" by blast
  from r assms(1) fdomain_vsubset_VUnion2 frange_vsubset_VUnion2 show 
    "𝒟∙ r ∈∘ Vset α" "ℛ∙ r ∈∘ Vset α"
    by auto
  from r assms(1) ffield_vsubset_VUnion2 show "ℱ∙ r ∈∘ Vset α" by auto
qed

lemma (in vsv) vsv_Limit_vrange_in_VsetI[intro]: 
  assumes "Limit α" and "ℛ∘ r ⊆∘ Vset α" and "vfinite (𝒟∘ r)" 
  shows "ℛ∘ r ∈∘ Vset α"
  using assms(3,1,2) vsv_axioms
proof(induction ‹𝒟∘ r› arbitrary: r rule: vfinite_induct)
  case vempty
  interpret r': vsv r by (rule vempty(4))
  from vempty(1) r'.vlrestriction_vdomain have "r = 0" by simp
  from Vset_in_mono vempty.prems(1) show ?case 
    unfolding ‹r = 0› by (auto simp: Limit_def)
next
  case (vinsert x F)
  interpret r': vsv r by (rule vinsert(7))
  have RrF_Rr: "ℛ∘ (r ↾l∘ F) ⊆∘ ℛ∘ r" by auto
  have F_DrF: "F = 𝒟∘ (r ↾l∘ F)" 
    unfolding vdomain_vlrestriction vinsert(4)[symmetric] by auto
  moreover note assms(1)
  moreover from RrF_Rr vinsert(6) have "ℛ∘ (r ↾l∘ F) ⊆∘ Vset α" by auto
  moreover have "vsv (r ↾l∘ F)" by simp
  ultimately have RrF_Vα: "ℛ∘ (r ↾l∘ F) ∈∘ Vset α" by (rule vinsert(3))
  have "ℛ∘ r = vinsert (r⦇x⦈) (ℛ∘ (r ↾l∘ F))" 
  proof(intro vsubset_antisym vsubsetI)
    fix b assume "b ∈∘ ℛ∘ r"
    then obtain a where "a ∈∘ 𝒟∘ r" and b_def: "b = r⦇a⦈" by force
    with vinsert.hyps(4) have "a = x ∨ a ∈∘ F" by auto
    with ‹a ∈∘ 𝒟∘ r› show "b ∈∘ vinsert (r⦇x⦈) (ℛ∘ (r ↾l∘ F))"
      unfolding b_def by (blast dest: r'.vsv_vimageI1)
  next
    fix b assume "b ∈∘ vinsert (r⦇x⦈) (ℛ∘ (r ↾l∘ F))"
    with RrF_Rr r'.vsv_axioms vinsert.hyps(4) show "b ∈∘ ℛ∘ r" by auto
  qed
  moreover with vinsert.prems(2) have "r⦇x⦈ ∈∘ Vset α" by auto
  moreover have "ℛ∘ (r ↾l∘ F) ∈∘ Vset α" by (blast intro: RrF_Vα)
  ultimately show "ℛ∘ r ∈∘ Vset α" 
    by (simp add: vinsert.prems(1) vinsert_in_VsetI)
qed

lemma (in vsv) vsv_Limit_vsv_in_VsetI[intro]: 
  assumes "Limit α" 
    and "𝒟∘ r ∈∘ Vset α"
    and "ℛ∘ r ⊆∘ Vset α" 
    and "vfinite (𝒟∘ r)" 
  shows "r ∈∘ Vset α"
  by (simp add: assms vsv_Limit_vrange_in_VsetI vbrelation_Limit_in_VsetI)

lemma Limit_vcomp_in_VsetI:
  assumes "Limit α" and "r ∈∘ Vset α" and "s ∈∘ Vset α"
  shows "r ∘∘ s ∈∘ Vset α"
proof(rule vbrelation.vbrelation_Limit_in_VsetI; (intro assms(1))?)
  show "vbrelation (r ∘∘ s)" by auto
  have "𝒟∘ (r ∘∘ s) ⊆∘ 𝒟∘ s" by auto
  with assms(3) show "𝒟∘ (r ∘∘ s) ∈∘ Vset α"  
    by (auto simp: vdomain_in_VsetI vsubset_in_VsetI)
  have "ℛ∘ (r ∘∘ s) ⊆∘ ℛ∘ r" by auto
  with assms(2) show "ℛ∘ (r ∘∘ s) ∈∘ Vset α"
    by (auto simp: vrange_in_VsetI vsubset_in_VsetI)
qed


text‹Operations on indexed families of sets.›

lemma Limit_vifintersection_in_VsetI:
  assumes "Limit α" and "⋀i. i ∈∘ I ⟹ A i ∈∘ Vset α" and "vfinite I"
  shows "(⋂∘i∈∘I. A i) ∈∘ Vset α"
proof-
  from assms(2) have range: "ℛ∘ (λi∈∘I. A i) ⊆∘ Vset α" by auto
  from assms(1) range assms(3) have "ℛ∘ (λi∈∘I. A i) ∈∘ Vset α"
    by (rule rel_VLambda.vsv_Limit_vrange_in_VsetI[unfolded vdomain_VLambda])
  then have "(λi∈∘I. A i) `∘ I ∈∘ Vset α" 
    by (simp add: vimage_VLambda_vrange_rep)
  then show "(⋂∘i∈∘I. A i) ∈∘ Vset α" by auto
qed

lemma Limit_vifunion_in_VsetI:
  assumes "Limit α" and "⋀i. i ∈∘ I ⟹ A i ∈∘ Vset α" and "vfinite I"
  shows "(⋃∘i∈∘I. A i) ∈∘ Vset α"
proof-
  from assms(2) have range: "ℛ∘ (λi∈∘I. A i) ⊆∘ Vset α" by auto
  from assms(1) range assms(3) have "ℛ∘ (λi∈∘I. A i) ∈∘ Vset α"
    by (rule rel_VLambda.vsv_Limit_vrange_in_VsetI[unfolded vdomain_VLambda])
  then have "(λi∈∘I. A i) `∘ I ∈∘ Vset α" 
    by (simp add: vimage_VLambda_vrange_rep)
  then show "(⋃∘i∈∘I. A i) ∈∘ Vset α" by auto
qed

lemma Limit_vifunion_in_Vset_if_VLambda_in_VsetI:
  assumes "Limit α" and "VLambda I A ∈∘ Vset α"
  shows "(⋃∘i∈∘I. A i) ∈∘ Vset α"
proof-
  from assms(2) have "ℛ∘ (λi∈∘I. A i) ∈∘ Vset α"
    by (simp add: vrange_in_VsetI)
  then have "(λi∈∘I. A i) `∘ I ∈∘ Vset α" 
    by (simp add: vimage_VLambda_vrange_rep)
  then show "(⋃∘i∈∘I. A i) ∈∘ Vset α" by auto
qed

lemma Limit_vproduct_in_VsetI:
  assumes "Limit α" 
    and "I ∈∘ Vset α" 
    and "⋀i. i ∈∘ I ⟹ A i ∈∘ Vset α" 
    and "vfinite I"
  shows "(∏∘i∈∘I. A i) ∈∘ Vset α"
proof-
  have "(⋃∘i∈∘I. A i) ∈∘ Vset α"
    by (rule Limit_vifunion_in_VsetI) (simp_all add: assms(1,3,4))
  with assms have "I ×∘ (⋃∘i∈∘I. A i) ∈∘ Vset α" by auto
  with assms(1) have "VPow (I ×∘ (⋃∘i∈∘I. A i)) ∈∘ Vset α" by auto
  from vsubset_in_VsetI[OF vproduct_vsubset_VPow[of I A] this] show ?thesis 
    by simp
qed

lemma Limit_vproduct_in_Vset_if_VLambda_in_VsetI:
  assumes "Limit α" and "VLambda I A ∈∘ Vset α"
  shows "(∏∘i∈∘I. A i) ∈∘ Vset α"
proof-
  have "(⋃∘i∈∘I. A i) ∈∘ Vset α"
    by (rule Limit_vifunion_in_Vset_if_VLambda_in_VsetI) 
      (simp_all add: assms)
  moreover from assms(2) have "I ∈∘ Vset α"
    by (metis vdomain_VLambda vdomain_in_VsetI)
  ultimately have "I ×∘ (⋃∘i∈∘I. A i) ∈∘ Vset α" 
    using assms by auto
  with assms(1) have "VPow (I ×∘ (⋃∘i∈∘I. A i)) ∈∘ Vset α" by auto
  from vsubset_in_VsetI[OF vproduct_vsubset_VPow[of I A] this] show ?thesis 
    by simp  
qed

lemma Limit_vdunion_in_Vset_if_VLambda_in_VsetI:
  assumes "Limit α" and "VLambda I A ∈∘ Vset α"
  shows "(∐∘i∈∘I. A i) ∈∘ Vset α"
proof-
  interpret vsv ‹VLambda I A› by auto
  from assms have "𝒟∘ (VLambda I A) ∈∘ Vset α" 
    by (fastforce intro!: vdomain_in_VsetI)
  then have I: "I ∈∘ Vset α" by simp
  have "(∐∘i∈∘I. A i) ⊆∘ I ×∘ (⋃∘(ℛ∘ (VLambda I A)))" by force
  moreover have "I ×∘ (⋃∘(ℛ∘ (VLambda I A))) ∈∘ Vset α"
    by (intro Limit_vtimes_in_VsetI assms I VUnion_in_VsetI vrange_in_VsetI)
  ultimately show "(∐∘i∈∘I. A i) ∈∘ Vset α" by auto
qed

lemma vrange_vprojection_in_VsetI:
  assumes "Limit α" 
    and "A ∈∘ Vset α" 
    and "⋀f. f ∈∘ A ⟹ vsv f"
    and "⋀f. f ∈∘ A ⟹ x ∈∘ 𝒟∘ f"
  shows "ℛ∘ (λf∈∘A. f⦇x⦈) ∈∘ Vset α"
proof-
  have "ℛ∘ (λf∈∘A. f⦇x⦈) ⊆∘ ⋃∘(⋃∘(⋃∘A))"
  proof(intro vsubsetI)
    fix y assume "y ∈∘ ℛ∘ (λf∈∘A. f⦇x⦈)"
    then obtain f where f: "f ∈∘ A" and y_def: "y = f⦇x⦈" by auto
    from f have "vsv f" and "x ∈∘ 𝒟∘ f" by (auto intro: assms(3,4))+
    with y_def have xy: "⟨x, y⟩ ∈∘ f" by auto
    show "y ∈∘ ⋃∘(⋃∘(⋃∘A))"
    proof(intro VUnionI)
      show "f ∈∘ A" by (rule f)
      show "⟨x, y⟩ ∈∘ f" by (rule xy)
      show "set {x, y} ∈∘ ⟨x, y⟩" unfolding vpair_def by simp
    qed auto
  qed
  moreover from assms(1,2) have "⋃∘(⋃∘(⋃∘A)) ∈∘ Vset α"
    by (intro VUnion_in_VsetI)
  ultimately show ?thesis by auto
qed

lemma Limit_vcpower_in_VsetI:
  assumes "Limit α" and "n ∈∘ Vset α" and "A ∈∘ Vset α" and "vfinite n"
  shows "A ^× n ∈∘ Vset α"
  using assms Limit_vproduct_in_VsetI unfolding vcpower_def by auto


text‹Finite sets.›

lemma Limit_vfinite_in_VsetI:
  assumes "Limit α" and "A ⊆∘ Vset α" and "vfinite A"
  shows "A ∈∘ Vset α"
proof-
  from assms(3) obtain n where n: "n ∈∘ ω" and "n ≈∘ A" by clarsimp
  then obtain f where f: "v11 f" and dr: "𝒟∘ f = n" "ℛ∘ f = A" by auto
  interpret f: v11 f by (rule f)
  from n have n: "vfinite n" by auto
  show ?thesis 
    by (rule f.vsv_Limit_vrange_in_VsetI[simplified dr, OF assms(1,2) n])
qed


text‹Ordinal numbers.›

lemma Limit_omega_in_VsetI:
  assumes "Limit α"
  shows "aℕ ∈∘ Vset α"
proof-
  from assms have "α ⊆∘ Vset α" by force
  moreover have "ω ⊆∘ α" by (simp add: assms omega_le_Limit)
  moreover have "aℕ ∈∘ ω" by simp
  ultimately show "aℕ ∈∘ Vset α" by auto
qed

lemma Limit_succ_in_VsetI:
  assumes "Limit α" and "a ∈∘ Vset α"
  shows "succ a ∈∘ Vset α"
  by (simp add: assms succ_def vinsert_in_VsetI)


text‹Sequences.›

lemma (in vfsequence) vfsequence_Limit_vcons_in_VsetI:
  assumes "Limit α" and "x ∈∘ Vset α" and "xs ∈∘ Vset α"
  shows "vcons xs x ∈∘ Vset α"
  unfolding vcons_def
proof(intro vinsert_in_VsetI Limit_vpair_in_VsetI assms)
  show "vcard xs ∈∘ Vset α" 
    by (metis assms(3) vdomain_in_VsetI vfsequence_vdomain)
qed


text‹‹ftimes›.›

lemma Limit_ftimes_in_VsetI: 
  assumes "Limit α" and "A ∈∘ Vset α" and "B ∈∘ Vset α"
  shows "A ×∙ B ∈∘ Vset α"
    unfolding ftimes_def
proof(rule Limit_vproduct_in_VsetI)
  from assms(1) show "2ℕ ∈∘ Vset α" by (meson Limit_omega_in_VsetI)
  fix i assume "i ∈∘ 2ℕ"
  with assms(2,3) show "(i = 0 ? A : B) ∈∘ Vset α" by simp
qed (auto simp: assms(1))


text‹Auxiliary results.›

lemma vempty_in_Vset_succ[simp, intro]: "0 ∈∘ Vfrom a (succ b)"
  unfolding Vfrom_succ by force

lemma Limit_vid_on_in_Vset:
  assumes "Limit α" and "A ∈∘ Vset α"
  shows "vid_on A ∈∘ Vset α"
  by
    (
      rule vbrelation.vbrelation_Limit_in_VsetI
        [
          OF vbrelation_vid_on assms(1) ,
          unfolded vdomain_vid_on vrange_vid_on, OF assms(2,2)
        ]
    )

lemma Ord_vpair_in_Vset_succI[intro]:
  assumes "Ord α" and "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "⟨a, b⟩ ∈∘ Vset (succ (succ α))"
  unfolding vpair_def
proof-
  have aab: "set {set {a}, set {a, b}} = vinsert (set {a}) (set {set {a, b}})"
    by auto
  show "set {set {a}, set {a, b}} ∈∘ Vset (succ (succ α))"
    unfolding aab
    by 
      (
        intro
          assms
          vinsert_in_Vset_succI'
          Ord_vsingleton_in_Vset_succI 
          Ord_vdoubleton_in_Vset_succI 
          Ord_succ
      ) 
qed

lemma Limit_vifunion_vsubset_VsetI:
  assumes "Limit α" and "⋀i. i ∈∘ I ⟹ A i ∈∘ Vset α"
  shows "(⋃∘i∈∘I. A i) ⊆∘ Vset α"
proof(intro vsubsetI)
  fix x assume "x ∈∘ (⋃∘i∈∘I. A i)"
  then obtain i where i: "i ∈∘ I" and "x ∈∘ A i" by auto
  with assms(1) assms(2)[OF i] show "x ∈∘ Vset α" by auto
qed

lemma Limit_vproduct_vsubset_Vset_succI:
  assumes "Limit α" and "I ∈∘ Vset α" and "⋀i. i ∈∘ I ⟹ A i ⊆∘ Vset α"
  shows "(∏∘i∈∘I. A i) ⊆∘ Vset (succ α)"
proof(intro vsubsetI)
  fix a assume prems: "a ∈∘ (∏∘i∈∘I. A i)"
  note a = vproductD[OF prems]
  interpret vsv a by (rule a(1))
  from prems have "ℛ∘ a ⊆∘ (⋃∘i∈∘I. A i)" by (rule vproduct_vrange)  
  moreover have "(⋃∘i∈∘I. A i) ⊆∘ Vset α" by (intro vifunion_least assms(3))
  ultimately have "ℛ∘ a ⊆∘ Vset α" by auto
  moreover from assms(2) prems have "𝒟∘ a ⊆∘ Vset α" unfolding a(2) by auto
  ultimately have "a ⊆∘ Vset α"
    by (intro assms(1) vbrelation_Limit_vsubset_VsetI)
  with assms(1) show "a ∈∘ Vset (succ α)"
    by (simp add: Limit_is_Ord Ord_vsubset_in_Vset_succI)
qed

lemma Limit_vproduct_vsubset_Vset_succI':
  assumes "Limit α" and "I ∈∘ Vset α" and "⋀i. i ∈∘ I ⟹ A i ∈∘ Vset α"
  shows "(∏∘i∈∘I. A i) ⊆∘ Vset (succ α)"
proof-
  have "A i ⊆∘ Vset α" if "i ∈∘ I" for i
    by (simp add: Vset_trans vsubsetI assms(3) that)
  from assms(1,2) this show ?thesis by (rule Limit_vproduct_vsubset_Vset_succI)
qed

lemma (in vfsequence) vfsequence_Ord_vcons_in_Vset_succI: 
  assumes "Ord α"
    and "ω ∈∘ α"
    and "x ∈∘ Vset α"
    and "xs ∈∘ Vset (succ (succ (succ α)))"
  shows "vcons xs x ∈∘ Vset (succ (succ (succ α)))"
  unfolding vcons_def
proof(intro vinsert_in_Vset_succI' Ord_succ Ord_vpair_in_Vset_succI assms)
  have "vcard xs = 𝒟∘ xs" by (simp add: vfsequence_vdomain)
  from assms(1,2) vfsequence_vdomain_in_omega show "vcard xs ∈∘ Vset α" 
    unfolding vfsequence_vdomain[symmetric]
    by (meson Ord_in_in_VsetI Vset_trans)
qed

lemma Limit_VUnion_vdomain_in_VsetI:
  assumes "Limit α" and "Q ∈∘ Vset α"
  shows "(⋃∘r∈∘Q. 𝒟∘ r) ∈∘ Vset α"
proof-
  have "(⋃∘r∈∘Q. 𝒟∘ r) ⊆∘ ⋃∘(⋃∘(⋃∘Q))"
  proof(intro vsubsetI)
    fix a assume "a ∈∘ (⋃∘r∈∘Q. 𝒟∘ r)"
    then obtain r where r: "r ∈∘ Q" and "a ∈∘ 𝒟∘ r" by auto
    with assms obtain b where ab: "⟨a, b⟩ ∈∘ r" by auto
    show "a ∈∘ ⋃∘(⋃∘(⋃∘Q))"
    proof(intro VUnionI)
      show "r ∈∘ Q" by (rule r)  
      show "⟨a, b⟩ ∈∘ r" by (rule ab)
      show "set {a, b} ∈∘ ⟨a, b⟩" unfolding vpair_def by simp
    qed auto
  qed
  moreover from assms(2) have "⋃∘(⋃∘(⋃∘Q)) ∈∘ Vset α"
    by (blast dest!: VUnion_in_VsetI)
  ultimately show ?thesis using assms(1) by (auto simp: vsubset_in_VsetI)
qed

lemma Limit_VUnion_vrange_in_VsetI:
  assumes "Limit α" and "Q ∈∘ Vset α"
  shows "(⋃∘r∈∘Q. ℛ∘ r) ∈∘ Vset α"
proof-(*FIXME: duality*)
  have "(⋃∘r∈∘Q. ℛ∘ r) ⊆∘ ⋃∘(⋃∘(⋃∘Q))"
  proof(intro vsubsetI)
    fix b assume "b ∈∘ (⋃∘r∈∘Q. ℛ∘ r)"
    then obtain r where r: "r ∈∘ Q" and "b ∈∘ ℛ∘ r" by auto
    with assms obtain a where ab: "⟨a, b⟩ ∈∘ r" by auto
    show "b ∈∘ ⋃∘(⋃∘(⋃∘Q))"
    proof(intro VUnionI)
      show "r ∈∘ Q" by (rule r)  
      show "⟨a, b⟩ ∈∘ r" by (rule ab)
      show "set {a, b} ∈∘ ⟨a, b⟩" unfolding vpair_def by simp
    qed auto
  qed
  moreover from assms(2) have "⋃∘(⋃∘(⋃∘Q)) ∈∘ Vset α"
    by (blast dest!: VUnion_in_VsetI)
  ultimately show ?thesis using assms(1) by (auto simp: vsubset_in_VsetI)
qed



subsection‹Axioms for term‹Vset α››


text‹
The subsection demonstrates that the axioms of ZFC except for the 
Axiom Schema of Replacement hold in term‹Vset α› for any limit ordinal
term‹α› such that term‹ω ∈∘ α›\footnote{The presentation of the axioms is 
loosely based on the statement of the axioms of ZFC in Chapters 1-11 in 
cite‹"takeuti_introduction_1971"›.}.
›

locale 𝒵 = 
  fixes α 
  assumes Limit_α[intro, simp]: "Limit α"
    and omega_in_α[intro, simp]: "ω ∈∘ α"
begin

lemmas [intro] = 𝒵_axioms

lemma vempty_Z_def: "0 = set {x. x ≠ x}" by auto

lemma vempty_is_zet[intro, simp]: "0 ∈∘ Vset α" 
  using Vset_in_mono omega_in_α by auto

lemma Axiom_of_Extensionality:
  assumes "a ∈∘ Vset α" and "x = y" and "x ∈∘ a" 
  shows "y ∈∘ a" and "x ∈∘ Vset α" and "y ∈∘ Vset α"
  using assms by (simp_all add: Vset_trans)

lemma Axiom_of_Pairing:
  assumes "a ∈∘ Vset α" and "b ∈∘ Vset α"
  shows "set {a, b} ∈∘ Vset α"
  using assms by (simp add: Limit_vdoubleton_in_VsetI)

lemma Axiom_of_Unions:
  assumes "a ∈∘ Vset α"
  shows "⋃∘a ∈∘ Vset α"
  using assms by (simp add: VUnion_in_VsetI)

lemma Axiom_of_Powers:
  assumes "a ∈∘ Vset α"
  shows "VPow a ∈∘ Vset α"
  using assms by (simp add: Limit_VPow_in_VsetI)

lemma Axiom_of_Regularity:
  assumes "a ≠ 0" and "a ∈∘ Vset α"
  obtains x where "x ∈∘ a" and "x ∩∘ a = 0"
  using assms by (auto dest: trad_foundation)

lemma Axiom_of_Infinity: "ω ∈∘ Vset α"
  using Limit_is_Ord by (auto simp: Ord_iff_rank Ord_VsetI OrdmemD)

lemma Axiom_of_Choice: 
  assumes "A ∈∘ Vset α"
  obtains f where "f ∈∘ Vset α" and "⋀x. x ∈∘ A ⟹ x ≠ 0 ⟹ f⦇x⦈ ∈∘ x"
proof-
  define f where "f = (λx∈∘A. (SOME a. a ∈∘ x ∨ (x = 0 ∧ a = 0)))"
  interpret vsv f unfolding f_def by auto
  have A_def: "A = 𝒟∘ f" unfolding f_def by simp
  have Rf: "ℛ∘ f ⊆∘ vinsert 0 (⋃∘A)"
  proof(rule vsubsetI)
    fix y assume "y ∈∘ ℛ∘ f" 
    then obtain x where "x ∈∘ A" and "y = f⦇x⦈" 
      unfolding A_def by (blast dest: vrange_atD)
    then have y_def: "y = (SOME a. a ∈∘ x ∨ x = 0 ∧ a = 0)"
      unfolding f_def unfolding A_def by simp
    have "y = 0 ∨ y ∈∘ x"
    proof(cases ‹x = 0›)
      case False then show ?thesis 
        unfolding y_def by (metis (mono_tags, lifting) verit_sko_ex' vemptyE)
    qed (simp add: y_def)
    with ‹x ∈∘ A› show "y ∈∘ vinsert 0 (⋃∘A)" by clarsimp
  qed
  from assms have "⋃∘A ∈∘ Vset α" by (simp add: Axiom_of_Unions)
  with vempty_is_zet Limit_α have "vinsert 0 (⋃∘A) ∈∘ Vset α" by auto
  with Rf have "ℛ∘ f ∈∘ Vset α" by auto
  with Limit_α assms[unfolded A_def] have "f ∈∘ Vset α" by auto
  moreover have "x ∈∘ A ⟹ x ≠ 0 ⟹ f⦇x⦈ ∈∘ x" for x
  proof-
    assume prems: "x ∈∘ A" "x ≠ 0"
    then have "f⦇x⦈ = (SOME a. a ∈∘ x ∨ (x = 0 ∧ a = 0))"
      unfolding f_def by simp
    with prems(2) show "f⦇x⦈ ∈∘ x"
      by (metis (mono_tags, lifting) someI_ex vemptyE)
  qed
  ultimately show ?thesis by (simp add: that)
qed

end


text‹Trivial corollaries.›

lemma (in 𝒵) Ord_α: "Ord α" by auto

lemma (in 𝒵) 𝒵_Vset_ω2_vsubset_Vset: "Vset (ω + ω) ⊆∘ Vset α" 
  by (simp add: Vset_vsubset_mono omega2_vsubset_Limit)

lemma (in 𝒵) 𝒵_Limit_αω: "Limit (α + ω)" by (simp add: Limit_is_Ord)

lemma (in 𝒵) 𝒵_α_αω: "α ∈∘ α + ω" 
  by (simp add: Limit_is_Ord Ord_mem_iff_lt)

lemma (in 𝒵) 𝒵_ω_αω: "ω ∈∘ α + ω" 
  using add_le_cancel_left0 by blast

lemma 𝒵_ωω: "𝒵 (ω + ω)"
  using ω_gt0 by (auto intro: 𝒵.intro simp: Ord_mem_iff_lt)

lemma (in 𝒵) in_omega_in_omega_plus[intro]:
  assumes "a ∈∘ ω"
  shows "a ∈∘ Vset (α + ω)"
proof-
  from assms have "a ∈∘ Vset ω" by auto
  moreover have "Vset ω ∈∘ Vset (α + ω)" by (simp add: Vset_in_mono 𝒵_ω_αω)
  ultimately show "a ∈∘ Vset (α + ω)" by auto
qed

lemma (in 𝒵) ord_of_nat_in_Vset[simp]: "aℕ ∈∘ Vset α" by force


text‹‹vfsequences_on›.›

lemma (in 𝒵) vfsequences_on_in_VsetI:
  assumes "X ∈∘ Vset α"
  shows "vfsequences_on X ∈∘ Vset α"
proof-
  from vfsequences_on_subset_ω_set have "vfsequences_on X ⊆∘ VPow (ω ×∘ X)"
    by (auto simp: less_eq_V_def)
  moreover have "VPow (ω ×∘ X) ∈∘ Vset α"
    by (intro Limit_VPow_in_VsetI Limit_vtimes_in_VsetI assms Axiom_of_Infinity)
      auto
  ultimately show ?thesis by auto
qed



subsection‹Existence of a disjoint subset in term‹Vset α››

definition mk_doubleton :: "V ⇒ V ⇒ V"
  where "mk_doubleton X a = set {a, X}"

definition mk_doubleton_image :: "V ⇒ V ⇒ V"
  where "mk_doubleton_image X Y = set (mk_doubleton Y ` elts X)"

lemma inj_on_mk_doubleton: "inj_on (mk_doubleton X) (elts X)"
proof
  fix a b assume "mk_doubleton X a = mk_doubleton X b" 
  then have "{a, X} = {b, X}" unfolding mk_doubleton_def by auto
  then show "a = b" by (metis doubleton_eq_iff)
qed

lemma mk_doubleton_image_vsubset_veqpoll: 
  assumes "X ⊆∘ Y"
  shows "mk_doubleton_image X X ≈∘ mk_doubleton_image X Y"
  unfolding eqpoll_def
proof(intro exI[of _ ‹λA. vinsert Y (A -∘ set {X})›] bij_betw_imageI)
  show "inj_on (λA. vinsert Y (A -∘ set {X})) (elts (mk_doubleton_image X X))"
    unfolding mk_doubleton_image_def
  proof(intro inj_onI)
    fix y y' assume prems: 
      "y ∈∘ set (mk_doubleton X ` elts X)" 
      "y' ∈∘ set (mk_doubleton X ` elts X)" 
      "vinsert Y (y -∘ set {X}) = vinsert Y (y' -∘ set {X})" 
    then obtain x x' 
      where "x ∈∘ X" 
        and "x' ∈∘ X" 
        and y_def: "y = set {x, X}" 
        and y'_def: "y' = set {x', X}"
      by (clarsimp simp: mk_doubleton_def)
    with assms have xX_X: "set {x, X} -∘ set {X} = set {x}" 
      and x'X_X: "set {x', X} -∘ set {X} = set {x'}"
      by fastforce+
    from prems(3)[unfolded y_def y'_def] have "set {x, Y} = set {x', Y}"
      unfolding xX_X x'X_X by auto
    then have "x = x'" by (auto simp: doubleton_eq_iff)
    then show "y = y'" unfolding y_def y'_def by simp
  qed
  show 
    "(λA. vinsert Y (A -∘ set {X})) ` (elts (mk_doubleton_image X X)) = 
      (elts (mk_doubleton_image X Y))"
  proof(intro subset_antisym subsetI)
    fix z
    assume prems:
      "z ∈ (λA. vinsert Y (A -∘ set {X})) ` (elts (mk_doubleton_image X X))"
    then obtain y 
      where "y ∈∘ set (mk_doubleton X ` elts X)"
        and z_def: "z = vinsert Y (y -∘ set {X})"
      unfolding mk_doubleton_image_def by auto
    then obtain x where xX: "x ∈∘ X" and y_def: "y = set {x, X}" 
      unfolding mk_doubleton_def by clarsimp
    from xX have y_X: "y -∘ set {X} = set {x}" unfolding y_def by fastforce
    from z_def have z_def': "z = set {x, Y}"
      unfolding y_X by (simp add: doubleton_eq_iff vinsert_vsingleton)
    from xX show "z ∈∘ mk_doubleton_image X Y"
      unfolding z_def' mk_doubleton_def mk_doubleton_image_def by simp
  next
    fix z assume prems: "z ∈∘ mk_doubleton_image X Y"
    then obtain x where xX: "x ∈∘ X" and z_def: "z = set {x, Y}" 
      unfolding mk_doubleton_def mk_doubleton_image_def by clarsimp
    from xX have xX_XX: "set {x, X} ∈∘ set (mk_doubleton X ` elts X)"
      unfolding mk_doubleton_def by simp
    from xX have xX_X: "set {x, X} -∘ set {X} = set {x}" by fastforce
    have z_def': "z = vinsert Y (set {x, X} -∘ set {X})"
      unfolding xX_X z_def by auto
    with xX_XX show 
      "z ∈ (λA. vinsert Y (A -∘ set {X})) ` (elts (mk_doubleton_image X X))"
      unfolding z_def' mk_doubleton_image_def by simp
  qed
qed

lemma mk_doubleton_image_veqpoll: 
  assumes "X ⊆∘ Y"
  shows "X ≈∘ mk_doubleton_image X Y"
proof-
  have "X ≈∘ mk_doubleton_image X X"
    unfolding mk_doubleton_image_def by (auto simp: inj_on_mk_doubleton)
  also have "… ≈ elts (mk_doubleton_image X Y)"
    by (rule mk_doubleton_image_vsubset_veqpoll[OF assms])
  finally show "X ≈∘ mk_doubleton_image X Y".
qed

lemma vdisjnt_mk_doubleton_image: "vdisjnt (mk_doubleton_image X Y) Y"
proof
  fix b assume prems: "b ∈∘ Y" "b ∈∘ mk_doubleton_image X Y" 
  then obtain a where "a ∈∘ X" and "set {a, Y} = b" 
    unfolding mk_doubleton_def mk_doubleton_image_def by clarsimp
  then have "Y ∈∘ b" by clarsimp
  with mem_not_sym show False by (simp add: prems)
qed

lemma Limit_mk_doubleton_image_vsubset_Vset: 
  assumes "Limit α" and "X ⊆∘ Y" and "Y ∈∘ Vset α"
  shows "mk_doubleton_image X Y ⊆∘ Vset α"
proof(intro vsubsetI)
  fix b assume "b ∈∘ mk_doubleton_image X Y"
  then obtain a where "b = mk_doubleton Y a" and "a ∈∘ X" 
    unfolding mk_doubleton_image_def by clarsimp
  with assms have b_def: "b = set {a, Y}" and aα: "a ∈∘ Vset α" 
    by (auto simp: mk_doubleton_def)
  from this(2) assms show "b ∈∘ Vset α"
    unfolding b_def by (simp add: Limit_vdoubleton_in_VsetI)
qed

lemma Ord_mk_doubleton_image_vsubset_Vset_succ: 
  assumes "Ord α" and "X ⊆∘ Y" and "Y ∈∘ Vset α"
  shows "mk_doubleton_image X Y ⊆∘ Vset (succ α)"
proof(intro vsubsetI)
  fix b assume "b ∈∘ mk_doubleton_image X Y"
  then obtain a where "b = mk_doubleton Y a" and "a ∈∘ X" 
    unfolding mk_doubleton_image_def by clarsimp
  with assms have b_def: "b = set {a, Y}" and aα: "a ∈∘ Vset α" 
    by (auto simp: mk_doubleton_def)
  from this(2) assms show "b ∈∘ Vset (succ α)"
    unfolding b_def by (simp add: Ord_vdoubleton_in_Vset_succI)
qed

lemma Limit_ex_eqpoll_vdisjnt:
  assumes "Limit α" and "X ⊆∘ Y" and "Y ∈∘ Vset α"
  obtains Z where "X ≈∘ Z" and "vdisjnt Z Y" and "Z ⊆∘ Vset α"
  using assms
  by (intro that[of ‹mk_doubleton_image X Y›])
    (
      simp_all add: 
        mk_doubleton_image_veqpoll 
        vdisjnt_mk_doubleton_image 
        Limit_mk_doubleton_image_vsubset_Vset
    )

lemma Ord_ex_eqpoll_vdisjnt:
  assumes "Ord α" and "X ⊆∘ Y" and "Y ∈∘ Vset α"
  obtains Z where "X ≈∘ Z" and "vdisjnt Z Y" and "Z ⊆∘ Vset (succ α)"
  using assms
  by (intro that[of ‹mk_doubleton_image X Y›])
    (
      simp_all add: 
        mk_doubleton_image_veqpoll 
        vdisjnt_mk_doubleton_image 
        Ord_mk_doubleton_image_vsubset_Vset_succ
    )

text‹\newpage›

end