# Theory Cardinal_Library_Relative

section‹Cardinal Arithmetic under Choice\label{sec:cardinal-lib-rel}›

theory Cardinal_Library_Relative
imports
Replacement_Lepoll
begin

locale M_library = M_ZF_library + M_cardinal_AC +
assumes
separation_cardinal_rel_lesspoll_rel: "M(κ) ⟹ separation(M, λx . x ≺⇗M⇖ κ)"
begin

declare eqpoll_rel_refl [simp]

subsection‹Miscellaneous›

lemma cardinal_rel_RepFun_apply_le:
assumes "S ∈ A→B" "M(S)" "M(A)" "M(B)"
shows "|{Sa . a∈A}|⇗M⇖ ≤ |A|⇗M⇖"
proof -
note assms
moreover from this
have "{S  a . a ∈ A} = SA"
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. Sx"] apply_type[OF ‹S∈_›] transM[OF _ ‹M(B)›]
by auto
moreover from assms this
have "(λx∈A. Sx) ∈ surj_rel(M,A, {Sa . a∈A})"
using mem_surj_abs lam_funtype[of A "λx . Sx"]
unfolding surj_def by auto
ultimately
show ?thesis
using surj_rel_char surj_rel_implies_cardinal_rel_le by simp
qed

(* TODO: Check if we can use this lemma to prove the previous one and
not the other way around *)
lemma cardinal_rel_RepFun_le:
assumes lrf:"lam_replacement(M,f)" and f_closed:"∀x[M]. M(f(x))" and "M(X)"
shows "|{f(x) . x ∈ X}|⇗M⇖ ≤ |X|⇗M⇖"
using ‹M(X)› f_closed cardinal_rel_RepFun_apply_le[OF lam_funtype, of X _, OF
lrf[THEN [2] lam_replacement_iff_lam_closed[THEN iffD1, THEN rspec]]]
lrf[THEN lam_replacement_imp_strong_replacement]
by simp (auto simp flip:setclass_iff intro!:RepFun_closed dest:transM)

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"

end ― ‹\<^locale>‹M_library››

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
qed

end ― ‹\<^locale>‹M_cardinal_UN_nat››

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 ⟹ fi ∈ K" for i
using inj_rel_is_fun[OF f_inj] apply_type
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 ⟹ fi ∈ K›
have "x ∈ Y(fi)" "fi ∈ 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
moreover
note assms ‹⋀i. i∈J ⟹ fi ∈ 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_inj››

locale M_cardinal_UN_lepoll = M_library + M_replacement_lepoll _ "λ_. X" +
j:M_cardinal_UN _ J for J
begin

lemma lepoll_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 ― ‹\<^locale>‹M_cardinal_UN_lepoll››

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
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 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 ― ‹\<^locale>‹M_library››

subsection‹Countable and uncountable sets›

relativize functional "countable" "countable_rel" external
relationalize "countable_rel" "is_countable"

notation countable_rel (‹countable⇗_⇖'(_')›)

abbreviation
countable_r_set  :: "[i,i]⇒o"  (‹countable⇗_⇖'(_')›) where
"countable⇗M⇖(i) ≡ countable_rel(##M,i)"

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

― ‹Next lemma can be proved without using AC›
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 ― ‹\<^locale>‹M_library››

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 lepoll_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)⟩)"
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 Ga 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
cardinal_rel_separation :
"separation(M, λ⟨x,y⟩. cardinal_rel(M,x) = y)"
and
separation_cardinal_rel_lt :
"M(γ) ⟹ separation(M, λZ . cardinal_rel(M,Z) < γ)"

begin

lemma cdlt_assms: "M(x) ⟹ M(Q) ⟹ separation(M, λa .  ∀s∈x. ⟨s, a⟩ ∈ Q)"
using separation_in[OF _ lam_replacement_product] separation_ball
lam_replacement_fst lam_replacement_snd lam_replacement_constant
by simp_all

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
lam_replacement_minimum
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 separation_Ord lam_replacement_minimum
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 lam_replacement_minimum
by unfold_locales auto
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 ― ‹\<^locale>‹M_cardinal_library››

abbreviation
uncountable_rel :: "[i⇒o,i]⇒o" where
"uncountable_rel(M,X) ≡ ¬ countable_rel(M,X)"

context M_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_succ:
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

― ‹Could be proved without using AC›
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 Gx 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)

end ― ‹\<^locale>‹M_library››

context M_cardinal_library
begin

lemma lt_Aleph_rel_imp_cardinal_rel_UN_le_nat: "function(G) ⟹ domain(G) ≲⇗M⇖ ω ⟹
∀n∈domain(G). |Gn|⇗M⇖<ℵ⇘1⇙⇗M⇖ ⟹ M(G) ⟹ |⋃n∈domain(G). Gn|⇗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 Gx else 0"
using lam_replacement_inj_rel cardinal_lib_assms2 mem_F_bound1[of _ _ G]
lam_if_then_replacement_apply lam_replacement_minimum
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 Gn 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). Gn"
assume "?N ≲⇗M⇖ ω"
assume Eq1: "∀n∈?N. |Gn|⇗M⇖<ℵ⇘1⇙⇗M⇖"
{
fix n
assume "n∈?N"
with Eq1 ‹M(G)›
have "|Gn|⇗M⇖ ≤ ω"
using le_Aleph_rel1_nat[of "|G  n|⇗M⇖"] lepoll_rel_imp_cardinal_rel_UN_le
UN_if_zero[of "domain(G)" G]
by (auto dest:transM)
}
then
have "n∈?N ⟹ |Gn|⇗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 lepoll_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
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-{fx}" "fx ∈ 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). |?Gn|⇗M⇖ < ℵ⇘1⇙⇗M⇖"
using zero_lt_Aleph_rel1 by (auto)
with ‹function(?G)› ‹domain(?G) ≲⇗M⇖ ω› ‹M(?G)›
have "|⋃n∈domain(?G). ?Gn|⇗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

― ‹There is some asymmetry between assumptions and conclusion
(\<^term>‹eqpoll_rel› versus \<^term>‹cardinal_rel›)›

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

end ― ‹\<^locale>‹M_cardinal_library››

subsection‹Applications of transfinite recursive constructions›

locale M_cardinal_library_extra = M_cardinal_library +
assumes
replacement_trans_apply_image:
"M(f) ⟹ M(β) ⟹ Ord(β) ⟹
strong_replacement(M, λx y. x∈β ∧ y = ⟨x, transrec(x, λa g. f  (g  a))⟩)"
begin

lemma rec_constr_type_rel:
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 replacement_trans_apply_image,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_rel ‹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 replacement_trans_apply_image,unfolded rec_constr_def[symmetric],of f γ]
rec_constr_type_rel[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 separation_orthogonal by simp
let ?cdltγ="{Z∈Pow_rel(M,G) . |Z|⇗M⇖<γ}" ― ‹cardinal\_rel less than \<^term>‹γ›''›
and ?inQ="λY.{a∈G. ∀s∈Y. <s,a>∈Q}"
from ‹M(G)› ‹Card_rel(M,γ)› ‹M(γ)›
have "M(?cdltγ)" "Ord(γ)"
using separation_cardinal_rel_lt[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] surj_imp_inj_replacement3
lam_replacement_Collect_ball_Pair[THEN lam_replacement_imp_strong_replacement]
lam_replacement_minimum[THEN [5] lam_replacement_hcomp2,OF
lam_replacement_constant lam_replacement_Collect_ball_Pair,unfolded lam_replacement_def]
lam_replacement_Sigfun[OF lam_replacement_Collect_ball_Pair,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_rel 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(β)" "{Sx . 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∈β} = {Sx . 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 "{Sx . x ∈ β} ⊆ G" "M({Sx . x ∈ β})"
using Ord_trans[OF _ _ Card_rel_is_Ord, of _ β γ]
apply_type[of S γ "λ_. G"]
moreover from ‹Card_rel(M,γ)› ‹β∈γ› ‹S∈_› ‹β⊆γ› ‹M(S)› ‹M(β)› ‹M(G)› ‹M(γ)›
have "|{Sx . x ∈ β}|⇗M⇖ < γ"
using
‹{Sx . x∈β} = {restrict(S,β)x . x∈β}›[symmetric]
cardinal_rel_RepFun_apply_le[of "restrict(S,β)" β G,
OF restrict_type2[of S γ "λ_.G" β] restrict_closed]
Ord_in_Ord Ord_cardinal_rel
lt_trans1[of "|{Sx . x ∈ β}|⇗M⇖" "|β|⇗M⇖" γ]
Card_rel_lt_iff[THEN iffD2, of β γ, OF _ _ _ _ ltI]
Card_rel_is_Ord
by auto
moreover
have "∀x∈β. <Sx, f  {Sx . x ∈ β}> ∈ Q"
proof -
from calculation and f_type
have "f  {Sx . x ∈ β} ∈ {a∈G. ∀x∈β. <Sx,a>∈Q}"
using apply_type[of f ?cdltγ ?inQ "{Sx . 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 "{Sx . 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 separation_dist 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_minimum
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 . Fx = y})"
using apply_type by auto
then
show ?thesis
proof (cases "Finite(Y)")
case True
with ‹Z = (⋃y∈Y. {x∈Z . Fx = 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 . Fx = 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 . Fx = 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 . Fx = 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 . Fx = 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 . Fx = y}|⇗M⇖ ≤ |Y|⇗M⇖"
using lepoll_rel_imp_cardinal_rel_UN_le
Infinite_InfCard_rel_cardinal_rel[of Y] vimage_fun_sing[OF ‹F∈Z→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 . Fx = 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
moreover from assms this
show ?thesis
using Finite_to_one_rel_surj_rel_imp_cardinal_rel_eq by simp
qed

end ― ‹\<^locale>‹M_cardinal_library_extra››

context M_library
begin

subsection‹Results on relative cardinal exponentiation›

lemma cexp_rel_eqpoll_rel_cong:
assumes
"A ≈⇗M⇖ A'" "B ≈⇗M⇖ B'" "M(A)" "M(A')" "M(B)" "M(B')"
shows
"A⇗↑B,M⇖ = A'⇗↑B',M⇖"
unfolding cexp_rel_def using cardinal_rel_eqpoll_rel_iff
function_space_rel_eqpoll_rel_cong assms
by simp

lemma cexp_rel_cexp_rel_cmult:
assumes "M(κ)" "M(ν1)" "M(ν2)"
shows "(κ⇗↑ν1,M⇖)⇗↑ν2,M⇖ = κ⇗↑ν2 ⊗⇗M⇖ ν1,M⇖"
proof -
have "(κ⇗↑ν1,M⇖)⇗↑ν2,M⇖ = (ν1 →⇗M⇖ κ)⇗↑ν2,M⇖"
using cardinal_rel_eqpoll_rel
by (intro cexp_rel_eqpoll_rel_cong) (simp_all add:assms cexp_rel_def)
also from assms
have " … = κ⇗↑ν2 × ν1,M⇖"
unfolding cexp_rel_def using curry_eqpoll_rel[THEN cardinal_rel_cong] by blast
also
have " … = κ⇗↑ν2 ⊗⇗M⇖ ν1,M⇖"
using cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym]
unfolding cmult_rel_def by (intro cexp_rel_eqpoll_rel_cong) (auto simp add:assms)
finally
show ?thesis .
qed

lemma cardinal_rel_Pow_rel: "M(X) ⟹ |Pow_rel(M,X)|⇗M⇖ = 2⇗↑X,M⇖" ― ‹Perhaps it's better with |X|›
using cardinal_rel_eqpoll_rel_iff[THEN iffD2,
OF _ _ Pow_rel_eqpoll_rel_function_space_rel]
unfolding cexp_rel_def by simp

lemma cantor_cexp_rel:
assumes "Card_rel(M,ν)" "M(ν)"
shows "ν < 2⇗↑ν,M⇖"
using assms Card_rel_is_Ord Card_rel_cexp_rel
proof (intro not_le_iff_lt[THEN iffD1] notI)
assume "2⇗↑ν,M⇖ ≤ ν"
with assms
have "|Pow_rel(M,ν)|⇗M⇖ ≤ ν"
using cardinal_rel_Pow_rel[of ν] by simp
with assms
have "Pow_rel(M,ν) ≲⇗M⇖ ν"
using cardinal_rel_eqpoll_rel_iff Card_rel_le_imp_lepoll_rel Card_rel_cardinal_rel_eq
by auto
then
obtain g where "g ∈ inj_rel(M,Pow_rel(M,ν), ν)"
by blast
moreover
note ‹M(ν)›
moreover from calculation
have "M(g)" by (auto dest:transM)
ultimately
show "False"
using cantor_inj_rel by simp
qed simp

lemma countable_iff_lesspoll_rel_Aleph_rel_one:
notes iff_trans[trans]
assumes "M(C)"
shows "countable⇗M⇖(C) ⟷ C ≺⇗M⇖ ℵ⇘1⇙⇗M⇖"
using assms lesspoll_rel_csucc_rel[of ω C] Aleph_rel_succ Aleph_rel_zero
unfolding countable_rel_def by simp

lemma countable_iff_le_rel_Aleph_rel_one:
notes iff_trans[trans]
assumes "M(C)"
shows "countable⇗M⇖(C) ⟷ |C|⇗M⇖ ≺⇗M⇖ ℵ⇘1⇙⇗M⇖"
proof -
from assms
have "countable⇗M⇖(C) ⟷ C ≺⇗M⇖ ℵ⇘1⇙⇗M⇖"
using countable_iff_lesspoll_rel_Aleph_rel_one
by simp
also from assms
have "… ⟷ |C|⇗M⇖ ≺⇗M⇖ ℵ⇘1⇙⇗M⇖"
using cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym, THEN eq_lesspoll_rel_trans]
by (auto intro:cardinal_rel_eqpoll_rel[THEN eq_lesspoll_rel_trans])
finally
show ?thesis .
qed

end ― ‹\<^locale>‹M_library››

(* TODO: This can be generalized. *)
lemma (in M_cardinal_library) countable_fun_imp_countable_image:
assumes "f:C →⇗M⇖ B" "countable⇗M⇖(C)" "⋀c. c∈C ⟹ countable⇗M⇖(fc)"
"M(C)" "M(B)"
shows "countable⇗M⇖(⋃(fC))"
using assms function_space_rel_char image_fun[of f]
cardinal_rel_RepFun_apply_le[of f C B]
countable_rel_iff_cardinal_rel_le_nat[THEN iffD1, THEN [2] le_trans, of _ ]
countable_rel_iff_cardinal_rel_le_nat
by (rule_tac countable_rel_union_countable_rel)
(auto dest:transM del:imageE)

end