Theory Delta_System_Relative
section‹The Delta System Lemma, Relativized\label{sec:dsl-rel}›
theory Delta_System_Relative
imports
Cardinal_Library_Relative
begin
definition
delta_system :: "i ⇒ o" where
"delta_system(D) ≡ ∃r. ∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
lemma delta_systemI [intro]:
assumes "∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
shows "delta_system(D)"
using assms unfolding delta_system_def by simp
lemma delta_systemD [dest]:
"delta_system(D) ⟹ ∃r. ∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
unfolding delta_system_def by simp
lemma delta_system_root_eq_Inter :
assumes "delta_system(D)"
shows "∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = ⋂D"
proof (clarify, intro equalityI, auto)
fix A' B' x C
assume hyp:"A'∈D" "B'∈ D" "A'≠B'" "x∈A'" "x∈B'" "C∈D"
with assms
obtain r where delta:"∀A∈D. ∀B∈D. A ≠ B ⟶ A ∩ B = r"
by auto
show "x ∈ C"
proof (cases "C=A'")
case True
with hyp and assms
show ?thesis by simp
next
case False
moreover
note hyp
moreover from calculation and delta
have "r = C ∩ A'" "A' ∩ B' = r" "x∈r" by auto
ultimately
show ?thesis by simp
qed
qed
relativize functional "delta_system" "delta_system_rel" external
locale M_delta= M_cardinal_library +
assumes
cardinal_replacement:"strong_replacement(M, λA y. y = ⟨A, |A|⇗M⇖⟩)"
and
countable_lepoll_assms:
"M(G) ⟹ separation(M, λp. ∀x∈G. x ∈ snd(p) ⟷ fst(p) ∈ x)"
"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)⟩)"
and
disjoint_separation: "M(c) ⟹ separation(M, λ x. ∃a. ∃b. x=⟨a,b⟩ ∧ a ∩ b = c)"
begin
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 ‹M(F)›
have "M(λA∈F. |A|⇗M⇖)"
using cardinal_replacement
by (rule_tac lam_closed) (auto dest:transM)
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
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
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]
apply auto[1]
using cardinal_rel_eqpoll_rel_iff[of D "ℵ⇘1⇙⇗M⇖"] ‹M(D)› ‹D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖›
by simp
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⇖)›
‹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_plus_one[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(2-) lam_replacement_inj_rel separation_in_rev
lam_replacement_Collect[OF _ _ countable_lepoll_assms(1)] mem_F_bound6[of _ G]
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] leqpoll_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)›
find_theorems "M(?S) ⟹ strong_replacement(M, λx y. y = ?S ` x)"
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
end