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 "|{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)›]
    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

(* 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"
  by (simp add: Card_rel_lt_csucc_rel_iff)

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
    by (simp add: cardinal_rel_UN_le InfCard_rel_nat)
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 ⟹ 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_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
    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 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 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
    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
  proof(unfold_locales,auto simp add: separation_def)
    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 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)

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). |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 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 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⇖"] lepoll_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 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
  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

― ‹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(β)" "{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_apply_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 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 . 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 lepoll_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 ― ‹\<^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⇖(f`c)"
    "M(C)" "M(B)"
  shows "countable⇗M⇖(⋃(f``C))"
  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