Theory ZF_Library_Relative

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

theory ZF_Library_Relative
  imports
    Aleph_Relative ― ‹must be before theoryTransitive_Models.Cardinal_AC_Relative!›
    Cardinal_AC_Relative
    FiniteFun_Relative
begin

locale M_Pi_assumption_repl = M_Pi_replacement +
  fixes A f
  assumes A_in_M: "M(A)" and
  f_repl : "lam_replacement(M,f)" and
  f_closed : "x[M]. M(f(x))"
begin

sublocale M_Pi_assumptions M A f
    using Pi_replacement Pi_separation  A_in_M f_repl f_closed
      lam_replacement_Sigfun[THEN lam_replacement_imp_strong_replacement]
    by unfold_locales (simp_all add:transM[of _ A])

end ― ‹localeM_Pi_assumption_repl

no_notation sum (infixr + 65)
notation oadd (infixl + 65)

lemma (in M_cardinal_arith_jump) csucc_rel_cardinal_rel:
  assumes "Ord(κ)" "M(κ)"
  shows "(|κ|⇗M+)⇗M= (κ+)⇗M⇖"
proof (intro le_anti_sym) ― ‹we 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 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 termis_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_aleph + M_FiniteFun
begin

lemma Finite_Collect_imp: "Finite({xX . Q(x)})  Finite({xX . 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→⇗MY" "y. yY  Finite({xX . 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→⇗MY" "y. yY  Finite({xX . 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→⇗MY"
  "f  Finite_to_one⇗M⇖(X,Y)  yY  M(Y)  Finite({xX . M(x)  f`x = y})"
  unfolding Finite_to_one_rel_def by simp_all

lemma Diff_bij_rel:
  assumes "AF. X  A"
    and types: "M(F)" "M(X)" shows "(λAF. A-X)  bij⇗M⇖(F, {A-X. AF})"
proof -
  from assms
  have "A - X = C - X  A = C" if "AF" "CF" for A C
    using that subset_Diff_Un[of X A] subset_Diff_Un[of X C]
    by simp
  moreover
  note assms
  moreover from this
  have "M({A-X . AF})"  "(λAF. A-X)  F  {A-X. AF}" (is "?H  _") "M(λAF. A-X)"
    using lam_type lam_replacement_Diff[THEN [5] lam_replacement_hcomp2] lam_replacement_constant
      lam_replacement_identity transM[of _ F] lam_replacement_imp_strong_replacement RepFun_closed
      lam_replacement_imp_lam_closed
    by (simp,rule_tac lam_type,auto)
  ultimately
  show ?thesis
    using assms def_inj_rel def_surj_rel function_space_rel_char
    unfolding bij_rel_def
    by auto
qed

lemma function_space_rel_nonempty:
  assumes "bB"  and types: "M(B)" "M(A)"
  shows "(λxA. b) : A →⇗MB"
proof -
  note assms
  moreover from this
  have "M(λxA. 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 →⇗My" "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 ― ‹localeM_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 ― ‹localeM_Pi_assumptions

context M_ZF_library
begin

lemmas rel_apply_in_range = apply_in_codomain_Ord[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→⇗MB; 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 xrange(f) then converse(f)`x else b"
  assumes "f  inj⇗M⇖(B,A)" "bB" and types: "M(f)" "M(B)" "M(A)"
  shows "(λxA. ifx(x))  surj⇗M⇖(A,B)"
proof -
  from types and bB
  have "M(λxA. 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→⇗MB" "g  C→⇗MD"  "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→⇗MB" "g  C→⇗MD"  "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 ≲⇗MB  f[M]. f  inj⇗M⇖(A, B)"
  unfolding lepoll_rel_def .

― ‹Should the assumptions be on termf or on termA and termB?
    Should BOTH be intro rules?›
lemma lepoll_relI[intro]: "f  inj⇗M⇖(A, B)  M(f)  A ≲⇗MB"
  unfolding lepoll_rel_def by blast

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

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

lemma restrict_bij_rel:― ‹Unused›
  assumes "f  inj⇗M⇖(A,B)"  "CA"
    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 ≈⇗Mf `` 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

lemmas inj_rel_is_fun = inj_is_fun[OF mem_inj_rel]

lemma inj_rel_bij_rel_range: "f  inj⇗M⇖(A,B)  M(A)  M(B)  f  bij⇗M⇖(A,range(f))"
  using bij_rel_char inj_rel_char inj_bij_range by force

lemma bij_rel_is_inj_rel: "f  bij⇗M⇖(A,B)  M(A)  M(B)  f  inj⇗M⇖(A,B)"
  unfolding bij_rel_def by simp

lemma inj_rel_weaken_type: "[| f  inj⇗M⇖(A,B);  BD; M(A); M(B); M(D) |] ==> f  inj⇗M⇖(A,D)"
  using inj_rel_char inj_rel_is_fun inj_weaken_type by auto

lemma bij_rel_converse_bij_rel [TC]: "f  bij⇗M⇖(A,B)   M(A)  M(B) ==> converse(f): bij⇗M⇖(B,A)"
  using bij_rel_char by force

lemma bij_rel_is_fun_rel: "f  bij⇗M⇖(A,B)  M(A)  M(B)   f  A→⇗MB"
  using bij_rel_char mem_function_space_rel_abs bij_is_fun by simp

lemmas bij_rel_is_fun = bij_rel_is_fun_rel[THEN mem_function_space_rel]

lemma comp_bij_rel:
  "g  bij⇗M⇖(A,B)  f  bij⇗M⇖(B,C)  M(A)  M(B)  M(C)  (f O g)  bij⇗M⇖(A,C)"
  using bij_rel_char comp_bij by force

lemma inj_rel_converse_fun: "f  inj⇗M⇖(A,B)  M(A)  M(B)  converse(f)  range(f)→⇗MA"
proof -
  assume "f  inj⇗M⇖(A,B)" "M(A)" "M(B)"
  then
  have "M(f)" "M(converse(f))" "M(range(f))" "finj(A,B)"
    using inj_rel_char converse_closed range_closed
    by auto
  then
  show ?thesis
    using inj_converse_inj function_space_rel_char inj_is_fun M(A) by auto
qed

lemma fg_imp_bijective_rel:
  assumes "f  A →⇗MB"  "g  B→⇗MA"  "f O g = id(B)" "g O f = id(A)" "M(A)" "M(B)"
  shows "f  bij⇗M⇖(A,B)"
  using assms mem_bij_abs fg_imp_bijective mem_function_space_rel_abs[THEN iffD2] function_space_rel_char
  by auto

end ― ‹localeM_ZF_library

subsection‹Discipline for termcexp

relativize functional "cexp" "cexp_rel" external
relationalize "cexp_rel" "is_cexp"

context M_ZF_library
begin

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 ― ‹localeM_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,io]  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_rel_cexp_rel: "M(κ)  M(ν)  Card⇗M⇖(κ⇗↑ν,M)"
  unfolding cexp_rel_def by simp

― ‹Restoring congruence rule›
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" "ax. 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 bX
    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 ≈⇗MX)"
  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 ≲⇗MX"
  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 ≈⇗MX)"
      using nepoll_imp_nepoll_rel types by simp
    with x ≲⇗MX
    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 "fsurj(x,X)" "finj(x,X)"
      using surj_rel_char by simp_all
    moreover
    from this
    obtain b where "b  X" "ax. 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) bX M(X) M(succ(x))
    moreover from this
    have "M(?g)" "cons(b, X - {b}) = X" by auto
    moreover from calculation
    have "?ginj_rel(M,succ(x),X)"
      using mem_inj_abs by simp
    with M(?g)
    show "succ(x) ≲⇗MX" using lepoll_relI by simp
  qed
qed

lemma lepoll_rel_imp_lepoll: "A ≲⇗MB  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: "ω ≲⇗MX  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 ― ‹localeM_ZF_library

relativize functional "mono_map" "mono_map_rel" external
relationalize "mono_map_rel" "is_mono_map"
synthesize "is_mono_map" from_definition assuming "nonempty"

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) = {fmono_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 termmono_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_lesspoll_rel_nat:
  assumes "Finite(x)" "M(x)"
  shows "x ≺⇗Mnat"
proof -
  note assms
  moreover from this
  obtain n where "n  ω" "M(n)" "x  n"
    unfolding Finite_def by auto
  moreover from calculation
  obtain f where "f  bij(x,n)" "f: x-||>n"
    using Finite_Fin[THEN fun_FiniteFunI, OF _ subset_refl] bij_is_fun
    unfolding eqpoll_def by auto
  ultimately
  have "x≈⇗Mn" unfolding eqpoll_rel_def by (auto dest:transM)
  with assms and M(n)
  have "n ≈⇗Mx" using eqpoll_rel_sym by simp
  moreover
  note nω M(n)
  ultimately
  show ?thesis
    using assms eq_lesspoll_rel_trans[OF x≈⇗Mn n_lesspoll_rel_nat]
    by simp
qed

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 ≈⇗Mn" unfolding eqpoll_rel_def by (auto dest:transM)
  with assms and M(n)
  have "n ≈⇗MA" using eqpoll_rel_sym by simp
  moreover
  note nω M(n)
  ultimately
  show ?thesis
    using assms Least_le[of "λi. M(i)  i ≈⇗MA" 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 [source] 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 ≈⇗Mn" 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: "aA" 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]

lemma f_imp_injective_rel:
  assumes "f  A →⇗MB" "xA. d(f ` x) = x" "M(A)" "M(B)"
  shows "f  inj⇗M⇖(A, B)"
  using assms
  by (simp (no_asm_simp) add: def_inj_rel,auto intro: subst_context [THEN box_equals])

lemma lam_injective_rel:
  assumes "x. x  A  c(x)  B"
    "x. x  A  d(c(x)) = x"
    "x[M]. M(c(x))" "lam_replacement(M,c)"
    "M(A)" "M(B)"
  shows "(λxA. c(x))  inj⇗M⇖(A, B)"
  using assms function_space_rel_char lam_replacement_iff_lam_closed
  by (rule_tac d = d in f_imp_injective_rel)
    (auto simp add: lam_type)

lemma f_imp_surjective_rel:
  assumes "f  A →⇗MB" "y. y  B  d(y)  A" "y. y  B  f ` d(y) = y"
    "M(A)" "M(B)"
  shows "f  surj⇗M⇖(A, B)"
  using assms
  by (simp add: def_surj_rel, blast)

lemma lam_surjective_rel:
  assumes "x. x  A  c(x)  B"
    "y. y  B  d(y)  A"
    "y. y  B  c(d(y)) = y"
    "x[M]. M(c(x))" "lam_replacement(M,c)"
    "M(A)" "M(B)"
  shows "(λxA. c(x))  surj⇗M⇖(A, B)"
  using assms function_space_rel_char lam_replacement_iff_lam_closed
  by (rule_tac d = d in f_imp_surjective_rel)
    (auto simp add: lam_type)

lemma lam_bijective_rel:
  assumes "x. x  A  c(x)  B"
    "y. y  B  d(y)  A"
    "x. x  A  d(c(x)) = x"
    "y. y  B  c(d(y)) = y"
    "x[M]. M(c(x))" "lam_replacement(M,c)"
    "M(A)" "M(B)"
  shows "(λxA. c(x))  bij⇗M⇖(A, B)"
  using assms
  unfolding bij_rel_def
  by (blast intro!: lam_injective_rel lam_surjective_rel)

lemma function_space_rel_eqpoll_rel_cong:
  assumes
    "A ≈⇗MA'" "B ≈⇗MB'" "M(A)" "M(A')" "M(B)" "M(B')"
  shows
    "A →⇗MB ≈⇗MA' →⇗MB'"
proof -
  from assms(1)[THEN eqpoll_rel_sym] assms(2) assms lam_type
  obtain f g where "f  bij⇗M⇖(A',A)" "g  bij⇗M⇖(B,B')"
    by blast
  with assms
  have "converse(g) : bij⇗M⇖(B', B)" "converse(f): bij⇗M⇖(A, A')"
    using bij_converse_bij by auto
  let ?H="λ h  A →⇗MB . g O h O f"
  let ?I="λ h  A' →⇗MB' . converse(g) O h O converse(f)"
  have go:"g O F O f : A' →⇗MB'" if "F: A →⇗MB" for F
  proof -
    note assms f_ g_ that
    moreover from this
    have "g O F O f : A'  B'"
      using bij_rel_is_fun[OF g_] bij_rel_is_fun[OF f_] comp_fun
        mem_function_space_rel[OF F_]
      by blast
    ultimately
    show "g O F O f : A' →⇗MB'"
      using comp_closed function_space_rel_char bij_rel_char
      by auto
  qed
  have og:"converse(g) O F O converse(f) : A →⇗MB" if "F: A' →⇗MB'" for F
  proof -
    note assms that converse(f)  _ converse(g)  _
    moreover from this
    have "converse(g) O F O converse(f) : A  B"
      using bij_rel_is_fun[OF converse(g)_] bij_rel_is_fun[OF converse(f)_] comp_fun
        mem_function_space_rel[OF F_]
      by blast
    ultimately
    show "converse(g) O F O converse(f) : A →⇗MB" (is "?G_")
      using comp_closed function_space_rel_char bij_rel_char
      by auto
  qed
  with go
  have tc:"?H  (A →⇗MB)  (A'→⇗MB')" "?I  (A' →⇗MB')  (A→⇗MB)"
    using lam_type by auto
  with assms f_ g_
  have "M(g O x O f)" and "M(converse(g) O x O converse(f))" if "M(x)" for x
    using bij_rel_char comp_closed that by auto
  with assms f_ g_
  have "M(?H)" "M(?I)"
    using lam_replacement_iff_lam_closed[THEN iffD1,OF _ lam_replacement_comp']
      bij_rel_char by auto
  show ?thesis
    unfolding eqpoll_rel_def
  proof (intro rexI[of _ ?H] fg_imp_bijective_rel)
    from og go
    have "(x. x  A' →⇗MB'  converse(g) O x O converse(f)  A →⇗MB)"
      by simp
  next
    show "M(A →⇗MB)" using assms by simp
  next
    show "M(A' →⇗MB')" using assms by simp
  next
    from og assms
    have "?H O ?I = (λxA' →⇗MB' . (g O converse(g)) O x O (converse(f) O f))"
      using lam_cong[OF refl[of "A' →⇗MB'"]] comp_assoc comp_lam
      by auto
    also
    have "... = (λxA' →⇗MB' . id(B') O x O (id(A')))"
      using left_comp_inverse[OF mem_inj_rel[OF bij_rel_is_inj_rel]] f_
        right_comp_inverse[OF bij_is_surj[OF mem_bij_rel]] g_ assms
      by auto
    also
    have "... = (λxA' →⇗MB' . x)"
      using left_comp_id[OF fun_is_rel[OF mem_function_space_rel]]
        right_comp_id[OF fun_is_rel[OF mem_function_space_rel]] assms
      by auto
    also
    have "... = id(A'→⇗MB')" unfolding id_def by simp
    finally
    show "?H O ?I = id(A' →⇗MB')" .
  next
    from go assms
    have "?I O ?H = (λxA →⇗MB . (converse(g) O g) O x O (f O converse(f)))"
      using lam_cong[OF refl[of "A →⇗MB"]] comp_assoc comp_lam by auto
    also
    have "... = (λxA →⇗MB . id(B) O x O (id(A)))"
      using
        left_comp_inverse[OF mem_inj_rel[OF bij_rel_is_inj_rel[OF g_]]]
        right_comp_inverse[OF bij_is_surj[OF mem_bij_rel[OF f_]]] assms
      by auto
    also
    have "... = (λxA →⇗MB . x)"
      using left_comp_id[OF fun_is_rel[OF mem_function_space_rel]]
        right_comp_id[OF fun_is_rel[OF mem_function_space_rel]]
        assms
      by auto
    also
    have "... = id(A→⇗MB)" unfolding id_def by simp
    finally
    show "?I O ?H = id(A →⇗MB)" .
  next
    from assms tc M(?H) M(?I)
    show "?H  (A→⇗MB) →⇗M(A'→⇗MB')" "M(?H)"
      "?I  (A'→⇗MB') →⇗M(A→⇗MB)"
      using mem_function_space_rel_abs by auto
  qed
qed

lemma curry_eqpoll_rel:
  fixes ν1 ν2  κ
  assumes  "M(ν1)" "M(ν2)" "M(κ)"
  shows "ν1 →⇗M(ν2 →⇗Mκ) ≈⇗Mν1 × ν2 →⇗Mκ"
  unfolding eqpoll_rel_def
proof (intro rexI, rule lam_bijective_rel,
    rule_tac [1-2] mem_function_space_rel_abs[THEN iffD2],
    rule_tac [4] lam_type, rule_tac [8] lam_type,
    rule_tac [8] mem_function_space_rel_abs[THEN iffD2],
    rule_tac [11] lam_type, simp_all add:assms)
  let ?cur="λx. λwν1 × ν2. x ` fst(w) ` snd(w)"
  fix f z
  assume "f : ν1 →⇗M(ν2 →⇗Mκ)"
  moreover
  note assms
  moreover from calculation
  have "M(ν2 →⇗Mκ)"
    using function_space_rel_closed by simp
  moreover from calculation
  have "M(f)" "f : ν1  (ν2 →⇗Mκ)"
    using function_space_rel_char by (auto dest:transM)
  moreover from calculation
  have "x  ν1  f`x : ν2  κ" for x
    by (auto dest:transM intro!:mem_function_space_rel_abs[THEN iffD1])
  moreover from this
  show "(λaν1. λbν2. ?cur(f) ` a, b) = f"
    using Pi_type[OF f  ν1  ν2 →⇗Mκ, of "λ_.ν2  κ"] by simp
  moreover
  assume "z  ν1 × ν2"
  moreover from calculation
  have "f`fst(z): ν2 →⇗Mκ" by simp
  ultimately
  show "f`fst(z)`snd(z)  κ"
    using mem_function_space_rel_abs by (auto dest:transM)
next ― ‹one composition is the identity:›
  let ?cur="λx. λwν1 × ν2. x ` fst(w) ` snd(w)"
  fix f
  assume "f : ν1 × ν2 →⇗Mκ"
  with assms
  show "?cur(λxν1. λxaν2. f ` x, xa) = f"
    using function_space_rel_char mem_function_space_rel_abs
    by (auto dest:transM intro:fun_extension)
  fix x y
  assume "xν1" "yν2"
  with assms f : ν1 × ν2 →⇗Mκ
  show "f`x,y  κ"
    using function_space_rel_char mem_function_space_rel_abs
    by (auto dest:transM[of _ "ν1 × ν2 →⇗Mκ"])
next
  let ?cur="λx. λwν1 × ν2. x ` fst(w) ` snd(w)"
  note assms
  moreover from this
  show "x[M]. M(?cur(x))"
    using  lam_replacement_fst lam_replacement_snd
      lam_replacement_apply2[THEN [5] lam_replacement_hcomp2,
        THEN [1] lam_replacement_hcomp2, where h="(`)", OF
        lam_replacement_constant] lam_replacement_apply2
    by (auto intro: lam_replacement_iff_lam_closed[THEN iffD1, rule_format])
  moreover from calculation
  show "x  ν1 →⇗M(ν2 →⇗Mκ)  M(?cur(x))" for x
    by (auto dest:transM)
  moreover from assms
  show "lam_replacement(M, ?cur)"
    using lam_replacement_Lambda_apply_fst_snd by simp
  ultimately
  show "M(λxν1 →⇗M(ν2 →⇗Mκ). ?cur(x))"
    using lam_replacement_iff_lam_closed
    by (auto dest:transM)
  from assms
  show "y  ν1 × ν2 →⇗Mκ  x  ν1  M(λxaν2. y ` x, xa)" for x y
    using lam_replacement_apply_const_id
    by (rule_tac lam_replacement_iff_lam_closed[THEN iffD1, rule_format])
      (auto dest:transM)
  from assms
  show "y  ν1 × ν2 →⇗Mκ  M(λxν1. λxaν2. y ` x, xa)" for y
    using lam_replacement_apply2[THEN [5] lam_replacement_hcomp2,
        OF lam_replacement_constant lam_replacement_const_id]
      lam_replacement_Lambda_apply_Pair[of ν2]
    by (auto dest:transM
        intro!: lam_replacement_iff_lam_closed[THEN iffD1, rule_format])
qed

lemma Pow_rel_eqpoll_rel_function_space_rel:
  fixes d X
  notes bool_of_o_def [simp]
  defines [simp]:"d(A)  (λxX. bool_of_o(xA))"
    ― ‹the witnessing map for the thesis:›
  assumes "M(X)"
  shows "Pow⇗M⇖(X) ≈⇗MX →⇗M2"
proof -
  from assms
  interpret M_Pi_assumption_repl M X "λx . 2"
    by unfold_locales (simp_all add:lam_replacement_constant)
  have "lam_replacement(M, λx. bool_of_o(xA))" if "M(A)" for A
    using that lam_replacement_if lam_replacement_constant
      separation_in_constant by simp
  with assms
  have "lam_replacement(M, λx. d(x))"
    using separation_in_constant[THEN [3] lam_replacement_if, of "λ_.1" "λ_.0"]
      lam_replacement_identity lam_replacement_constant lam_replacement_Lambda_if_mem
    by simp
  show ?thesis
    unfolding eqpoll_rel_def
  proof (intro rexI, rule lam_bijective_rel)
    ― ‹We give explicit mutual inverses›
    fix A
    assume "APow⇗M⇖(X)"
    moreover
    note M(X)
    moreover from calculation
    have "M(A)" by (auto dest:transM)
    moreover
    note _  lam_replacement(M, λx. bool_of_o(xA))
    ultimately
    show "d(A) : X →⇗M2"
      using function_space_rel_char lam_replacement_iff_lam_closed[THEN iffD1]
      by (simp, rule_tac lam_type[of X "λx. bool_of_o(xA)" "λ_. 2", simplified])
        auto
    from APow⇗M⇖(X) M(X)
    show "{yX. d(A)`y = 1} = A"
      using Pow_rel_char by auto
  next
    fix f
    assume "f: X→⇗M2"
    with assms
    have "f: X 2" "M(f)" using function_space_rel_char by simp_all
    then
    show "d({y  X . f ` y = 1}) = f"
      using apply_type[OF f: X2] by (force intro:fun_extension)
    from M(X) M(f)
    show "{ya  X . f ` ya = 1}  Pow⇗M⇖(X)"
      using Pow_rel_char separation_equal_apply by auto
  next
    from assms lam_replacement(M, λx. d(x))
      A. _  lam_replacement(M, λx. bool_of_o(xA))
    show "M(λxPow⇗M⇖(X). d(x))" "lam_replacement(M, λx. d(x))"
      "x[M]. M(d(x))"
      using lam_replacement_iff_lam_closed[THEN iffD1] by auto
  qed (auto simp:M(X))
qed

lemma Pow_rel_bottom: "M(B)  0  Pow⇗M⇖(B)"
  using Pow_rel_char by simp

lemma cantor_surj_rel:
  assumes "M(f)" "M(A)"
  shows "f  surj⇗M⇖(A,Pow⇗M⇖(A))"
proof
  assume "f  surj⇗M⇖(A,Pow⇗M⇖(A))"
  with assms
  have "f  surj(A,Pow⇗M⇖(A))" using surj_rel_char by simp
  moreover
  note assms
  moreover from this
  have "M({x  A . x  f ` x})" "{x  A . x  f ` x} = A - {x  A . x  f ` x}"
    using lam_replacement_apply[THEN [4] separation_in, of  "λx. x"]
      lam_replacement_identity lam_replacement_constant by auto
  with M(A)
  have "{xA . x  f`x}  Pow⇗M⇖(A)"
    by (intro mem_Pow_rel_abs[THEN iffD2]) auto
  ultimately
  obtain d where "dA" "f`d = {xA . x  f`x}"
    unfolding surj_def by blast
  show False
  proof (cases "d  f`d")
    case True
    note d  f`d
    also
    note f`d = {xA . x  f`x}
    finally
    have "d  f`d" using dA by simp
    then
    show False using d  f ` d by simp
  next
    case False
    with dA
    have "d  {xA . x  f`x}" by simp
    also from f`d = 
    have " = f`d" by simp
    finally
    show False using d  f`d by simp
  qed
qed

lemma cantor_inj_rel: "M(f)  M(A)  f  inj⇗M⇖(Pow⇗M⇖(A),A)"
  using inj_rel_imp_surj_rel[OF _ Pow_rel_bottom, of f A A]
    cantor_surj_rel[of "λxA. if x  range(f) then converse(f) ` x else 0" A]
    lam_replacement_if separation_in_constant[of "range(f)"]
    lam_replacement_converse_app[THEN [5] lam_replacement_hcomp2]
    lam_replacement_identity lam_replacement_constant
    lam_replacement_iff_lam_closed by auto

end ― ‹localeM_ZF_library

end