(* 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