Theory ZF_Library_Relative

section‹Library of basic $\mathit{ZF}$ results\label{sec:zf-lib}›

theory ZF_Library_Relative
  imports
    "Delta_System_Lemma.ZF_Library"
    "ZF-Constructible.Normal"
    Aleph_Relative― ‹must be before Cardinal\_AC\_Relative!›
    Lambda_Replacement
    Cardinal_AC_Relative
    FiniteFun_Relative
begin

lemma (in M_cardinal_arith_jump) csucc_rel_cardinal_rel :
  assumes "Ord(κ)" "M(κ)"
  shows "(|κ|⇗M⇖⇧+)⇗M⇖ = (κ⇧+)⇗M⇖"
proof (intro le_anti_sym)― ‹show both inequalities›
  from assms
  have hips:"M((κ⇧+)⇗M⇖)" "Ord((κ⇧+)⇗M⇖)" "κ < (κ⇧+)⇗M⇖"
    using Card_rel_csucc_rel[THEN Card_rel_is_Ord]
      csucc_rel_basic by simp_all
  then
  show "(|κ|⇗M⇖⇧+)⇗M⇖ ≤ (κ⇧+)⇗M⇖"
    using Ord_cardinal_rel_le[THEN lt_trans1]
      Card_rel_csucc_rel
    unfolding csucc_rel_def
    by (rule_tac Least_antitone) (assumption, simp_all add:assms)
  from assms
  have "κ < L" if "Card⇗M⇖(L)" "|κ|⇗M⇖ < L" "M(L)" for L
    using (* Card_rel_le_iff[THEN iffD1, THEN le_trans, of κ _ L] *) that
      Card_rel_is_Ord leI Card_rel_le_iff[of κ L]
    by (rule_tac ccontr, auto dest:not_lt_imp_le) (fast dest: le_imp_not_lt)
  with hips
  show "(κ⇧+)⇗M⇖ ≤ (|κ|⇗M⇖⇧+)⇗M⇖"
    using Ord_cardinal_rel_le[THEN lt_trans1] Card_rel_csucc_rel
    unfolding csucc_rel_def
    by (rule_tac Least_antitone) (assumption, auto simp add:assms)
qed

lemma (in M_cardinal_arith_jump) csucc_rel_le_mono :
  assumes "κ ≤ ν" "M(κ)" "M(ν)"
  shows "(κ⇧+)⇗M⇖ ≤ (ν⇧+)⇗M⇖"
proof (cases "κ = ν")
  case True
  with assms
  show ?thesis using Card_rel_csucc_rel [THEN Card_rel_is_Ord] by simp
next
  case False
  with assms
  have "κ < ν" using le_neq_imp_lt by simp
  show ?thesis― ‹by way of contradiction›
  proof (rule ccontr)
    assume "¬ (κ⇧+)⇗M⇖ ≤ (ν⇧+)⇗M⇖"
    with assms
    have "(ν⇧+)⇗M⇖ < (κ⇧+)⇗M⇖"
      using Card_rel_csucc_rel[THEN Card_rel_is_Ord] le_Ord2 lt_Ord
      by (intro not_le_iff_lt[THEN iffD1]) auto
    with assms
    have "(ν⇧+)⇗M⇖ ≤ |κ|⇗M⇖"
      using le_Ord2[THEN Card_rel_csucc_rel, of κ ν]
        Card_rel_lt_csucc_rel_iff[of "(ν⇧+)⇗M⇖" "|κ|⇗M⇖", THEN iffD1]
        csucc_rel_cardinal_rel[OF lt_Ord] leI[of "(ν⇧+)⇗M⇖" "(κ⇧+)⇗M⇖"]
      by simp
    with assms
    have "(ν⇧+)⇗M⇖ ≤ κ"
      using Ord_cardinal_rel_le[OF lt_Ord] le_trans by auto
    with assms
    have "ν < κ"
      using csucc_rel_basic le_Ord2[THEN Card_rel_csucc_rel, of κ ν] Card_rel_is_Ord
        le_Ord2
      by (rule_tac j="(ν⇧+)⇗M⇖" in lt_trans2) simp_all
    with ‹κ < ν›
    show "False" using le_imp_not_lt leI by blast
  qed
qed

lemma (in M_cardinal_AC) cardinal_rel_succ_not_0 :   "|A|⇗M⇖ = succ(n) ⟹ M(A) ⟹ M(n) ⟹ A ≠ 0"
  by auto

(* "Finite_to_one(X,Y) ≡ {f:X→Y. ∀y∈Y. Finite({x∈X . f`x = y})}" *)
reldb_add functional "Finite" "Finite" ― ‹wrongly done? Finite is absolute›
relativize functional "Finite_to_one" "Finite_to_one_rel" external
(* reldb_add relational "Finite" "is_Finite" ― ‹don't have is_Finite yet›
relationalize "Finite_to_one_rel" "is_Finite_to_one" *)

notation Finite_to_one_rel (‹Finite'_to'_one⇗_⇖'(_,_')›)

abbreviation
  Finite_to_one_r_set :: "[i,i,i] ⇒ i" (‹Finite'_to'_one⇗_⇖'(_,_')›) where
  "Finite_to_one⇗M⇖(X,Y) ≡ Finite_to_one_rel(##M,X,Y)"

locale M_ZF_library=  M_cardinal_arith + M_aleph + M_FiniteFun + M_replacement_extra
begin

lemma Finite_Collect_imp : "Finite({x∈X . Q(x)}) ⟹ Finite({x∈X . M(x) ∧ Q(x)})"
  (is "Finite(?A) ⟹ Finite(?B)")
  using subset_Finite[of ?B ?A] by auto 

lemma Finite_to_one_relI [intro]:
  assumes "f:X→⇗M⇖Y" "⋀y. y∈Y ⟹ Finite({x∈X . f`x = y})"
    and types:"M(f)" "M(X)" "M(Y)"
  shows "f ∈ Finite_to_one⇗M⇖(X,Y)"
  using assms Finite_Collect_imp unfolding Finite_to_one_rel_def
  by (simp)

lemma Finite_to_one_relI' [intro]:
  assumes "f:X→⇗M⇖Y" "⋀y. y∈Y ⟹ Finite({x∈X . M(x) ∧ f`x = y})"
    and types:"M(f)" "M(X)" "M(Y)"
  shows "f ∈ Finite_to_one⇗M⇖(X,Y)"
  using assms unfolding Finite_to_one_rel_def
  by (simp)

lemma Finite_to_one_relD [dest]:
  "f ∈ Finite_to_one⇗M⇖(X,Y) ⟹f:X→⇗M⇖Y"
  "f ∈ Finite_to_one⇗M⇖(X,Y) ⟹ y∈Y ⟹ M(Y) ⟹ Finite({x∈X . M(x) ∧ f`x = y})"
  unfolding Finite_to_one_rel_def by simp_all

lemma Diff_bij_rel :
  assumes "∀A∈F. X ⊆ A" 
    and types: "M(F)" "M(X)" shows "(λA∈F. A-X) ∈ bij⇗M⇖(F, {A-X. A∈F})"
  using assms  def_inj_rel def_surj_rel unfolding bij_rel_def
  apply (auto)
   apply (subgoal_tac "M(λA∈F. A - X)" "M({A - X . A ∈ F})")
     apply (auto simp add:mem_function_space_rel_abs)
      apply (rule_tac lam_type, auto)
     prefer 4
     apply (subgoal_tac "M(λA∈F. A - X)" "M({A - X . A ∈ F})")
       apply(tactic ‹distinct_subgoals_tac›)
     apply (auto simp add:mem_function_space_rel_abs)
     apply (rule_tac lam_type, auto) prefer 3
    apply (subst subset_Diff_Un[of X])
     apply auto
proof -
  from types 
  show "M({A - X . A ∈ F})"
    using diff_replacement
    by (rule_tac RepFun_closed) (auto dest:transM[of _ F])
  from types
  show "M(λA∈F. A - X)"
    using Pair_diff_replacement
    by (rule_tac lam_closed, auto dest:transM)
qed

lemma function_space_rel_nonempty :
  assumes "b∈B"  and types: "M(B)" "M(A)"
  shows "(λx∈A. b) : A →⇗M⇖ B"
proof -
  note assms
  moreover from this
  have "M(λx∈A. b)" 
    using tag_replacement by (rule_tac lam_closed, auto dest:transM)
  ultimately
  show ?thesis
    by (simp add:mem_function_space_rel_abs)
qed

lemma mem_function_space_rel :
  assumes "f ∈ A →⇗M⇖ y" "M(A)" "M(y)"
  shows  "f ∈ A → y"
  using assms function_space_rel_char by simp

lemmas range_fun_rel_subset_codomain= range_fun_subset_codomain[OF mem_function_space_rel]

end (* M_ZF_library *)

context M_Pi_assumptions
begin

lemma mem_Pi_rel : "f ∈ Pi⇗M⇖(A,B) ⟹ f ∈ Pi(A, B)"
  using trans_closed mem_Pi_rel_abs
  by force

lemmas Pi_rel_rangeD= Pi_rangeD[OF mem_Pi_rel]

lemmas rel_apply_Pair= apply_Pair[OF mem_Pi_rel]

lemmas rel_apply_rangeI= apply_rangeI[OF mem_Pi_rel]

lemmas Pi_rel_range_eq= Pi_range_eq[OF mem_Pi_rel]

lemmas Pi_rel_vimage_subset= Pi_vimage_subset[OF mem_Pi_rel]

end (* M_Pi_assumptions *)

context M_ZF_library
begin

lemma mem_bij_rel : "⟦f ∈ bij⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f∈bij(A,B)"
  using bij_rel_char by simp

lemma mem_inj_rel : "⟦f ∈ inj⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f∈inj(A,B)"
  using inj_rel_char by simp

lemma mem_surj_rel : "⟦f ∈ surj⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f∈surj(A,B)"
  using surj_rel_char by simp

lemmas rel_apply_in_range= apply_in_range[OF _ _ mem_function_space_rel]

lemmas rel_range_eq_image= ZF_Library.range_eq_image[OF mem_function_space_rel]

lemmas rel_Image_sub_codomain= Image_sub_codomain[OF mem_function_space_rel]

lemma rel_inj_to_Image : "⟦f:A→⇗M⇖B; f ∈ inj⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f ∈ inj⇗M⇖(A,f``A)"
  using inj_to_Image[OF mem_function_space_rel mem_inj_rel]
    transM[OF _ function_space_rel_closed] by simp

lemma inj_rel_imp_surj_rel :
  fixes f b
  defines [simp]: "ifx(x) ≡ if x∈range(f) then converse(f)`x else b"
  assumes "f ∈ inj⇗M⇖(B,A)" "b∈B" and types: "M(f)" "M(B)" "M(A)"
  shows "(λx∈A. ifx(x)) ∈ surj⇗M⇖(A,B)"
proof -
  from types and ‹b∈B›
  have "M(λx∈A. ifx(x))"
    using ifx_replacement by (rule_tac lam_closed) (auto dest:transM)
  with assms(2-)
  show ?thesis
    using inj_imp_surj mem_surj_abs by simp
qed

lemma function_space_rel_disjoint_Un :
  assumes "f ∈ A→⇗M⇖B" "g ∈ C→⇗M⇖D"  "A ∩ C = 0"
    and types:"M(A)" "M(B)" "M(C)" "M(D)"
  shows "f ∪ g ∈ (A ∪ C)→⇗M⇖ (B ∪ D)"
  using assms fun_Pi_disjoint_Un[OF mem_function_space_rel
      mem_function_space_rel, OF assms(1) _ _ assms(2)]
    function_space_rel_char by auto

lemma restrict_eq_imp_Un_into_function_space_rel :
  assumes "f ∈ A→⇗M⇖B" "g ∈ C→⇗M⇖D"  "restrict(f, A ∩ C) = restrict(g, A ∩ C)"
    and types:"M(A)" "M(B)" "M(C)" "M(D)"
  shows "f ∪ g ∈ (A ∪ C)→⇗M⇖ (B ∪ D)"
  using assms restrict_eq_imp_Un_into_Pi[OF mem_function_space_rel
      mem_function_space_rel, OF assms(1) _ _ assms(2)]
    function_space_rel_char by auto

lemma lepoll_relD [dest]: "A ≲⇗M⇖ B ⟹ ∃f[M]. f ∈ inj⇗M⇖(A, B)"
  unfolding lepoll_rel_def .

― ‹Should the assumptions be on \<^term>‹f› or on \<^term>‹A› and \<^term>‹B›?
    Should BOTH be intro rules?›
lemma lepoll_relI [intro]: "f ∈ inj⇗M⇖(A, B) ⟹ M(f) ⟹ A ≲⇗M⇖ B"
  unfolding lepoll_rel_def by blast

lemma eqpollD [dest]: "A ≈⇗M⇖ B ⟹ ∃f[M]. f ∈ bij⇗M⇖(A, B)"
  unfolding eqpoll_rel_def .

― ‹Same as @{thm lepoll_relI}›
lemma bij_rel_imp_eqpoll_rel [intro]: "f ∈ bij⇗M⇖(A,B) ⟹ M(f) ⟹ A ≈⇗M⇖ B"
  unfolding eqpoll_rel_def by blast

lemma restrict_bij_rel :― ‹Unused›
  assumes "f ∈ inj⇗M⇖(A,B)"  "C⊆A"
    and types:"M(A)" "M(B)" "M(C)"
  shows "restrict(f,C)∈ bij⇗M⇖(C, f``C)"
  using assms restrict_bij inj_rel_char bij_rel_char by auto

lemma range_of_subset_eqpoll_rel :
  assumes "f ∈ inj⇗M⇖(X,Y)" "S ⊆ X"
    and types:"M(X)" "M(Y)" "M(S)"
  shows "S ≈⇗M⇖ f `` S"
  using assms restrict_bij bij_rel_char
    trans_inj_rel_closed[OF ‹f ∈ inj⇗M⇖(X,Y)›]
  unfolding eqpoll_rel_def
  by (rule_tac x="restrict(f,S)" in rexI) auto

end (* M_ZF_library *)

(*************   Discipline for cexp   ****************)
relativize functional "cexp" "cexp_rel" external
relationalize "cexp_rel" "is_cexp"

context M_ZF_library
begin

― ‹MOVE THIS to an appropriate place›
is_iff_rel for "function_space"
proof -
  assume "M(A)" "M(B)" "M(res)"
  then
  show ?thesis
  using function_space_rel_char mem_function_space_rel_abs
  unfolding is_funspace_def is_function_space_def
  by (safe, intro equalityI; clarsimp) (auto dest:transM)
qed

is_iff_rel for "cexp"
  using is_cardinal_iff is_function_space_iff unfolding cexp_rel_def is_cexp_def
  by (simp)

rel_closed for "cexp" unfolding cexp_rel_def by simp

end (* M_ZF_library *)

synthesize "is_cexp" from_definition assuming "nonempty"
notation is_cexp_fm (‹⋅_⇗↑_⇖ is _⋅›)
arity_theorem for "is_cexp_fm"

abbreviation
  cexp_r :: "[i,i,i⇒o] ⇒ i"  (‹_⇗↑_,_⇖›) where
  "cexp_r(x,y,M) ≡ cexp_rel(M,x,y)"

abbreviation
  cexp_r_set :: "[i,i,i] ⇒ i"  (‹_⇗↑_,_⇖›) where
  "cexp_r_set(x,y,M) ≡ cexp_rel(##M,x,y)"

context M_ZF_library
begin

lemma Card_cexp : "M(κ) ⟹ M(ν) ⟹ Card⇗M⇖(κ⇗↑ν,M⇖)"
  unfolding cexp_rel_def by simp

― ‹Restoring congruence rule, but NOTE: beware›
declare conj_cong[cong]

lemma eq_csucc_rel_ord :
  "Ord(i) ⟹ M(i) ⟹ (i⇧+)⇗M⇖ = (|i|⇗M⇖⇧+)⇗M⇖"
  using Card_rel_lt_iff Least_cong unfolding csucc_rel_def by auto

lemma lesspoll_succ_rel :
  assumes "Ord(κ)" "M(κ)"
  shows "κ ≲⇗M⇖ (κ⇧+)⇗M⇖"
  using csucc_rel_basic assms lt_Card_rel_imp_lesspoll_rel
    Card_rel_csucc_rel lepoll_rel_iff_leqpoll_rel
  by auto

lemma lesspoll_rel_csucc_rel :
  assumes "Ord(κ)"
    and types:"M(κ)" "M(d)"
  shows "d ≺⇗M⇖ (κ⇧+)⇗M⇖ ⟷ d ≲⇗M⇖ κ"
proof
  assume "d ≺⇗M⇖ (κ⇧+)⇗M⇖"
  moreover
  note Card_rel_csucc_rel assms Card_rel_is_Ord
  moreover from calculation
  have "Card⇗M⇖((κ⇧+)⇗M⇖)" "M((κ⇧+)⇗M⇖)" "Ord((κ⇧+)⇗M⇖)"
    using Card_rel_is_Ord by simp_all
  moreover from calculation
  have "d ≺⇗M⇖ (|κ|⇗M⇖⇧+)⇗M⇖" "d ≈⇗M⇖ |d|⇗M⇖"
    using eq_csucc_rel_ord[OF _ ‹M(κ)›]
      lesspoll_rel_imp_eqpoll_rel eqpoll_rel_sym by simp_all
  moreover from calculation
  have "|d|⇗M⇖ < (|κ|⇗M⇖⇧+)⇗M⇖"
    using lesspoll_cardinal_lt_rel by simp
  moreover from calculation
  have "|d|⇗M⇖ ≲⇗M⇖ |κ|⇗M⇖"
    using Card_rel_lt_csucc_rel_iff le_imp_lepoll_rel by simp
  moreover from calculation
  have "|d|⇗M⇖ ≲⇗M⇖ κ"
    using Ord_cardinal_rel_eqpoll_rel lepoll_rel_eq_trans
    by simp
  ultimately
  show "d ≲⇗M⇖ κ"
    using eq_lepoll_rel_trans by simp
next
  from ‹Ord(κ)›
  have "κ < (κ⇧+)⇗M⇖" "Card⇗M⇖((κ⇧+)⇗M⇖)" "M((κ⇧+)⇗M⇖)"
    using Card_rel_csucc_rel lt_csucc_rel_iff types eq_csucc_rel_ord[OF _ ‹M(κ)›]
    by simp_all
  then
  have "κ ≺⇗M⇖ (κ⇧+)⇗M⇖"
  using lt_Card_rel_imp_lesspoll_rel[OF _ ‹κ <_›] types by simp
  moreover
  assume "d ≲⇗M⇖ κ"
  ultimately
  have "d ≲⇗M⇖ (κ⇧+)⇗M⇖"
    using Card_rel_csucc_rel types lesspoll_succ_rel lepoll_rel_trans ‹Ord(κ)›
    by simp
  moreover
  from ‹d ≲⇗M⇖ κ› ‹Ord(κ)›
  have "(κ⇧+)⇗M⇖ ≲⇗M⇖ κ" if "d ≈⇗M⇖ (κ⇧+)⇗M⇖"
    using eqpoll_rel_sym[OF that] types eq_lepoll_rel_trans[OF _ ‹d≲⇗M⇖κ›]
    by simp
  moreover from calculation ‹κ ≺⇗M⇖ (κ⇧+)⇗M⇖›
  have False if "d ≈⇗M⇖ (κ⇧+)⇗M⇖"
    using lesspoll_rel_irrefl[OF _ ‹M((κ⇧+)⇗M⇖)›] lesspoll_rel_trans1 types that
    by auto
  ultimately
  show "d ≺⇗M⇖ (κ⇧+)⇗M⇖"
    unfolding lesspoll_rel_def by auto
qed

lemma Infinite_imp_nats_lepoll :
  assumes "Infinite(X)" "n ∈ ω"
  shows "n ≲ X"
  using ‹n ∈ ω›
proof (induct)
  case 0
  then
  show ?case using empty_lepollI by simp
next
  case (succ x)
  show ?case
  proof -
    from ‹Infinite(X)› and ‹x ∈ ω›
    have "¬ (x ≈ X)"
      using eqpoll_sym unfolding Finite_def by auto
    with ‹x ≲ X›
    obtain f where "f ∈ inj(x,X)" "f ∉ surj(x,X)"
      unfolding bij_def eqpoll_def by auto
    moreover from this
    obtain b where "b ∈ X" "∀a∈x. f`a ≠ b"
      using inj_is_fun unfolding surj_def by auto
    ultimately
    have "f ∈ inj(x,X-{b})"
      unfolding inj_def by (auto intro:Pi_type)
    then
    have "cons(⟨x, b⟩, f) ∈ inj(succ(x), cons(b, X - {b}))"
      using inj_extend[of f x "X-{b}" x b] unfolding succ_def
      by (auto dest:mem_irrefl)
    moreover from ‹b∈X›
    have "cons(b, X - {b}) = X" by auto
    ultimately
    show "succ(x) ≲ X" by auto
  qed
qed

lemma nepoll_imp_nepoll_rel :
  assumes "¬ x ≈ X" "M(x)" "M(X)"
  shows "¬ (x ≈⇗M⇖ X)"
  using assms unfolding eqpoll_def eqpoll_rel_def by simp

lemma Infinite_imp_nats_lepoll_rel :
  assumes "Infinite(X)" "n ∈ ω"
    and types: "M(X)"
  shows "n ≲⇗M⇖ X"
  using ‹n ∈ ω›
proof (induct)
  case 0
  then
  show ?case using empty_lepoll_relI types by simp
next
  case (succ x)
  show ?case
  proof -
    from ‹Infinite(X)› and ‹x ∈ ω›
    have "¬ (x ≈ X)" "M(x)" "M(succ(x))"
      using eqpoll_sym unfolding Finite_def by auto
    then
    have "¬ (x ≈⇗M⇖ X)"
      using nepoll_imp_nepoll_rel types by simp
    with ‹x ≲⇗M⇖ X›
    obtain f where "f ∈ inj⇗M⇖(x,X)" "f ∉ surj⇗M⇖(x,X)" "M(f)"
      unfolding bij_rel_def eqpoll_rel_def by auto
    with ‹M(X)› ‹M(x)›
    have "f∉surj(x,X)" "f∈inj(x,X)"
      using surj_rel_char by simp_all
    moreover
    from this
    obtain b where "b ∈ X" "∀a∈x. f`a ≠ b"
      using inj_is_fun unfolding surj_def by auto
    moreover
    from this calculation ‹M(x)›
    have "f ∈ inj(x,X-{b})" "M(<x,b>)"
      unfolding inj_def using transM[OF _ ‹M(X)›]
      by (auto intro:Pi_type)
    moreover
    from this
    have "cons(⟨x, b⟩, f) ∈ inj(succ(x), cons(b, X - {b}))" (is "?g∈_")
      using inj_extend[of f x "X-{b}" x b] unfolding succ_def
      by (auto dest:mem_irrefl)
    moreover
    note ‹M(<x,b>)› ‹M(f)› ‹b∈X› ‹M(X)› ‹M(succ(x))›
    moreover from this
    have "M(?g)" "cons(b, X - {b}) = X" by auto
    moreover from calculation
    have "?g∈inj_rel(M,succ(x),X)"
      using mem_inj_abs by simp
    with ‹M(?g)›
    show "succ(x) ≲⇗M⇖ X" using lepoll_relI by simp
  qed
qed

lemma lepoll_rel_imp_lepoll : "A ≲⇗M⇖ B ⟹ M(A) ⟹ M(B) ⟹ A ≲ B"
  unfolding lepoll_rel_def by auto

lemma zero_lesspoll_rel : assumes "0<κ" "M(κ)" shows "0 ≺⇗M⇖ κ"
  using assms eqpoll_rel_0_iff[THEN iffD1, of κ] eqpoll_rel_sym
  unfolding lesspoll_rel_def lepoll_rel_def
  by (auto simp add:inj_def)

lemma lepoll_rel_nat_imp_Infinite : "ω ≲⇗M⇖ X ⟹ M(X) ⟹ Infinite(X)"
  using  lepoll_nat_imp_Infinite lepoll_rel_imp_lepoll by simp

lemma InfCard_rel_imp_Infinite : "InfCard⇗M⇖(κ) ⟹ M(κ) ⟹ Infinite(κ)"
  using le_imp_lepoll_rel[THEN lepoll_rel_nat_imp_Infinite, of κ]
  unfolding InfCard_rel_def by simp

lemma lt_surj_rel_empty_imp_Card_rel :
  assumes "Ord(κ)" "⋀α. α < κ ⟹ surj⇗M⇖(α,κ) = 0"
    and types:"M(κ)"
  shows "Card⇗M⇖(κ)"
proof -
  {
    define min where "min≡μ x. ∃f[M]. f ∈ bij⇗M⇖(x,κ)"
    moreover
    note ‹Ord(κ)› ‹M(κ)›
    moreover
    assume "|κ|⇗M⇖ < κ"
    moreover from calculation 
    have "∃f. f ∈ bij⇗M⇖(min,κ)"
      using LeastI[of "λi. i ≈⇗M⇖ κ" κ, OF eqpoll_rel_refl]
      unfolding Card_rel_def cardinal_rel_def eqpoll_rel_def
      by (auto)
    moreover from calculation
    have "min < κ"
      using lt_trans1[of min "μ i. M(i) ∧ (∃f[M]. f ∈ bij⇗M⇖(i, κ))" κ]
       Least_le[of "λi. i ≈⇗M⇖ κ" "|κ|⇗M⇖", OF Ord_cardinal_rel_eqpoll_rel]
      unfolding Card_rel_def cardinal_rel_def eqpoll_rel_def
      by (simp)
    moreover
    note ‹min < κ ⟹ surj⇗M⇖(min,κ) = 0›
    ultimately
    have "False"
      unfolding bij_rel_def by simp
  }
  with assms
  show ?thesis
    using Ord_cardinal_rel_le[of κ] not_lt_imp_le[of "|κ|⇗M⇖" κ] le_anti_sym
    unfolding Card_rel_def by auto
qed

end (* M_ZF_library *)

relativize functional "mono_map" "mono_map_rel" external
relationalize "mono_map_rel" "is_mono_map"

notation mono_map_rel (‹mono'_map⇗_⇖'(_,_,_,_')›)

abbreviation
  mono_map_r_set  :: "[i,i,i,i,i]⇒i"  (‹mono'_map⇗_⇖'(_,_,_,_')›) where
  "mono_map⇗M⇖(a,r,b,s) ≡ mono_map_rel(##M,a,r,b,s)"

context M_ZF_library
begin

lemma mono_map_rel_char :
  assumes "M(a)" "M(b)"
  shows "mono_map⇗M⇖(a,r,b,s) = {f∈mono_map(a,r,b,s) . M(f)}"
  using assms function_space_rel_char unfolding mono_map_rel_def mono_map_def
  by auto

text‹Just a sample of porting results on \<^term>‹mono_map››
lemma mono_map_rel_mono :
  assumes
    "f ∈ mono_map⇗M⇖(A,r,B,s)" "B ⊆ C"
    and types:"M(A)" "M(B)" "M(C)"
  shows
    "f ∈ mono_map⇗M⇖(A,r,C,s)"
  using assms mono_map_mono mono_map_rel_char by auto

lemma nats_le_InfCard_rel :
  assumes "n ∈ ω" "InfCard⇗M⇖(κ)"
  shows "n ≤ κ"
  using assms Ord_is_Transset
    le_trans[of n ω κ, OF le_subset_iff[THEN iffD2]]
  unfolding InfCard_rel_def Transset_def by simp

lemma nat_into_InfCard_rel :
  assumes "n ∈ ω" "InfCard⇗M⇖(κ)"
  shows "n ∈ κ"
  using assms  le_imp_subset[of ω κ]
  unfolding InfCard_rel_def by auto

lemma Finite_cardinal_rel_in_nat [simp]:
  assumes "Finite(A)" "M(A)" shows "|A|⇗M⇖ ∈ ω"
proof -
  note assms
  moreover from this
  obtain n where "n ∈ ω" "M(n)" "A ≈ n"
    unfolding Finite_def by auto
  moreover from calculation
  obtain f where "f ∈ bij(A,n)" "f: A-||>n"
    using Finite_Fin[THEN fun_FiniteFunI, OF _ subset_refl] bij_is_fun
    unfolding eqpoll_def by auto
  ultimately
  have "A ≈⇗M⇖ n" unfolding eqpoll_rel_def by (auto dest:transM)
  with assms and ‹M(n)›
  have "n ≈⇗M⇖ A" using eqpoll_rel_sym by simp
  moreover
  note ‹n∈ω› ‹M(n)›
  ultimately
  show ?thesis
    using assms Least_le[of "λi. M(i) ∧ i ≈⇗M⇖ A" n]
      lt_trans1[of _ n ω, THEN ltD]
    unfolding cardinal_rel_def Finite_def
    by (auto dest!:naturals_lt_nat)
qed

lemma Finite_cardinal_rel_eq_cardinal :
  assumes "Finite(A)" "M(A)" shows "|A|⇗M⇖ = |A|"
proof -
  ― ‹Copy-paste from @{thm Finite_cardinal_rel_in_nat}›
  note assms
  moreover from this
  obtain n where "n ∈ ω" "M(n)" "A ≈ n"
    unfolding Finite_def by auto
  moreover from this
  have "|A| = n"
    using cardinal_cong[of A n]
      nat_into_Card[THEN Card_cardinal_eq, of n] by simp
  moreover from calculation
  obtain f where "f ∈ bij(A,n)" "f: A-||>n"
    using Finite_Fin[THEN fun_FiniteFunI, OF _ subset_refl] bij_is_fun
    unfolding eqpoll_def by auto
  ultimately
  have "A ≈⇗M⇖ n" unfolding eqpoll_rel_def by (auto dest:transM)
  with assms and ‹M(n)› ‹n∈ω›
  have "|A|⇗M⇖ = n"
    using cardinal_rel_cong[of A n]
      nat_into_Card_rel[THEN Card_rel_cardinal_rel_eq, of n]
    by simp
  with ‹|A| = n›
  show ?thesis by simp
qed

lemma Finite_imp_cardinal_rel_cons :
  assumes FA: "Finite(A)" and a: "a∉A" and types:"M(A)" "M(a)"
  shows "|cons(a,A)|⇗M⇖ = succ(|A|⇗M⇖)"
  using assms Finite_imp_cardinal_cons Finite_cardinal_rel_eq_cardinal by simp

lemma Finite_imp_succ_cardinal_rel_Diff :
  assumes "Finite(A)" "a ∈ A" "M(A)"
  shows "succ(|A-{a}|⇗M⇖) = |A|⇗M⇖"
proof -
  from assms
  have inM: "M(A-{a})" "M(a)" "M(A)" by (auto dest:transM)
  with ‹Finite(A)›
  have "succ(|A-{a}|⇗M⇖) = succ(|A-{a}|)"
    using Diff_subset[THEN subset_Finite,
        THEN Finite_cardinal_rel_eq_cardinal, of A "{a}"] by simp
  also from assms
  have "… = |A|"
    using Finite_imp_succ_cardinal_Diff by simp
  also from assms
  have "… = |A|⇗M⇖" using Finite_cardinal_rel_eq_cardinal by simp
  finally
  show ?thesis .
qed

lemma InfCard_rel_Aleph_rel :
  notes Aleph_rel_zero[simp]
  assumes "Ord(α)"
    and types: "M(α)"
  shows "InfCard⇗M⇖(ℵ⇘α⇙⇗M⇖)"
proof -
  have "¬ (ℵ⇘α⇙⇗M⇖ ∈ ω)"
  proof (cases "α=0")
    case True
    then show ?thesis using mem_irrefl by auto
  next
    case False
    with assms
    have "ω ∈ ℵ⇘α⇙⇗M⇖" using Ord_0_lt[of α] ltD by (auto dest:Aleph_rel_increasing)
    then show ?thesis using foundation by blast
  qed
  with assms
  have "¬ (|ℵ⇘α⇙⇗M⇖|⇗M⇖ ∈ ω)"
    using Card_rel_cardinal_rel_eq by auto
  with assms
  have "Infinite(ℵ⇘α⇙⇗M⇖)" using Ord_Aleph_rel by clarsimp
  with assms
  show ?thesis
    using Inf_Card_rel_is_InfCard_rel by simp
qed

lemmas Limit_Aleph_rel= InfCard_rel_Aleph_rel[THEN InfCard_rel_is_Limit]

bundle Ord_dests = Limit_is_Ord[dest] Card_rel_is_Ord[dest]
bundle Aleph_rel_dests = Aleph_rel_cont[dest]
bundle Aleph_rel_intros = Aleph_rel_increasing[intro!]
bundle Aleph_rel_mem_dests = Aleph_rel_increasing[OF ltI, THEN ltD, dest]


end (* M_ZF_library *)

end