section‹The Delta System Lemma, Relativized\label{sec:dsl-rel}› theory Delta_System_Relative imports Cardinal_Library_Relative begin relativize functional "delta_system" "delta_system_rel" external locale M_delta = M_cardinal_library_extra + assumes countable_lepoll_assms: "M(G) ⟹ M(A) ⟹ M(b) ⟹ M(f) ⟹ separation(M, λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λx. {xa ∈ G . x ∈ xa}, b, f, i)⟩)" begin lemma disjoint_separation: "M(c) ⟹ separation(M, λ x. ∃a. ∃b. x=⟨a,b⟩ ∧ a ∩ b = c)" using separation_Pair separation_eq lam_replacement_constant lam_replacement_Int by simp lemma (in M_trans) mem_F_bound6: fixes F G defines "F ≡ λ_ x. Collect(G, (∈)(x))" shows "x∈F(G,c) ⟹ c ∈ (range(f) ∪ ⋃G)" using apply_0 unfolding F_def by (cases "M(c)", auto simp:F_def) lemma delta_system_Aleph_rel1: assumes "∀A∈F. Finite(A)" "F ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(F)" shows "∃D[M]. D ⊆ F ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" proof - have "M(G) ⟹ M(p) ⟹ M({A∈G . p ∈ A})" for G p proof - assume "M(G)" "M(p)" have "{A∈G . p ∈ A} = G ∩ (Memrel({p} ∪ G) `` {p})" unfolding Memrel_def by auto with ‹M(G)› ‹M(p)› show ?thesis by simp qed from ‹∀A∈F. Finite(A)› ‹M(F)› have "M(λA∈F. |A|⇗M⇖)" using cardinal_rel_separation Finite_cardinal_rel_in_nat[OF _ transM[of _ F]] separation_imp_lam_closed[of _ "cardinal_rel(M)" ω] by simp text‹Since all members are finite,› with ‹∀A∈F. Finite(A)› ‹M(F)› have "(λA∈F. |A|⇗M⇖) : F →⇗M⇖ ω" (is "?cards : _") by (simp add:mem_function_space_rel_abs, rule_tac lam_type) (force dest:transM) moreover from this have a:"?cards -`` {n} = { A∈F . |A|⇗M⇖ = n }" for n using vimage_lam by auto moreover note ‹F ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(F)› moreover from calculation text‹there are uncountably many have the same cardinal:› obtain n where "n∈ω" "|?cards -`` {n}|⇗M⇖ = ℵ⇘1⇙⇗M⇖" using eqpoll_rel_Aleph_rel1_cardinal_rel_vimage[of F ?cards] by auto moreover define G where "G ≡ ?cards -`` {n}" moreover from calculation and ‹M(?cards)› have "M(G)" by blast moreover from calculation have "G ⊆ F" by auto ultimately text‹Therefore, without loss of generality, we can assume that all elements of the family have cardinality \<^term>‹n∈ω›.› have "A∈G ⟹ |A|⇗M⇖ = n" and "G ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" and "M(G)" for A using cardinal_rel_Card_rel_eqpoll_rel_iff by auto with ‹n∈ω› text‹So we prove the result by induction on this \<^term>‹n› and generalizing \<^term>‹G›, since the argument requires changing the family in order to apply the inductive hypothesis.› have "∃D[M]. D ⊆ G ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" proof (induct arbitrary:G) case 0 ― ‹This case is impossible› then have "G ⊆ {0}" using cardinal_rel_0_iff_0 by (blast dest:transM) with ‹G ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(G)› show ?case using nat_lt_Aleph_rel1 subset_imp_le_cardinal_rel[of G "{0}"] lt_trans2 cardinal_rel_Card_rel_eqpoll_rel_iff by auto next case (succ n) have "∀a∈G. Finite(a)" proof fix a assume "a ∈ G" moreover note ‹M(G)› ‹n∈ω› moreover from calculation have "M(a)" by (auto dest: transM) moreover from succ and ‹a∈G› have "|a|⇗M⇖ = succ(n)" by simp ultimately show "Finite(a)" using Finite_cardinal_rel_iff' nat_into_Finite[of "succ(n)"] by fastforce qed show "∃D[M]. D ⊆ G ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" proof (cases "∃p[M]. {A∈G . p ∈ A} ≈⇗M⇖ ℵ⇘1⇙⇗M⇖") case True ― ‹the positive case, uncountably many sets with a common element› then obtain p where "{A∈G . p ∈ A} ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(p)" by blast moreover note 1=‹M(G)› ‹M(G) ⟹ M(p) ⟹ M({A∈G . p ∈ A})› singleton_closed[OF ‹M(p)›] moreover from this have "M({x - {p} . x ∈ {x ∈ G . p ∈ x}})" using RepFun_closed[OF lam_replacement_Diff'[THEN lam_replacement_imp_strong_replacement]] Diff_closed[OF transM[OF _ 1(2)]] by auto moreover from 1 have "M(converse(λx∈{x ∈ G . p ∈ x}. x - {p}))" (is "M(converse(?h))") using converse_closed[of ?h] lam_closed[OF diff_Pair_replacement] Diff_closed[OF transM[OF _ 1(2)]] by auto moreover from calculation have "{A-{p} . A∈{X∈G. p∈X}} ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" (is "?F ≈⇗M⇖ _") using Diff_bij_rel[of "{A∈G . p ∈ A}" "{p}", THEN comp_bij_rel[OF bij_rel_converse_bij_rel, where C="ℵ⇘1⇙⇗M⇖", THEN bij_rel_imp_eqpoll_rel, of _ _ ?F]] unfolding eqpoll_rel_def by (auto simp del:mem_bij_abs) text‹Now using the hypothesis of the successor case,› moreover from ‹⋀A. A∈G ⟹ |A|⇗M⇖=succ(n)› ‹∀a∈G. Finite(a)› and this ‹M(G)› have "p∈A ⟹ A∈G ⟹ |A - {p}|⇗M⇖ = n" for A using Finite_imp_succ_cardinal_rel_Diff[of _ p] by (force dest: transM) moreover have "∀a∈?F. Finite(a)" proof (clarsimp) fix A assume "p∈A" "A∈G" with ‹⋀A. p ∈ A ⟹ A ∈ G ⟹ |A - {p}|⇗M⇖ = n› and ‹n∈ω› ‹M(G)› have "Finite(|A - {p}|⇗M⇖)" using nat_into_Finite by simp moreover from ‹p∈A› ‹A∈G› ‹M(G)› have "M(A - {p})" by (auto dest: transM) ultimately show "Finite(A - {p})" using Finite_cardinal_rel_iff' by simp qed moreover text‹we may apply the inductive hypothesis to the new family \<^term>‹?F›:› note ‹(⋀A. A ∈ ?F ⟹ |A|⇗M⇖ = n) ⟹ ?F ≈⇗M⇖ ℵ⇘1⇙⇗M⇖ ⟹ M(?F) ⟹ ∃D[M]. D ⊆ ?F ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› moreover note 1=‹M(G)› ‹M(G) ⟹ M(p) ⟹ M({A∈G . p ∈ A})› singleton_closed[OF ‹M(p)›] moreover from this have "M({x - {p} . x ∈ {x ∈ G . p ∈ x}})" using RepFun_closed[OF lam_replacement_Diff'[THEN lam_replacement_imp_strong_replacement]] Diff_closed[OF transM[OF _ 1(2)]] by auto ultimately obtain D where "D⊆{A-{p} . A∈{X∈G. p∈X}}" "delta_system(D)" "D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(D)" by auto moreover from this obtain r where "∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r" by fastforce then have "∀A∈D.∀B∈D. A∪{p} ≠ B∪{p}⟶(A ∪ {p}) ∩ (B ∪ {p}) = r∪{p}" by blast ultimately have "delta_system({B ∪ {p} . B∈D})" (is "delta_system(?D)") by fastforce moreover from ‹M(D)› ‹M(p)› have "M(?D)" using RepFun_closed un_Pair_replacement transM[of _ D] by auto moreover from ‹D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(D)› have "Infinite(D)" "|D|⇗M⇖ = ℵ⇘1⇙⇗M⇖" using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1[THEN iffD2, THEN uncountable_rel_imp_Infinite, of D] cardinal_rel_eqpoll_rel_iff[of D "ℵ⇘1⇙⇗M⇖"] ‹M(D)› ‹D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› by auto moreover from this ‹M(?D)› ‹M(D)› ‹M(p)› have "?D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" using cardinal_rel_map_Un[of D "{p}"] naturals_lt_nat cardinal_rel_eqpoll_rel_iff[THEN iffD1] by simp moreover note ‹D ⊆ {A-{p} . A∈{X∈G. p∈X}}› have "?D ⊆ G" proof - { fix A assume "A∈G" "p∈A" moreover from this have "A = A - {p} ∪ {p}" by blast ultimately have "A -{p} ∪ {p} ∈ G" by auto } with ‹D ⊆ {A-{p} . A∈{X∈G. p∈X}}› show ?thesis by blast qed moreover note ‹M(?D)› ultimately show "∃D[M]. D ⊆ G ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" by auto next case False note ‹¬ (∃p[M]. {A ∈ G . p ∈ A} ≈⇗M⇖ ℵ⇘1⇙⇗M⇖)› ― ‹the other case› ‹M(G)› ‹⋀p. M(G) ⟹ M(p) ⟹ M({A∈G . p ∈ A})› moreover from ‹G ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› and this have "M(p) ⟹ {A ∈ G . p ∈ A} ≲⇗M⇖ ℵ⇘1⇙⇗M⇖" (is "_ ⟹ ?G(p) ≲⇗M⇖ _") for p by (auto intro!:lepoll_rel_eq_trans[OF subset_imp_lepoll_rel] dest:transM) moreover from calculation have "M(p) ⟹ ?G(p) ≺⇗M⇖ ℵ⇘1⇙⇗M⇖" for p using ‹M(G) ⟹ M(p) ⟹ M({A∈G . p ∈ A})› unfolding lesspoll_rel_def by simp moreover from calculation have "M(p) ⟹ ?G(p) ≲⇗M⇖ ω" for p using lesspoll_rel_Aleph_rel_succ[of 0] Aleph_rel_zero by auto moreover have "{A ∈ G . S ∩ A ≠ 0} = (⋃p∈S. ?G(p))" for S by auto moreover from calculation have "M(S) ⟹ i ∈ S ⟹ M({x ∈ G . i ∈ x})" for i S by (auto dest: transM) moreover have "M(S) ⟹ countable_rel(M,S) ⟹ countable_rel(M,{A ∈ G . S ∩ A ≠ 0})" for S proof - from ‹M(G)› interpret M_replacement_lepoll M "λ_ x. Collect(G, (∈)(x))" using countable_lepoll_assms lam_replacement_inj_rel separation_in_rev lam_replacement_Collect'[of G "λx y. x∈y"] mem_F_bound6[of _ G] lam_replacement_minimum separation_in lam_replacement_fst lam_replacement_snd by unfold_locales (auto dest:transM intro:lam_Least_assumption_general[of _ _ _ _ Union]) fix S assume "M(S)" with ‹M(G)› ‹⋀i. M(S) ⟹ i ∈ S ⟹ M({x ∈ G . i ∈ x})› interpret M_cardinal_UN_lepoll _ ?G S using lepoll_assumptions by unfold_locales (auto dest:transM) assume "countable_rel(M,S)" with ‹M(S)› calculation(6) calculation(7,8)[of S] show "countable_rel(M,{A ∈ G . S ∩ A ≠ 0})" using InfCard_rel_nat Card_rel_nat le_Card_rel_iff[THEN iffD2, THEN [3] lepoll_rel_imp_cardinal_rel_UN_le, THEN [4] le_Card_rel_iff[THEN iffD1], of ω] j.UN_closed unfolding countable_rel_def by (auto dest: transM) qed define Disjoint where "Disjoint = {<A,B> ∈ G×G . B ∩ A = 0}" have "Disjoint = {x ∈ G×G . ∃ a b. x=<a,b> ∧ a∩b=0}" unfolding Disjoint_def by force with ‹M(G)› have "M(Disjoint)" using disjoint_separation by simp text‹For every countable\_rel subfamily of \<^term>‹G› there is another some element disjoint from all of them:› have "∃A∈G. ∀S∈X. <S,A>∈Disjoint" if "|X|⇗M⇖ < ℵ⇘1⇙⇗M⇖" "X ⊆ G" "M(X)" for X proof - note ‹n∈ω› ‹M(G)› moreover from this and ‹⋀A. A∈G ⟹ |A|⇗M⇖ = succ(n)› have "|A|⇗M⇖= succ(n)" "M(A)" if "A∈G" for A using that Finite_cardinal_rel_eq_cardinal[of A] Finite_cardinal_rel_iff'[of A] nat_into_Finite transM[of A G] by (auto dest:transM) ultimately have "A∈G ⟹ Finite(A)" for A using cardinal_rel_Card_rel_eqpoll_rel_iff[of "succ(n)" A] Finite_cardinal_rel_eq_cardinal[of A] nat_into_Card_rel[of "succ(n)"] nat_into_M[of n] unfolding Finite_def eqpoll_rel_def by (auto) with ‹X⊆G› ‹M(X)› have "A∈X ⟹ countable_rel(M,A)" for A using Finite_imp_countable_rel by (auto dest: transM) moreover from ‹M(X)› have "M(⋃X)" by simp moreover note ‹|X|⇗M⇖ < ℵ⇘1⇙⇗M⇖› ‹M(X)› ultimately have "countable_rel(M,⋃X)" using Card_rel_nat[THEN cardinal_rel_lt_csucc_rel_iff, of X] countable_rel_union_countable_rel[of X] countable_rel_iff_cardinal_rel_le_nat[of X] Aleph_rel_succ Aleph_rel_zero by simp with ‹M(⋃X)› ‹M(_) ⟹ countable_rel(M,_) ⟹ countable_rel(M,{A ∈ G . _ ∩ A ≠ 0})› have "countable_rel(M,{A ∈ G . (⋃X) ∩ A ≠ 0})" by simp with ‹G ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(G)› obtain B where "B∈G" "B ∉ {A ∈ G . (⋃X) ∩ A ≠ 0}" using nat_lt_Aleph_rel1 cardinal_rel_Card_rel_eqpoll_rel_iff[of "ℵ⇘1⇙⇗M⇖" G] uncountable_rel_not_subset_countable_rel [of "{A ∈ G . (⋃X) ∩ A ≠ 0}" G] uncountable_rel_iff_nat_lt_cardinal_rel[of G] by force then have "∃A∈G. ∀S∈X. A ∩ S = 0" by auto with ‹X⊆G› show "∃A∈G. ∀S∈X. <S,A>∈Disjoint" unfolding Disjoint_def using subsetD by simp qed moreover from ‹G ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(G)› obtain b where "b∈G" using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1 uncountable_rel_not_empty by blast ultimately text‹Hence, the hypotheses to perform a bounded-cardinal selection are satisfied,› obtain S where "S:ℵ⇘1⇙⇗M⇖→⇗M⇖G" "α∈ℵ⇘1⇙⇗M⇖ ⟹ β∈ℵ⇘1⇙⇗M⇖ ⟹ α<β ⟹ <S`α, S`β> ∈Disjoint" for α β using bounded_cardinal_rel_selection[of "ℵ⇘1⇙⇗M⇖" G Disjoint] ‹M(Disjoint)› by force moreover from this ‹n∈ω› ‹M(G)› have inM:"M(S)" "M(n)" "⋀x. x ∈ ℵ⇘1⇙⇗M⇖ ⟹ S ` x ∈ G" "⋀x. x ∈ ℵ⇘1⇙⇗M⇖ ⟹ M(x)" using function_space_rel_char by (auto dest: transM) ultimately have "α ∈ ℵ⇘1⇙⇗M⇖ ⟹ β ∈ ℵ⇘1⇙⇗M⇖ ⟹ α≠β ⟹ S`α ∩ S`β = 0" for α β unfolding Disjoint_def using lt_neq_symmetry[of "ℵ⇘1⇙⇗M⇖" "λα β. S`α ∩ S`β = 0"] Card_rel_is_Ord by auto (blast) text‹and a symmetry argument shows that obtained \<^term>‹S› is an injective \<^term>‹ℵ⇘1⇙⇗M⇖›-sequence of disjoint elements of \<^term>‹G›.› moreover from this and ‹⋀A. A∈G ⟹ |A|⇗M⇖ = succ(n)› inM ‹S : ℵ⇘1⇙⇗M⇖ →⇗M⇖ G› ‹M(G)› have "S ∈ inj_rel(M,ℵ⇘1⇙⇗M⇖, G)" using def_inj_rel[OF Aleph_rel_closed ‹M(G)›, of 1] proof (clarsimp) fix w x from inM have "a ∈ ℵ⇘1⇙⇗M⇖ ⟹ b ∈ ℵ⇘1⇙⇗M⇖ ⟹ a ≠ b ⟹ S ` a ≠ S ` b" for a b using ‹⋀A. A∈G ⟹ |A|⇗M⇖ = succ(n)›[THEN [4] cardinal_rel_succ_not_0[THEN [4] Int_eq_zero_imp_not_eq[OF calculation, of "ℵ⇘1⇙⇗M⇖" "λx. x"], of "λ_.n"], OF _ _ _ _ apply_closed] by auto moreover assume "w ∈ ℵ⇘1⇙⇗M⇖" "x ∈ ℵ⇘1⇙⇗M⇖" "S ` w = S ` x" ultimately show "w = x" by blast qed moreover from this ‹M(G)› have "range(S) ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" using inj_rel_bij_rel_range eqpoll_rel_sym unfolding eqpoll_rel_def by (blast dest: transM) moreover note ‹M(G)› moreover from calculation have "range(S) ⊆ G" using inj_rel_is_fun range_fun_subset_codomain by (fastforce dest: transM) moreover note ‹M(S)› ultimately show "∃D[M]. D ⊆ G ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" using inj_rel_is_fun ZF_Library.range_eq_image[of S "ℵ⇘1⇙⇗M⇖" G] image_function[OF fun_is_function, OF inj_rel_is_fun, of S "ℵ⇘1⇙⇗M⇖" G] domain_of_fun[OF inj_rel_is_fun, of S "ℵ⇘1⇙⇗M⇖" G] apply_replacement[of S] by (rule_tac x="S``ℵ⇘1⇙⇗M⇖" in rexI) (auto dest:transM intro!:RepFun_closed) text‹This finishes the successor case and hence the proof.› qed qed with ‹G ⊆ F› show ?thesis by blast qed lemma delta_system_uncountable_rel: assumes "∀A∈F. Finite(A)" "uncountable_rel(M,F)" "M(F)" shows "∃D[M]. D ⊆ F ∧ delta_system(D) ∧ D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" proof - from assms obtain S where "S ⊆ F" "S ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(S)" using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1[of F] by auto moreover from ‹∀A∈F. Finite(A)› and this have "∀A∈S. Finite(A)" by auto ultimately show ?thesis using delta_system_Aleph_rel1[of S] by (auto dest:transM) qed end ― ‹\<^locale>‹M_delta›› end