Theory Cardinal_Library_Relative
section‹Cardinal Arithmetic under Choice\label{sec:cardinal-lib-rel}›
theory Cardinal_Library_Relative
imports
ZF_Library_Relative
"Delta_System_Lemma.ZF_Library"
Replacement_Lepoll
begin
locale M_library= M_ZF_library + M_cardinal_AC
begin
declare eqpoll_rel_refl [simp]
subsection‹Miscellaneous›
lemma cardinal_rel_RepFun_le :
assumes "S ∈ A→B" "M(S)" "M(A)" "M(B)"
shows "|{S`a . a∈A}|⇗M⇖ ≤ |A|⇗M⇖"
proof -
note assms
moreover from this
have "{S ` a . a ∈ A} = S``A"
using image_eq_UN RepFun_def UN_iff by force
moreover from calculation
have "M(λx∈A. S ` x)" "M({S ` a . a ∈ A})"
using lam_closed[of "λ x. S`x"] apply_type[OF ‹S∈_›]
transM[OF _ ‹M(B)›] image_closed
by auto
moreover from assms this
have "(λx∈A. S`x) ∈ surj_rel(M,A, {S`a . a∈A})"
using mem_surj_abs lam_funtype[of A "λx . S`x"]
unfolding surj_def by auto
ultimately
show ?thesis
using surj_rel_char surj_rel_implies_cardinal_rel_le by simp
qed
lemma subset_imp_le_cardinal_rel : "A ⊆ B ⟹ M(A) ⟹ M(B) ⟹ |A|⇗M⇖ ≤ |B|⇗M⇖"
using subset_imp_lepoll_rel[THEN lepoll_rel_imp_cardinal_rel_le] .
lemma lt_cardinal_rel_imp_not_subset : "|A|⇗M⇖ < |B|⇗M⇖ ⟹ M(A) ⟹ M(B) ⟹ ¬ B ⊆ A"
using subset_imp_le_cardinal_rel le_imp_not_lt by blast
lemma cardinal_rel_lt_csucc_rel_iff :
"Card_rel(M,K) ⟹ M(K) ⟹ M(K') ⟹ |K'|⇗M⇖ < (K⇧+)⇗M⇖ ⟷ |K'|⇗M⇖ ≤ K"
by (simp add: Card_rel_lt_csucc_rel_iff)
lemmas inj_rel_is_fun= inj_is_fun[OF mem_inj_rel]
lemma inj_rel_bij_rel_range : "f ∈ inj⇗M⇖(A,B) ⟹ M(A) ⟹ M(B) ⟹ f ∈ bij⇗M⇖(A,range(f))"
using bij_rel_char inj_rel_char inj_bij_range by force
lemma bij_rel_is_inj_rel : "f ∈ bij⇗M⇖(A,B) ⟹ M(A) ⟹ M(B) ⟹ f ∈ inj⇗M⇖(A,B)"
unfolding bij_rel_def by simp
lemma inj_rel_weaken_type : "[| f ∈ inj⇗M⇖(A,B); B⊆D; M(A); M(B); M(D) |] ==> f ∈ inj⇗M⇖(A,D)"
using inj_rel_char inj_rel_is_fun inj_weaken_type by auto
lemma bij_rel_converse_bij_rel [TC]: "f ∈ bij⇗M⇖(A,B) ⟹ M(A) ⟹ M(B) ==> converse(f): bij⇗M⇖(B,A)"
using bij_rel_char by force
lemma bij_rel_is_fun_rel : "f ∈ bij⇗M⇖(A,B) ⟹ M(A) ⟹ M(B) ⟹ f ∈ A→⇗M⇖B"
using bij_rel_char mem_function_space_rel_abs bij_is_fun by simp
lemmas bij_rel_is_fun= bij_rel_is_fun_rel[THEN mem_function_space_rel]
lemma comp_bij_rel :
"g ∈ bij⇗M⇖(A,B) ⟹ f ∈ bij⇗M⇖(B,C) ⟹ M(A) ⟹ M(B) ⟹ M(C) ⟹ (f O g) ∈ bij⇗M⇖(A,C)"
using bij_rel_char comp_bij by force
lemma inj_rel_converse_fun : "f ∈ inj⇗M⇖(A,B) ⟹ M(A) ⟹ M(B) ⟹ converse(f) ∈ range(f)→⇗M⇖A"
proof -
assume "f ∈ inj⇗M⇖(A,B)" "M(A)" "M(B)"
then
have "M(f)" "M(converse(f))" "M(range(f))" "f∈inj(A,B)"
using inj_rel_char converse_closed range_closed
by auto
then
show ?thesis
using inj_converse_inj function_space_rel_char inj_is_fun ‹M(A)› by auto
qed
end
locale M_cardinal_UN_nat= M_cardinal_UN _ ω X for X
begin
lemma cardinal_rel_UN_le_nat :
assumes "⋀i. i∈ω ⟹ |X(i)|⇗M⇖ ≤ ω"
shows "|⋃i∈ω. X(i)|⇗M⇖ ≤ ω"
proof -
from assms
show ?thesis
by (simp add: cardinal_rel_UN_le InfCard_rel_nat)
qed
end
locale M_cardinal_UN_inj= M_library +
j:M_cardinal_UN _ J +
y:M_cardinal_UN _ K "λk. if k∈range(f) then X(converse(f)`k) else 0" for J K f +
assumes
f_inj: "f ∈ inj_rel(M,J,K)"
begin
lemma inj_rel_imp_cardinal_rel_UN_le :
notes [dest] = InfCard_is_Card Card_is_Ord
fixes Y
defines "Y(k) ≡ if k∈range(f) then X(converse(f)`k) else 0"
assumes "InfCard⇗M⇖(K)" "⋀i. i∈J ⟹ |X(i)|⇗M⇖ ≤ K"
shows "|⋃i∈J. X(i)|⇗M⇖ ≤ K"
proof -
have "M(K)" "M(J)" "⋀w x. w ∈ X(x) ⟹ M(x)"
using y.Pi_assumptions j.Pi_assumptions j.X_witness_in_M by simp_all
then
have "M(f)"
using inj_rel_char f_inj by simp
note inM = ‹M(f)› ‹M(K)› ‹M(J)› ‹⋀w x. w ∈ X(x) ⟹ M(x)›
have "i∈J ⟹ f`i ∈ K" for i
using inj_rel_is_fun[OF f_inj] apply_type
function_space_rel_char by (auto simp add:inM)
have "(⋃i∈J. X(i)) ⊆ (⋃i∈K. Y(i))"
proof (standard, elim UN_E)
fix x i
assume "i∈J" "x∈X(i)"
with ‹i∈J ⟹ f`i ∈ K›
have "x ∈ Y(f`i)" "f`i ∈ K"
unfolding Y_def
using inj_is_fun right_inverse f_inj
by (auto simp add:inM Y_def intro: apply_rangeI)
then
show "x ∈ (⋃i∈K. Y(i))" by auto
qed
then
have "|⋃i∈J. X(i)|⇗M⇖ ≤ |⋃i∈K. Y(i)|⇗M⇖"
using subset_imp_le_cardinal_rel j.UN_closed y.UN_closed
unfolding Y_def by (simp add:inM)
moreover
note assms ‹⋀i. i∈J ⟹ f`i ∈ K› inM
moreover from this
have "k∈range(f) ⟹ converse(f)`k ∈ J" for k
using inj_rel_converse_fun[OF f_inj]
range_fun_subset_codomain function_space_rel_char by simp
ultimately
show "|⋃i∈J. X(i)|⇗M⇖ ≤ K"
using InfCard_rel_is_Card_rel[THEN Card_rel_is_Ord,THEN Ord_0_le, of K]
by (rule_tac le_trans[OF _ y.cardinal_rel_UN_le])
(auto intro:Ord_0_le simp:Y_def)+
qed
end
locale M_cardinal_UN_lepoll= M_library + M_replacement_lepoll _ "λ_. X" +
j:M_cardinal_UN _ J for J
begin
lemma leqpoll_rel_imp_cardinal_rel_UN_le :
notes [dest] = InfCard_is_Card Card_is_Ord
assumes "InfCard⇗M⇖(K)" "J ≲⇗M⇖ K" "⋀i. i∈J ⟹ |X(i)|⇗M⇖ ≤ K"
"M(K)"
shows "|⋃i∈J. X(i)|⇗M⇖ ≤ K"
proof -
from ‹J ≲⇗M⇖ K›
obtain f where "f ∈ inj_rel(M,J,K)" "M(f)" by blast
moreover
let ?Y="λk. if k∈range(f) then X(converse(f)`k) else 0"
note ‹M(K)›
moreover from calculation
have "k ∈ range(f) ⟹ converse(f)`k ∈ J" for k
using mem_inj_rel[THEN inj_converse_fun, THEN apply_type]
j.Pi_assumptions by blast
moreover from ‹M(f)›
have "w ∈ ?Y(x) ⟹ M(x)" for w x
by (cases "x∈range(f)") (auto dest:transM)
moreover from calculation
interpret M_Pi_assumptions_choice _ K ?Y
using j.Pi_assumptions lepoll_assumptions
proof (unfold_locales, auto dest:transM)
show "strong_replacement(M, λy z. False)"
unfolding strong_replacement_def by auto
qed
from calculation
interpret M_cardinal_UN_inj _ _ _ _ f
using lepoll_assumptions
by unfold_locales auto
from assms
show ?thesis using inj_rel_imp_cardinal_rel_UN_le by simp
qed
end
context M_library
begin
lemma cardinal_rel_lt_csucc_rel_iff' :
includes Ord_dests
assumes "Card_rel(M,κ)"
and types:"M(κ)" "M(X)"
shows "κ < |X|⇗M⇖ ⟷ (κ⇧+)⇗M⇖ ≤ |X|⇗M⇖"
using assms cardinal_rel_lt_csucc_rel_iff[of κ X] Card_rel_csucc_rel[of κ]
not_le_iff_lt[of "(κ⇧+)⇗M⇖" "|X|⇗M⇖"] not_le_iff_lt[of "|X|⇗M⇖" κ]
by blast
lemma lepoll_rel_imp_subset_bij_rel :
assumes "M(X)" "M(Y)"
shows "X ≲⇗M⇖ Y ⟷ (∃Z[M]. Z ⊆ Y ∧ Z ≈⇗M⇖ X)"
proof
assume "X ≲⇗M⇖ Y"
then
obtain j where "j ∈ inj_rel(M,X,Y)"
by blast
with assms
have "range(j) ⊆ Y" "j ∈ bij_rel(M,X,range(j))" "M(range(j))" "M(j)"
using inj_rel_bij_rel_range inj_rel_char
inj_rel_is_fun[THEN range_fun_subset_codomain,of j X Y]
by auto
with assms
have "range(j) ⊆ Y" "X ≈⇗M⇖ range(j)"
unfolding eqpoll_rel_def by auto
with assms ‹M(j)›
show "∃Z[M]. Z ⊆ Y ∧ Z ≈⇗M⇖ X"
using eqpoll_rel_sym[OF ‹X ≈⇗M⇖ range(j)›]
by auto
next
assume "∃Z[M]. Z ⊆ Y ∧ Z ≈⇗M⇖ X"
then
obtain Z f where "f ∈ bij_rel(M,Z,X)" "Z ⊆ Y" "M(Z)" "M(f)"
unfolding eqpoll_rel_def by blast
with assms
have "converse(f) ∈ inj_rel(M,X,Y)" "M(converse(f))"
using inj_rel_weaken_type[OF bij_rel_converse_bij_rel[THEN bij_rel_is_inj_rel],of f Z X Y]
by auto
then
show "X ≲⇗M⇖ Y"
unfolding lepoll_rel_def by auto
qed
text‹The following result proves to be very useful when combining
\<^term>‹cardinal_rel› and \<^term>‹eqpoll_rel› in a calculation.›
lemma cardinal_rel_Card_rel_eqpoll_rel_iff :
"Card_rel(M,κ) ⟹ M(κ) ⟹ M(X) ⟹ |X|⇗M⇖ = κ ⟷ X ≈⇗M⇖ κ"
using Card_rel_cardinal_rel_eq[of κ] cardinal_rel_eqpoll_rel_iff[of X κ] by auto
lemma lepoll_rel_imp_lepoll_rel_cardinal_rel :
assumes"X ≲⇗M⇖ Y" "M(X)" "M(Y)"
shows "X ≲⇗M⇖ |Y|⇗M⇖"
using assms cardinal_rel_Card_rel_eqpoll_rel_iff[of "|Y|⇗M⇖" Y]
Card_rel_cardinal_rel
lepoll_rel_eq_trans[of _ _ "|Y|⇗M⇖"] by simp
lemma lepoll_rel_Un :
assumes "InfCard_rel(M,κ)" "A ≲⇗M⇖ κ" "B ≲⇗M⇖ κ" "M(A)" "M(B)" "M(κ)"
shows "A ∪ B ≲⇗M⇖ κ"
proof -
from assms
have "A ∪ B ≲⇗M⇖ sum(A,B)"
using Un_lepoll_rel_sum by simp
moreover
note assms
moreover from this
have "|sum(A,B)|⇗M⇖ ≤ κ ⊕⇗M⇖ κ"
using sum_lepoll_rel_mono[of A κ B κ] lepoll_rel_imp_cardinal_rel_le
unfolding cadd_rel_def by auto
ultimately
show ?thesis
using InfCard_rel_cdouble_eq Card_rel_cardinal_rel_eq
InfCard_rel_is_Card_rel Card_rel_le_imp_lepoll_rel[of "sum(A,B)" κ]
lepoll_rel_trans[of "A∪B"]
by auto
qed
lemma cardinal_rel_Un_le :
assumes "InfCard_rel(M,κ)" "|A|⇗M⇖ ≤ κ" "|B|⇗M⇖ ≤ κ" "M(κ)" "M(A)" "M(B)"
shows "|A ∪ B|⇗M⇖ ≤ κ"
using assms lepoll_rel_Un le_Card_rel_iff InfCard_rel_is_Card_rel by auto
lemma eqpoll_rel_imp_Finite : "A ≈⇗M⇖ B ⟹ Finite(A) ⟹ M(A) ⟹ M(B) ⟹ Finite(B)"
proof -
assume "A ≈⇗M⇖ B" "Finite(A)" "M(A)" "M(B)"
then obtain f n g where "f∈bij(A,B)" "n∈ω" "g∈bij(A,n)"
unfolding Finite_def eqpoll_def eqpoll_rel_def
using bij_rel_char
by auto
then
have "g O converse(f) ∈ bij(B,n)"
using bij_converse_bij comp_bij by simp
with ‹n∈_›
show"Finite(B)"
unfolding Finite_def eqpoll_def by auto
qed
lemma eqpoll_rel_imp_Finite_iff : "A ≈⇗M⇖ B ⟹ M(A) ⟹ M(B) ⟹ Finite(A) ⟷ Finite(B)"
using eqpoll_rel_imp_Finite eqpoll_rel_sym by force
lemma Finite_cardinal_rel_iff' : "M(i) ⟹ Finite(|i|⇗M⇖) ⟷ Finite(i)"
using eqpoll_rel_imp_Finite_iff[OF cardinal_rel_eqpoll_rel]
by auto
lemma cardinal_rel_subset_of_Card_rel :
assumes "Card_rel(M,γ)" "a ⊆ γ" "M(a)" "M(γ)"
shows "|a|⇗M⇖ < γ ∨ |a|⇗M⇖ = γ"
proof -
from assms
have "|a|⇗M⇖ < |γ|⇗M⇖ ∨ |a|⇗M⇖ = |γ|⇗M⇖"
using subset_imp_le_cardinal_rel[THEN le_iff[THEN iffD1]] by simp
with assms
show ?thesis
using Card_rel_cardinal_rel_eq by auto
qed
lemma cardinal_rel_cases :
includes Ord_dests
assumes "M(γ)" "M(X)"
shows "Card_rel(M,γ) ⟹ |X|⇗M⇖ < γ ⟷ ¬ |X|⇗M⇖ ≥ γ"
using assms not_le_iff_lt Card_rel_is_Ord Ord_cardinal_rel
by auto
end
subsection‹Countable and uncountable sets›
definition
countable :: "i⇒o" where
"countable(X) ≡ X ≲ ω"
relativize functional "countable" "countable_rel" external
relationalize "countable_rel" "is_countable"
context M_library
begin
lemma countableI [intro]: "X ≲⇗M⇖ ω ⟹ countable_rel(M,X)"
unfolding countable_rel_def by simp
lemma countableD [dest]: "countable_rel(M,X) ⟹ X ≲⇗M⇖ ω"
unfolding countable_rel_def by simp
lemma countable_rel_iff_cardinal_rel_le_nat : "M(X) ⟹ countable_rel(M,X) ⟷ |X|⇗M⇖ ≤ ω"
using le_Card_rel_iff[of ω X] Card_rel_nat
unfolding countable_rel_def by simp
lemma lepoll_rel_countable_rel : "X ≲⇗M⇖ Y ⟹ countable_rel(M,Y) ⟹ M(X) ⟹ M(Y) ⟹ countable_rel(M,X)"
using lepoll_rel_trans[of X Y] by blast
lemma surj_rel_countable_rel :
"countable_rel(M,X) ⟹ f ∈ surj_rel(M,X,Y) ⟹ M(X) ⟹ M(Y) ⟹ M(f) ⟹ countable_rel(M,Y)"
using surj_rel_implies_cardinal_rel_le[of f X Y, THEN le_trans]
countable_rel_iff_cardinal_rel_le_nat by simp
lemma Finite_imp_countable_rel : "Finite_rel(M,X) ⟹ M(X) ⟹ countable_rel(M,X)"
unfolding Finite_rel_def
by (auto intro:InfCard_rel_nat nats_le_InfCard_rel[of _ ω,
THEN le_imp_lepoll_rel] dest!:eq_lepoll_rel_trans[of X _ ω] )
end
lemma (in M_cardinal_UN_lepoll) countable_rel_imp_countable_rel_UN :
assumes "countable_rel(M,J)" "⋀i. i∈J ⟹ countable_rel(M,X(i))"
shows "countable_rel(M,⋃i∈J. X(i))"
using assms leqpoll_rel_imp_cardinal_rel_UN_le[of ω] InfCard_rel_nat
InfCard_rel_is_Card_rel j.UN_closed
countable_rel_iff_cardinal_rel_le_nat j.Pi_assumptions
Card_rel_le_imp_lepoll_rel[of J ω] Card_rel_cardinal_rel_eq[of ω]
by auto
locale M_cardinal_library= M_library + M_replacement +
assumes
lam_replacement_inj_rel:"lam_replacement(M, λx. inj⇗M⇖(fst(x),snd(x)))"
and
cardinal_lib_assms1:
"M(A) ⟹ M(b) ⟹ M(f) ⟹
separation(M, λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λx. if M(x) then x else 0,b,f,i)⟩)"
"separation(M,Ord)"
and
cardinal_lib_assms2:
"M(A') ⟹ M(G) ⟹ M(b) ⟹ M(f) ⟹
separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. if M(a) then G`a else 0,b,f,i)⟩)"
and
cardinal_lib_assms3:
"M(A') ⟹ M(b) ⟹ M(f) ⟹ M(F) ⟹
separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. if M(a) then F-``{a} else 0,b,f,i)⟩)"
and
cdlt_assms:
"M(G) ⟹ M(Q) ⟹ separation(M, λp. ∀x∈G. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ Q))"
"M(x) ⟹ M(Q) ⟹ separation(M, λa . ∀s∈x. ⟨s, a⟩ ∈ Q)"
and
cardinal_lib_assms5 :
"M(γ) ⟹ separation(M, λZ . cardinal_rel(M,Z) < γ)"
and
cardinal_lib_assms6:
"M(f) ⟹ M(β) ⟹ Ord(β) ⟹
strong_replacement(M, λx y. x∈β ∧ y = ⟨x, transrec(x, λa g. f ` (g `` a))⟩)"
"separation(M, λ x . ∃a. ∃b . x=⟨a,b⟩ ∧ a≠b)"
begin
lemma countable_rel_union_countable_rel :
assumes "⋀x. x ∈ C ⟹ countable_rel(M,x)" "countable_rel(M,C)" "M(C)"
shows "countable_rel(M,⋃C)"
proof -
have "x ∈ (if M(i) then i else 0) ⟹ M(i)" for x i
by (cases "M(i)") auto
then
interpret M_replacement_lepoll M "λ_ x. if M(x) then x else 0"
using lam_replacement_if[OF lam_replacement_identity
lam_replacement_constant[OF nonempty], where b=M] lam_replacement_inj_rel
apply unfold_locales apply (auto simp add: separation_def)
proof -
fix b f
assume "M(b)" "M(f)"
show "lam_replacement(M, λx. μ i. x ∈ if_range_F_else_F(λx. if M(x) then x else 0, b, f, i))"
proof (cases "b=0")
case True
with ‹M(f)›
show ?thesis
using cardinal_lib_assms1
by (simp_all; rule_tac lam_Least_assumption_ifM_b0)+
next
case False
with ‹M(f)› ‹M(b)›
show ?thesis
using cardinal_lib_assms1
by (rule_tac lam_Least_assumption_ifM_bnot0) auto
qed
qed
note ‹M(C)›
moreover
have "w ∈ (if M(x) then x else 0) ⟹ M(x)" for w x
by (cases "M(x)") auto
ultimately
interpret M_cardinal_UN_lepoll _ "λc. if M(c) then c else 0" C
using lepoll_assumptions
by unfold_locales simp_all
have "(if M(i) then i else 0) = i" if "i∈C" for i
using transM[OF _ ‹M(C)›] that by simp
then
show ?thesis
using assms countable_rel_imp_countable_rel_UN by simp
qed
end
abbreviation
uncountable_rel :: "[i⇒o,i]⇒o" where
"uncountable_rel(M,X) ≡ ¬ countable_rel(M,X)"
context M_cardinal_library
begin
lemma uncountable_rel_iff_nat_lt_cardinal_rel :
"M(X) ⟹ uncountable_rel(M,X) ⟷ ω < |X|⇗M⇖"
using countable_rel_iff_cardinal_rel_le_nat not_le_iff_lt by simp
lemma uncountable_rel_not_empty : "uncountable_rel(M,X) ⟹ X ≠ 0"
using empty_lepoll_relI by auto
lemma uncountable_rel_imp_Infinite : "uncountable_rel(M,X) ⟹ M(X) ⟹ Infinite(X)"
using uncountable_rel_iff_nat_lt_cardinal_rel[of X] lepoll_rel_nat_imp_Infinite[of X]
cardinal_rel_le_imp_lepoll_rel[of ω X] leI
by simp
lemma uncountable_rel_not_subset_countable_rel :
assumes "countable_rel(M,X)" "uncountable_rel(M,Y)" "M(X)" "M(Y)"
shows "¬ (Y ⊆ X)"
using assms lepoll_rel_trans subset_imp_lepoll_rel[of Y X]
by blast
subsection‹Results on Aleph\_rels›
lemma nat_lt_Aleph_rel1 : "ω < ℵ⇘1⇙⇗M⇖"
by (simp add: Aleph_rel_succ Aleph_rel_zero lt_csucc_rel)
lemma zero_lt_Aleph_rel1 : "0 < ℵ⇘1⇙⇗M⇖"
by (rule lt_trans[of _ "ω"], auto simp add: ltI nat_lt_Aleph_rel1)
lemma le_Aleph_rel1_nat : "M(k) ⟹ Card_rel(M,k) ⟹ k<ℵ⇘1⇙⇗M⇖ ⟹ k ≤ ω"
by (simp add: Aleph_rel_succ Aleph_rel_zero Card_rel_lt_csucc_rel_iff Card_rel_nat)
lemma lesspoll_rel_Aleph_rel_plus_one :
assumes "Ord(α)"
and types:"M(α)" "M(d)"
shows "d ≺⇗M⇖ ℵ⇘succ(α)⇙⇗M⇖ ⟷ d ≲⇗M⇖ ℵ⇘α⇙⇗M⇖"
using assms Aleph_rel_succ Card_rel_is_Ord Ord_Aleph_rel lesspoll_rel_csucc_rel
by simp
lemma cardinal_rel_Aleph_rel [simp]: "Ord(α) ⟹ M(α) ⟹ |ℵ⇘α⇙⇗M⇖|⇗M⇖ = ℵ⇘α⇙⇗M⇖"
using Card_rel_cardinal_rel_eq by simp
lemma Aleph_rel_lesspoll_rel_increasing :
includes Aleph_rel_intros
assumes "M(b)" "M(a)"
shows "a < b ⟹ ℵ⇘a⇙⇗M⇖ ≺⇗M⇖ ℵ⇘b⇙⇗M⇖"
using assms
cardinal_rel_lt_iff_lesspoll_rel[of "ℵ⇘a⇙⇗M⇖" "ℵ⇘b⇙⇗M⇖"]
Aleph_rel_increasing[of a b] Card_rel_cardinal_rel_eq[of "ℵ⇘b⇙"]
lt_Ord lt_Ord2 Card_rel_Aleph_rel[THEN Card_rel_is_Ord]
by auto
lemma uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1 :
includes Ord_dests
assumes "M(X)"
notes Aleph_rel_zero[simp] Card_rel_nat[simp] Aleph_rel_succ[simp]
shows "uncountable_rel(M,X) ⟷ (∃S[M]. S ⊆ X ∧ S ≈⇗M⇖ ℵ⇘1⇙⇗M⇖)"
proof
assume "uncountable_rel(M,X)"
with ‹M(X)›
have "ℵ⇘1⇙⇗M⇖ ≲⇗M⇖ X"
using uncountable_rel_iff_nat_lt_cardinal_rel cardinal_rel_lt_csucc_rel_iff'
cardinal_rel_le_imp_lepoll_rel by auto
with ‹M(X)›
obtain S where "M(S)" "S ⊆ X" "S ≈⇗M⇖ ℵ⇘1⇙⇗M⇖"
using lepoll_rel_imp_subset_bij_rel by auto
then
show "∃S[M]. S ⊆ X ∧ S ≈⇗M⇖ ℵ⇘1⇙⇗M⇖"
using cardinal_rel_cong Card_rel_csucc_rel[of ω] Card_rel_cardinal_rel_eq by auto
next
note Aleph_rel_lesspoll_rel_increasing[of 1 0,simplified]
assume "∃S[M]. S ⊆ X ∧ S ≈⇗M⇖ ℵ⇘1⇙⇗M⇖"
moreover
have eq:"ℵ⇘1⇙⇗M⇖ = (ω⇧+)⇗M⇖" by auto
moreover from calculation ‹M(X)›
have A:"(ω⇧+)⇗M⇖ ≲⇗M⇖ X"
using subset_imp_lepoll_rel[THEN [2] eq_lepoll_rel_trans, of "ℵ⇘1⇙⇗M⇖" _ X,
OF eqpoll_rel_sym] by auto
with ‹M(X)›
show "uncountable_rel(M,X)"
using
lesspoll_rel_trans1[OF lepoll_rel_trans[OF A _] ‹ω ≺⇗M⇖ (ω⇧+)⇗M⇖›]
lesspoll_rel_not_refl
by auto
qed
lemma UN_if_zero : "M(K) ⟹ (⋃x∈K. if M(x) then G ` x else 0) =(⋃x∈K. G ` x)"
using transM[of _ K] by auto
lemma mem_F_bound1 :
fixes F G
defines "F ≡ λ_ x. if M(x) then G`x else 0"
shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ domain(G) )"
using apply_0 unfolding F_def
by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)
lemma lt_Aleph_rel_imp_cardinal_rel_UN_le_nat : "function(G) ⟹ domain(G) ≲⇗M⇖ ω ⟹
∀n∈domain(G). |G`n|⇗M⇖<ℵ⇘1⇙⇗M⇖ ⟹ M(G) ⟹ |⋃n∈domain(G). G`n|⇗M⇖≤ω"
proof -
assume "M(G)"
moreover from this
have "x ∈ (if M(i) then G ` i else 0) ⟹ M(i)" for x i
by (cases "M(i)") auto
moreover
have "separation(M, M)" unfolding separation_def by auto
ultimately
interpret M_replacement_lepoll M "λ_ x. if M(x) then G`x else 0"
using lam_replacement_inj_rel cardinal_lib_assms2 mem_F_bound1[of _ _ G]
lam_if_then_replacement_apply
by (unfold_locales, simp_all)
(rule lam_Least_assumption_general[where U="λ_. domain(G)"], auto)
note ‹M(G)›
moreover
have "w ∈ (if M(x) then G ` x else 0) ⟹ M(x)" for w x
by (cases "M(x)") auto
ultimately
interpret M_cardinal_UN_lepoll _ "λn. if M(n) then G`n else 0" "domain(G)"
using lepoll_assumptions1[where S="domain(G)",unfolded lepoll_assumptions1_def]
cardinal_lib_assms2 lepoll_assumptions
by (unfold_locales, auto)
assume "function(G)"
let ?N="domain(G)" and ?R="⋃n∈domain(G). G`n"
assume "?N ≲⇗M⇖ ω"
assume Eq1: "∀n∈?N. |G`n|⇗M⇖<ℵ⇘1⇙⇗M⇖"
{
fix n
assume "n∈?N"
with Eq1 ‹M(G)›
have "|G`n|⇗M⇖ ≤ ω"
using le_Aleph_rel1_nat[of "|G ` n|⇗M⇖"] leqpoll_rel_imp_cardinal_rel_UN_le
UN_if_zero[of "domain(G)" G]
by (auto dest:transM)
}
then
have "n∈?N ⟹ |G`n|⇗M⇖ ≤ ω" for n .
moreover
note ‹?N ≲⇗M⇖ ω› ‹M(G)›
moreover
have "(if M(i) then G ` i else 0) ⊆ G ` i" for i
by auto
with ‹M(G)›
have "|if M(i) then G ` i else 0|⇗M⇖ ≤ |G ` i|⇗M⇖" for i
proof(cases "M(i)")
case True
with ‹M(G)› show ?thesis using Ord_cardinal_rel[OF apply_closed]
by simp
next
case False
then
have "i∉domain(G)"
using transM[OF _ domain_closed[OF ‹M(G)›]] by auto
then
show ?thesis
using Ord_cardinal_rel[OF apply_closed] apply_0 by simp
qed
ultimately
show ?thesis
using InfCard_rel_nat leqpoll_rel_imp_cardinal_rel_UN_le[of ω]
UN_if_zero[of "domain(G)" G]
le_trans[of "|if M(_) then G ` _ else 0|⇗M⇖" "|G ` _|⇗M⇖" ω]
by auto blast
qed
lemma Aleph_rel1_eq_cardinal_rel_vimage : "f:ℵ⇘1⇙⇗M⇖→⇗M⇖ω ⟹ ∃n∈ω. |f-``{n}|⇗M⇖ = ℵ⇘1⇙⇗M⇖"
proof -
assume "f:ℵ⇘1⇙⇗M⇖→⇗M⇖ω"
then
have "function(f)" "domain(f) = ℵ⇘1⇙⇗M⇖" "range(f)⊆ω" "f∈ℵ⇘1⇙⇗M⇖→ω" "M(f)"
using mem_function_space_rel[OF ‹f∈_›] domain_of_fun fun_is_function range_fun_subset_codomain
function_space_rel_char
by auto
let ?G="λn∈range(f). f-``{n}"
from ‹f:ℵ⇘1⇙⇗M⇖→ω›
have "range(f) ⊆ ω" "domain(?G) = range(f)"
using range_fun_subset_codomain
by simp_all
from ‹f:ℵ⇘1⇙⇗M⇖→ω› ‹M(f)› ‹range(f) ⊆ ω›
have "M(f-``{n})" if "n ∈ range(f)" for n
using that transM[of _ ω] by auto
with ‹M(f)› ‹range(f) ⊆ ω›
have "domain(?G) ≲⇗M⇖ ω" "M(?G)"
using subset_imp_lepoll_rel lam_closed[of "λx . f-``{x}"] cardinal_lib_assms4
by simp_all
have "function(?G)" by (simp add:function_lam)
from ‹f:ℵ⇘1⇙⇗M⇖→ω›
have "n∈ω ⟹ f-``{n} ⊆ ℵ⇘1⇙⇗M⇖" for n
using Pi_vimage_subset by simp
with ‹range(f) ⊆ ω›
have "ℵ⇘1⇙⇗M⇖ = (⋃n∈range(f). f-``{n})"
proof (intro equalityI, intro subsetI)
fix x
assume "x ∈ ℵ⇘1⇙⇗M⇖"
with ‹f:ℵ⇘1⇙⇗M⇖→ω› ‹function(f)› ‹domain(f) = ℵ⇘1⇙⇗M⇖›
have "x ∈ f-``{f`x}" "f`x ∈ range(f)"
using function_apply_Pair vimage_iff apply_rangeI by simp_all
then
show "x ∈ (⋃n∈range(f). f-``{n})" by auto
qed auto
{
assume "∀n∈range(f). |f-``{n}|⇗M⇖ < ℵ⇘1⇙⇗M⇖"
then
have "∀n∈domain(?G). |?G`n|⇗M⇖ < ℵ⇘1⇙⇗M⇖"
using zero_lt_Aleph_rel1 by (auto)
with ‹function(?G)› ‹domain(?G) ≲⇗M⇖ ω› ‹M(?G)›
have "|⋃n∈domain(?G). ?G`n|⇗M⇖≤ω"
using lt_Aleph_rel_imp_cardinal_rel_UN_le_nat[of ?G]
by auto
then
have "|⋃n∈range(f). f-``{n}|⇗M⇖≤ω" by simp
with ‹ℵ⇘1⇙⇗M⇖ = _›
have "|ℵ⇘1⇙⇗M⇖|⇗M⇖ ≤ ω" by auto
then
have "ℵ⇘1⇙⇗M⇖ ≤ ω"
using Card_rel_Aleph_rel Card_rel_cardinal_rel_eq
by auto
then
have "False"
using nat_lt_Aleph_rel1 by (blast dest:lt_trans2)
}
with ‹range(f)⊆ω› ‹M(f)›
obtain n where "n∈ω" "¬(|f -`` {n}|⇗M⇖ < ℵ⇘1⇙⇗M⇖)" "M(f -`` {n})"
using nat_into_M by auto
moreover from this
have "ℵ⇘1⇙⇗M⇖ ≤ |f-``{n}|⇗M⇖"
using not_lt_iff_le Card_rel_is_Ord by simp
moreover
note ‹n∈ω ⟹ f-``{n} ⊆ ℵ⇘1⇙⇗M⇖›
ultimately
show ?thesis
using subset_imp_le_cardinal_rel[THEN le_anti_sym, of _ "ℵ⇘1⇙⇗M⇖"]
Card_rel_Aleph_rel Card_rel_cardinal_rel_eq
by auto
qed
lemma eqpoll_rel_Aleph_rel1_cardinal_rel_vimage :
assumes "Z ≈⇗M⇖ (ℵ⇘1⇙⇗M⇖)" "f ∈ Z →⇗M⇖ ω" "M(Z)"
shows "∃n∈ω. |f-``{n}|⇗M⇖ = ℵ⇘1⇙⇗M⇖"
proof -
have "M(1)" "M(ω)" by simp_all
then
have "M(ℵ⇘1⇙⇗M⇖)" by simp
with assms ‹M(1)›
obtain g where A:"g∈bij_rel(M,ℵ⇘1⇙⇗M⇖,Z)" "M(g)"
using eqpoll_rel_sym unfolding eqpoll_rel_def by blast
with ‹f : Z →⇗M⇖ ω› assms
have "M(f)" "converse(g) ∈ bij_rel(M,Z, ℵ⇘1⇙⇗M⇖)" "f∈Z→ω" "g∈ ℵ⇘1⇙⇗M⇖→Z"
using bij_rel_is_fun_rel bij_rel_converse_bij_rel bij_rel_char function_space_rel_char
by simp_all
with ‹g∈bij_rel(M,ℵ⇘1⇙⇗M⇖,Z)› ‹M(g)›
have "f O g : ℵ⇘1⇙⇗M⇖ →⇗M⇖ ω" "M(converse(g))"
using comp_fun[OF _ ‹f∈ Z→_›,of g] function_space_rel_char
by simp_all
then
obtain n where "n∈ω" "|(f O g)-``{n}|⇗M⇖ = ℵ⇘1⇙⇗M⇖"
using Aleph_rel1_eq_cardinal_rel_vimage
by auto
with ‹M(f)› ‹M(converse(g))›
have "M(converse(g) `` (f -`` {n}))" "f -`` {n} ⊆ Z"
using image_comp converse_comp Pi_iff[THEN iffD1,OF ‹f∈Z→ω›] vimage_subset
unfolding vimage_def
using transM[OF ‹n∈ω›]
by auto
from ‹n∈ω› ‹|(f O g)-``{n}|⇗M⇖ = ℵ⇘1⇙⇗M⇖›
have "ℵ⇘1⇙⇗M⇖ = |converse(g) `` (f -``{n})|⇗M⇖"
using image_comp converse_comp unfolding vimage_def
by auto
also from ‹converse(g) ∈ bij_rel(M,Z, ℵ⇘1⇙⇗M⇖)› ‹f: Z→⇗M⇖ ω› ‹M(Z)› ‹M(f)› ‹M(ℵ⇘1⇙⇗M⇖)›
‹M(converse(g) `` (f -`` {n}))›
have "… = |f -``{n}|⇗M⇖"
using range_of_subset_eqpoll_rel[of "converse(g)" Z _ "f -``{n}",
OF bij_rel_is_inj_rel[OF ‹converse(g)∈_›] ‹f -`` {n} ⊆ Z›]
cardinal_rel_cong vimage_closed[OF singleton_closed[OF transM[OF ‹n∈ω›]],of f]
by auto
finally
show ?thesis using ‹n∈_› by auto
qed
subsection‹Applications of transfinite recursive constructions›
definition
rec_constr :: "[i,i] ⇒ i" where
"rec_constr(f,α) ≡ transrec(α,λa g. f`(g``a))"
text‹The function \<^term>‹rec_constr› allows to perform ∗‹recursive
constructions›: given a choice function on the powerset of some
set, a transfinite sequence is created by successively choosing
some new element.
The next result explains its use.›
lemma rec_constr_unfold : "rec_constr(f,α) = f`({rec_constr(f,β). β∈α})"
using def_transrec[OF rec_constr_def, of f α] image_lam by simp
lemma rec_constr_type :
assumes "f:Pow_rel(M,G)→⇗M⇖ G" "Ord(α)" "M(G)"
shows "M(α) ⟹ rec_constr(f,α) ∈ G"
using assms(2)
proof(induct rule:trans_induct)
case (step β)
with assms
have "{rec_constr(f, x) . x ∈ β} = {y . x ∈ β, y=rec_constr(f, x)}" (is "_ = ?Y")
"M(f)"
using transM[OF _ ‹M(β)›] function_space_rel_char Ord_in_Ord
by auto
moreover from assms this step ‹M(β)› ‹Ord(β)›
have "M({y . x ∈ β, y=<x,rec_constr(f, x)>})" (is "M(?Z)")
using strong_replacement_closed[OF cardinal_lib_assms6(1),of f β β,OF _ _ _ _
univalent_conjI2[where P="λx _ . x∈β",OF univalent_triv]]
transM[OF _ ‹M(β)›] transM[OF step(2) ‹M(G)›] Ord_in_Ord
unfolding rec_constr_def
by auto
moreover from assms this step ‹M(β)› ‹Ord(β)›
have "?Y = {snd(y) . y∈?Z}"
proof(intro equalityI, auto)
fix u
assume "u∈β"
with assms this step ‹M(β)› ‹Ord(β)›
have "<u,rec_constr(f,u)> ∈ ?Z" "rec_constr(f, u) = snd(<u,rec_constr(f,u)>)"
by auto
then
show "∃x∈{y . x ∈ β, y = ⟨x, rec_constr(f, x)⟩}. rec_constr(f, u) = snd(x)"
using bexI[of _ u] by force
qed
moreover from ‹M(?Z)› ‹?Y = _›
have "M(?Y)"
using
RepFun_closed[OF lam_replacement_imp_strong_replacement[OF lam_replacement_snd] ‹M(?Z)›]
fst_snd_closed[THEN conjunct2] transM[OF _ ‹M(?Z)›]
by simp
moreover from assms step
have "{rec_constr(f, x) . x ∈ β} ∈ Pow(G)" (is "?X∈_")
using transM[OF _ ‹M(β)›] function_space_rel_char
by auto
moreover from assms calculation step
have "M(?X)"
by simp
moreover from calculation ‹M(G)›
have "?X∈Pow_rel(M,G)"
using Pow_rel_char by simp
ultimately
have "f`?X ∈ G"
using assms apply_type[OF mem_function_space_rel[of f],of "Pow_rel(M,G)" G ?X]
by auto
then
show ?case
by (subst rec_constr_unfold,simp)
qed
lemma rec_constr_closed :
assumes "f:Pow_rel(M,G)→⇗M⇖ G" "Ord(α)" "M(G)" "M(α)"
shows "M(rec_constr(f,α))"
using transM[OF rec_constr_type ‹M(G)›] assms by auto
lemma lambda_rec_constr_closed :
assumes "Ord(γ)" "M(γ)" "M(f)" "f:Pow_rel(M,G)→⇗M⇖ G" "M(G)"
shows "M(λα∈γ . rec_constr(f,α))"
using lam_closed2[OF cardinal_lib_assms6(1),unfolded rec_constr_def[symmetric],of f γ]
rec_constr_type[OF ‹f∈_› Ord_in_Ord[of γ]] transM[OF _ ‹M(G)›] assms
by simp
text‹The next lemma is an application of recursive constructions.
It works under the assumption that whenever the already constructed
subsequence is small enough, another element can be added.›
lemma bounded_cardinal_rel_selection :
includes Ord_dests
assumes
"⋀Z. |Z|⇗M⇖ < γ ⟹ Z ⊆ G ⟹ M(Z) ⟹ ∃a∈G. ∀s∈Z. <s,a>∈Q" "b∈G" "Card_rel(M,γ)"
"M(G)" "M(Q)" "M(γ)"
shows
"∃S[M]. S : γ →⇗M⇖ G ∧ (∀α ∈ γ. ∀β ∈ γ. α<β ⟶ <S`α,S`β>∈Q)"
proof -
from assms
have "M(x) ⟹ M({a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})" for x
using cdlt_assms by simp
let ?cdltγ="{Z∈Pow_rel(M,G) . |Z|⇗M⇖<γ}"
and ?inQ="λY.{a∈G. ∀s∈Y. <s,a>∈Q}"
from ‹M(G)› ‹Card_rel(M,γ)› ‹M(γ)›
have "M(?cdltγ)" "Ord(γ)"
using cardinal_lib_assms5[OF ‹M(γ)›] Card_rel_is_Ord
by simp_all
from assms
have H:"∃a. a ∈ ?inQ(Y)" if "Y∈?cdltγ" for Y
proof -
{
fix Y
assume "Y∈?cdltγ"
then
have A:"Y∈Pow_rel(M,G)" "|Y|⇗M⇖<γ" by simp_all
then
have "Y⊆G" "M(Y)" using Pow_rel_char[OF ‹M(G)›] by simp_all
with A
obtain a where "a∈G" "∀s∈Y. <s,a>∈Q"
using assms(1) by force
with ‹M(G)›
have "∃a. a ∈ ?inQ(Y)" by auto
}
then show ?thesis using that by simp
qed
then
have "∃f[M]. f ∈ Pi_rel(M,?cdltγ,?inQ) ∧ f ∈ Pi(?cdltγ,?inQ)"
proof -
from ‹⋀x. M(x) ⟹ M({a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})› ‹M(G)›
have "x ∈ {Z ∈ Pow⇗M⇖(G) . |Z|⇗M⇖ < γ} ⟹ M({a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})" for x
by (auto dest:transM)
with‹M(G)› ‹⋀x. M(x) ⟹ M({a ∈ G . ∀s∈x. ⟨s, a⟩ ∈ Q})› ‹M(Q)› ‹M(?cdltγ)›
interpret M_Pi_assumptions_choice M ?cdltγ ?inQ
using cdlt_assms[where Q=Q] lam_replacement_Collect_ball_Pair[THEN
lam_replacement_imp_strong_replacement] surj_imp_inj_replacement3
lam_replacement_hcomp2[OF lam_replacement_constant
lam_replacement_Collect_ball_Pair _ _ lam_replacement_minimum,
unfolded lam_replacement_def]
lam_replacement_hcomp lam_replacement_Sigfun[OF
lam_replacement_Collect_ball_Pair, of G Q, THEN
lam_replacement_imp_strong_replacement]
by unfold_locales (blast dest: transM, auto dest:transM)
show ?thesis using AC_Pi_rel Pi_rel_char H by auto
qed
then
obtain f where f_type:"f ∈ Pi_rel(M,?cdltγ,?inQ)" "f ∈ Pi(?cdltγ,?inQ)" and "M(f)"
by auto
moreover
define Cb where "Cb ≡ λ_∈Pow_rel(M,G)-?cdltγ. b"
moreover from ‹b∈G› ‹M(?cdltγ)› ‹M(G)›
have "Cb ∈ Pow_rel(M,G)-?cdltγ → G" "M(Cb)"
using lam_closed[of "λ_.b" "Pow_rel(M,G)-?cdltγ"]
tag_replacement transM[OF ‹b∈G›]
unfolding Cb_def by auto
moreover
note ‹Card_rel(M,γ)›
ultimately
have "f ∪ Cb : (∏x∈Pow_rel(M,G). ?inQ(x) ∪ G)" using
fun_Pi_disjoint_Un[ of f ?cdltγ ?inQ Cb "Pow_rel(M,G)-?cdltγ" "λ_.G"]
Diff_partition[of "{Z∈Pow_rel(M,G). |Z|⇗M⇖<γ}" "Pow_rel(M,G)", OF Collect_subset]
by auto
moreover
have "?inQ(x) ∪ G = G" for x by auto
moreover from calculation
have "f ∪ Cb : Pow_rel(M,G) → G"
using function_space_rel_char by simp
ultimately
have "f ∪ Cb : Pow_rel(M,G) →⇗M⇖ G"
using function_space_rel_char ‹M(f)› ‹M(Cb)› Pow_rel_closed ‹M(G)›
by auto
define S where "S≡λα∈γ. rec_constr(f ∪ Cb, α)"
from ‹f ∪ Cb: Pow_rel(M,G) →⇗M⇖ G› ‹Card_rel(M,γ)› ‹M(γ)› ‹M(G)›
have "S : γ → G" "M(f ∪ Cb)"
unfolding S_def
using Ord_in_Ord[OF Card_rel_is_Ord] rec_constr_type lam_type transM[OF _ ‹M(γ)›]
function_space_rel_char
by auto
moreover from ‹f∪Cb ∈ _→⇗M⇖ G› ‹Card_rel(M,γ)› ‹M(γ)› ‹M(G)› ‹M(f ∪ Cb)› ‹Ord(γ)›
have "M(S)"
unfolding S_def
using lambda_rec_constr_closed
by simp
moreover
have "∀α∈γ. ∀β∈γ. α < β ⟶ <S ` α, S ` β>∈Q"
proof (intro ballI impI)
fix α β
assume "β∈γ"
with ‹Card_rel(M,γ)› ‹M(S)› ‹M(γ)›
have "β⊆γ" "M(S``β)" "M(β)" "{S`x . x ∈ β} = {restrict(S,β)`x . x ∈ β}"
using transM[OF ‹β∈γ› ‹M(γ)›] image_closed Card_rel_is_Ord OrdmemD
by auto
with ‹β∈_› ‹Card_rel(M,γ)› ‹M(γ)›
have "{rec_constr(f ∪ Cb, x) . x∈β} = {S`x . x ∈ β}"
using Ord_trans[OF _ _ Card_rel_is_Ord, of _ β γ]
unfolding S_def
by auto
moreover from ‹β∈γ› ‹S : γ → G› ‹Card_rel(M,γ)› ‹M(γ)› ‹M(S``β)›
have "{S`x . x ∈ β} ⊆ G" "M({S`x . x ∈ β})"
using Ord_trans[OF _ _ Card_rel_is_Ord, of _ β γ]
apply_type[of S γ "λ_. G"]
by(auto,simp add:image_fun_subset[OF ‹S∈_› ‹β⊆_›])
moreover from ‹Card_rel(M,γ)› ‹β∈γ› ‹S∈_› ‹β⊆γ› ‹M(S)› ‹M(β)› ‹M(G)› ‹M(γ)›
have "|{S`x . x ∈ β}|⇗M⇖ < γ"
using
‹{S`x . x∈β} = {restrict(S,β)`x . x∈β}›[symmetric]
cardinal_rel_RepFun_le[of "restrict(S,β)" β G,
OF restrict_type2[of S γ "λ_.G" β] restrict_closed]
Ord_in_Ord Ord_cardinal_rel
lt_trans1[of "|{S`x . x ∈ β}|⇗M⇖" "|β|⇗M⇖" γ]
Card_rel_lt_iff[THEN iffD2, of β γ, OF _ _ _ _ ltI]
Card_rel_is_Ord
by auto
moreover
have "∀x∈β. <S`x, f ` {S`x . x ∈ β}> ∈ Q"
proof -
from calculation and f_type
have "f ` {S`x . x ∈ β} ∈ {a∈G. ∀x∈β. <S`x,a>∈Q}"
using apply_type[of f ?cdltγ ?inQ "{S`x . x ∈ β}"]
Pow_rel_char[OF ‹M(G)›]
by simp
then
show ?thesis by simp
qed
moreover
assume "α∈γ" "α < β"
moreover from this
have "α∈β" using ltD by simp
moreover
note ‹β∈γ› ‹Cb ∈ Pow_rel(M,G)-?cdltγ → G›
ultimately
show "<S ` α, S ` β>∈Q"
using fun_disjoint_apply1[of "{S`x . x ∈ β}" Cb f]
domain_of_fun[of Cb] ltD[of α β]
by (subst (2) S_def, auto) (subst rec_constr_unfold, auto)
qed
moreover
note ‹M(G)› ‹M(γ)›
ultimately
show ?thesis using function_space_rel_char by auto
qed
text‹The following basic result can, in turn, be proved by a
bounded-cardinal\_rel selection.›
lemma Infinite_iff_lepoll_rel_nat : "M(Z) ⟹ Infinite(Z) ⟷ ω ≲⇗M⇖ Z"
proof
define Distinct where "Distinct = {<x,y> ∈ Z×Z . x≠y}"
have "Distinct = {xy ∈ Z×Z . ∃a b. xy = ⟨a, b⟩ ∧ a ≠ b}" (is "_=?A")
unfolding Distinct_def by auto
moreover
assume "Infinite(Z)" "M(Z)"
moreover from calculation
have "M(Distinct)"
using cardinal_lib_assms6 by simp
from ‹Infinite(Z)› ‹M(Z)›
obtain b where "b∈Z"
using Infinite_not_empty by auto
{
fix Y
assume "|Y|⇗M⇖ < ω" "M(Y)"
then
have "Finite(Y)"
using Finite_cardinal_rel_iff' ltD nat_into_Finite by auto
with ‹Infinite(Z)›
have "Z ≠ Y" by auto
}
moreover
have "(⋀W. M(W) ⟹ |W|⇗M⇖ < ω ⟹ W ⊆ Z ⟹ ∃a∈Z. ∀s∈W. <s,a>∈Distinct)"
proof -
fix W
assume "M(W)" "|W|⇗M⇖ < ω" "W ⊆ Z"
moreover from this
have "Finite_rel(M,W)"
using
cardinal_rel_closed[OF ‹M(W)›] Card_rel_nat
lt_Card_rel_imp_lesspoll_rel[of ω,simplified,OF _ ‹|W|⇗M⇖ < ω›]
lesspoll_rel_nat_is_Finite_rel[of W]
eqpoll_rel_imp_lepoll_rel eqpoll_rel_sym[OF cardinal_rel_eqpoll_rel,of W]
lesspoll_rel_trans1[of W "|W|⇗M⇖" ω] by auto
moreover from calculation
have "¬Z⊆W"
using equalityI ‹Infinite(Z)› by auto
moreover from calculation
show "∃a∈Z. ∀s∈W. <s,a>∈Distinct"
unfolding Distinct_def by auto
qed
moreover from ‹b∈Z› ‹M(Z)› ‹M(Distinct)› this
obtain S where "S : ω →⇗M⇖ Z" "M(S)" "∀α∈ω. ∀β∈ω. α < β ⟶ <S`α,S`β> ∈ Distinct"
using bounded_cardinal_rel_selection[OF _ ‹b∈Z› Card_rel_nat,of Distinct]
by blast
moreover from this
have "α ∈ ω ⟹ β ∈ ω ⟹ α≠β ⟹ S`α ≠ S`β" for α β
unfolding Distinct_def
by (rule_tac lt_neq_symmetry[of "ω" "λα β. S`α ≠ S`β"])
auto
moreover from this ‹S∈_› ‹M(Z)›
have "S∈inj(ω,Z)" using function_space_rel_char unfolding inj_def by auto
ultimately
show "ω ≲⇗M⇖ Z"
unfolding lepoll_rel_def using inj_rel_char ‹M(Z)› by auto
next
assume "ω ≲⇗M⇖ Z" "M(Z)"
then
show "Infinite(Z)" using lepoll_rel_nat_imp_Infinite by simp
qed
lemma Infinite_InfCard_rel_cardinal_rel : "Infinite(Z) ⟹ M(Z) ⟹ InfCard_rel(M,|Z|⇗M⇖)"
using lepoll_rel_eq_trans eqpoll_rel_sym lepoll_rel_nat_imp_Infinite
Infinite_iff_lepoll_rel_nat Inf_Card_rel_is_InfCard_rel cardinal_rel_eqpoll_rel
by simp
lemma (in M_trans) mem_F_bound2 :
fixes F A
defines "F ≡ λ_ x. if M(x) then A-``{x} else 0"
shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ range(A))"
using apply_0 unfolding F_def
by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)
lemma Finite_to_one_rel_surj_rel_imp_cardinal_rel_eq :
assumes "F ∈ Finite_to_one_rel(M,Z,Y) ∩ surj_rel(M,Z,Y)" "Infinite(Z)" "M(Z)" "M(Y)"
shows "|Y|⇗M⇖ = |Z|⇗M⇖"
proof -
have sep_true: "separation(M, M)" unfolding separation_def by auto
note ‹M(Z)› ‹M(Y)›
moreover from this assms
have "M(F)" "F ∈ Z → Y"
unfolding Finite_to_one_rel_def
using function_space_rel_char by simp_all
moreover from this
have "x ∈ (if M(i) then F -`` {i} else 0) ⟹ M(i)" for x i
by (cases "M(i)") auto
moreover from calculation
interpret M_replacement_lepoll M "λ_ x. if M(x) then F-``{x} else 0"
using lam_replacement_inj_rel mem_F_bound2 cardinal_lib_assms3
lam_replacement_vimage_sing_fun
lam_replacement_if[OF _
lam_replacement_constant[OF nonempty],where b=M] sep_true
by (unfold_locales, simp_all)
(rule lam_Least_assumption_general[where U="λ_. range(F)"], auto)
have "w ∈ (if M(y) then F-``{y} else 0) ⟹ M(y)" for w y
by (cases "M(y)") auto
moreover from ‹F∈_∩_›
have 0:"Finite(F-``{y})" if "y∈Y" for y
unfolding Finite_to_one_rel_def
using vimage_fun_sing ‹F∈Z→Y› transM[OF that ‹M(Y)›] transM[OF _ ‹M(Z)›] that by simp
ultimately
interpret M_cardinal_UN_lepoll _ "λy. if M(y) then F-``{y} else 0" Y
using cardinal_lib_assms3 lepoll_assumptions
by unfold_locales (auto dest:transM simp del:mem_inj_abs)
from ‹F∈Z→Y›
have "Z = (⋃y∈Y. {x∈Z . F`x = y})"
using apply_type by auto
then
show ?thesis
proof (cases "Finite(Y)")
case True
with ‹Z = (⋃y∈Y. {x∈Z . F`x = y})› and assms and ‹F∈Z→Y›
show ?thesis
using Finite_RepFun[THEN [2] Finite_Union, of Y "λy. F-``{y}"] 0 vimage_fun_sing[OF ‹F∈Z→Y›]
by simp
next
case False
moreover from this ‹M(Y)›
have "Y ≲⇗M⇖ |Y|⇗M⇖"
using cardinal_rel_eqpoll_rel eqpoll_rel_sym eqpoll_rel_imp_lepoll_rel by auto
moreover
note assms
moreover from ‹F∈_∩_›
have "Finite({x∈Z . F`x = y})" "M(F-``{y})" if "y∈Y" for y
unfolding Finite_to_one_rel_def
using transM[OF that ‹M(Y)›] transM[OF _ ‹M(Z)›] vimage_fun_sing[OF ‹F∈Z→Y›] that
by simp_all
moreover from calculation
have "|{x∈Z . F`x = y}|⇗M⇖ ∈ ω" if "y∈Y" for y
using Finite_cardinal_rel_in_nat that transM[OF that ‹M(Y)›] vimage_fun_sing[OF ‹F∈Z→Y›] that
by simp
moreover from calculation
have "|{x∈Z . F`x = y}|⇗M⇖ ≤ |Y|⇗M⇖" if "y∈Y" for y
using Infinite_imp_nats_lepoll_rel[THEN lepoll_rel_imp_cardinal_rel_le,
of _ "|{x∈Z . F`x = y}|⇗M⇖"]
that cardinal_rel_idem transM[OF that ‹M(Y)›] vimage_fun_sing[OF ‹F∈Z→Y›]
by auto
ultimately
have "|⋃y∈Y. {x∈Z . F`x = y}|⇗M⇖ ≤ |Y|⇗M⇖"
using leqpoll_rel_imp_cardinal_rel_UN_le
Infinite_InfCard_rel_cardinal_rel[of Y] vimage_fun_sing[OF ‹F∈Z→Y›]
by(auto simp add:transM[OF _ ‹M(Y)›])
moreover from ‹F ∈ Finite_to_one_rel(M,Z,Y) ∩ surj_rel(M,Z,Y)› ‹M(Z)› ‹M(F)› ‹M(Y)›
have "|Y|⇗M⇖ ≤ |Z|⇗M⇖"
using surj_rel_implies_cardinal_rel_le by auto
moreover
note ‹Z = (⋃y∈Y. {x∈Z . F`x = y})›
ultimately
show ?thesis
using le_anti_sym by auto
qed
qed
lemma cardinal_rel_map_Un :
assumes "Infinite(X)" "Finite(b)" "M(X)" "M(b)"
shows "|{a ∪ b . a ∈ X}|⇗M⇖ = |X|⇗M⇖"
proof -
have "(λa∈X. a ∪ b) ∈ Finite_to_one_rel(M,X,{a ∪ b . a ∈ X})"
"(λa∈X. a ∪ b) ∈ surj_rel(M,X,{a ∪ b . a ∈ X})"
"M({a ∪ b . a ∈ X})"
unfolding def_surj_rel
proof
fix d
have "Finite({a ∈ X . a ∪ b = d})" (is "Finite(?Y(b,d))")
using ‹Finite(b)›
proof (induct arbitrary:d)
case 0
have "{a ∈ X . a ∪ 0 = d} = (if d∈X then {d} else 0)"
by auto
then
show ?case by simp
next
case (cons c b)
from ‹c ∉ b›
have "?Y(cons(c,b),d) ⊆ (if c∈d then ?Y(b,d) ∪ ?Y(b,d-{c}) else 0)"
by auto
with cons
show ?case
using subset_Finite
by simp
qed
moreover
assume "d ∈ {x ∪ b . x ∈ X}"
ultimately
show "Finite({a ∈ X . M(a) ∧ (λx∈X. x ∪ b) ` a = d})"
using subset_Finite[of "{a ∈ X . M(a) ∧ (λx∈X. x ∪ b) ` a = d}"
"{a ∈ X . (λx∈X. x ∪ b) ` a = d}"] by auto
next
note ‹M(X)› ‹M(b)›
moreover
show "M(λa∈X. a ∪ b)"
using lam_closed[of "λ x . x∪b",OF _ ‹M(X)›] Un_closed[OF transM[OF _ ‹M(X)›] ‹M(b)›]
tag_union_replacement[OF ‹M(b)›]
by simp
moreover from this
have "{a ∪ b . a ∈ X} = (λx∈X. x ∪ b) `` X"
using image_lam by simp
with calculation
show "M({a ∪ b . a ∈ X})" by auto
moreover from calculation
show "(λa∈X. a ∪ b) ∈ X →⇗M⇖ {a ∪ b . a ∈ X}"
using function_space_rel_char by (auto intro:lam_funtype)
ultimately
show "(λa∈X. a ∪ b) ∈ surj⇗M⇖(X,{a ∪ b . a ∈ X})" "M({a ∪ b . a ∈ X})"
using surj_rel_char function_space_rel_char
unfolding surj_def by auto
next
qed (simp add:‹M(X)›)
moreover from assms this
show ?thesis
using Finite_to_one_rel_surj_rel_imp_cardinal_rel_eq by simp
qed
end
end