# 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```