# 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 \<^theory>‹Transitive_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 ― ‹\<^locale>‹M_Pi_assumption_repl››

no_notation sum (infixr ‹+› 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 . fx = 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 \<^term>‹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_aleph + M_FiniteFun
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 . fx = 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) ∧ fx = 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) ∧ fx = 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})"
proof -
from assms
have "A - X = C - X ⟹ A = C" if "A∈F" "C∈F" 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 . A∈F})"  "(λA∈F. A-X) ∈ F → {A-X. A∈F}" (is "?H ∈ _") "M(λA∈F. A-X)"
using lam_type lam_replacement_Diff[THEN  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 "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
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 ― ‹\<^locale>‹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 ― ‹\<^locale>‹M_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→⇗M⇖B; f ∈ inj⇗M⇖(A,B); M(A); M(B)⟧ ⟹ f ∈ inj⇗M⇖(A,fA)"
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 [source] 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, fC)"
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

lemmas inj_rel_is_fun = inj_is_fun[OF mem_inj_rel]

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

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

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

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

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

lemmas bij_rel_is_fun = bij_rel_is_fun_rel[THEN mem_function_space_rel]

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

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

lemma fg_imp_bijective_rel:
assumes "f ∈ A →⇗M⇖B"  "g ∈ B→⇗M⇖A"  "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 ― ‹\<^locale>‹M_ZF_library››

subsection‹Discipline for \<^term>‹cexp››

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 ― ‹\<^locale>‹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_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" "∀a∈x. fa ≠ 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. fa ≠ 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

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 ― ‹\<^locale>‹M_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) = {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_lesspoll_rel_nat:
assumes "Finite(x)" "M(x)"
shows "x ≺⇗M⇖ nat"
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≈⇗M⇖ n" unfolding eqpoll_rel_def by (auto dest:transM)
with assms and ‹M(n)›
have "n ≈⇗M⇖ x" using eqpoll_rel_sym by simp
moreover
note ‹n∈ω› ‹M(n)›
ultimately
show ?thesis
using assms eq_lesspoll_rel_trans[OF ‹x≈⇗M⇖ n› 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 ≈⇗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 [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 ≈⇗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]

lemma f_imp_injective_rel:
assumes "f ∈ A →⇗M⇖ B" "∀x∈A. 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 "(λx∈A. 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)

lemma f_imp_surjective_rel:
assumes "f ∈ A →⇗M⇖ B" "⋀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

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 "(λx∈A. 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)

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 "(λx∈A. 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 ≈⇗M⇖ A'" "B ≈⇗M⇖ B'" "M(A)" "M(A')" "M(B)" "M(B')"
shows
"A →⇗M⇖ B ≈⇗M⇖ A' →⇗M⇖ B'"
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 →⇗M⇖ B . g O h O f"
let ?I="λ h ∈ A' →⇗M⇖ B' . converse(g) O h O converse(f)"
have go:"g O F O f : A' →⇗M⇖ B'" if "F: A →⇗M⇖ B" 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' →⇗M⇖ B'"
using comp_closed function_space_rel_char bij_rel_char
by auto
qed
have og:"converse(g) O F O converse(f) : A →⇗M⇖ B" if "F: A' →⇗M⇖ B'" 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 →⇗M⇖ B" (is "?G∈_")
using comp_closed function_space_rel_char bij_rel_char
by auto
qed
with go
have tc:"?H ∈ (A →⇗M⇖ B) → (A'→⇗M⇖ B')" "?I ∈ (A' →⇗M⇖ B') → (A→⇗M⇖ B)"
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' →⇗M⇖ B' ⟹ converse(g) O x O converse(f) ∈ A →⇗M⇖ B)"
by simp
next
show "M(A →⇗M⇖ B)" using assms by simp
next
show "M(A' →⇗M⇖ B')" using assms by simp
next
from og assms
have "?H O ?I = (λx∈A' →⇗M⇖ B' . (g O converse(g)) O x O (converse(f) O f))"
using lam_cong[OF refl[of "A' →⇗M⇖ B'"]] comp_assoc comp_lam
by auto
also
have "... = (λx∈A' →⇗M⇖ B' . 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 "... = (λx∈A' →⇗M⇖ B' . 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'→⇗M⇖B')" unfolding id_def by simp
finally
show "?H O ?I = id(A' →⇗M⇖ B')" .
next
from go assms
have "?I O ?H = (λx∈A →⇗M⇖ B . (converse(g) O g) O x O (f O converse(f)))"
using lam_cong[OF refl[of "A →⇗M⇖ B"]] comp_assoc comp_lam by auto
also
have "... = (λx∈A →⇗M⇖ B . 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 "... = (λx∈A →⇗M⇖ B . 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→⇗M⇖B)" unfolding id_def by simp
finally
show "?I O ?H = id(A →⇗M⇖ B)" .
next
from assms tc ‹M(?H)› ‹M(?I)›
show "?H ∈ (A→⇗M⇖ B) →⇗M⇖ (A'→⇗M⇖ B')" "M(?H)"
"?I ∈ (A'→⇗M⇖ B') →⇗M⇖ (A→⇗M⇖ B)"
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  lam_type, rule_tac  lam_type,
rule_tac  mem_function_space_rel_abs[THEN iffD2],
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 ⟹ fx : ν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 "ffst(z): ν2 →⇗M⇖ κ" by simp
ultimately
show "ffst(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  lam_replacement_hcomp2,
THEN  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  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) ≡ (λx∈X. bool_of_o(x∈A))"
― ‹the witnessing map for the thesis:›
assumes "M(X)"
shows "Pow⇗M⇖(X) ≈⇗M⇖ X →⇗M⇖ 2"
proof -
from assms
interpret M_Pi_assumption_repl M X "λx . 2"
have "lam_replacement(M, λx. bool_of_o(x∈A))" 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  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 "A∈Pow⇗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(x∈A))›
ultimately
show "d(A) : X →⇗M⇖ 2"
using function_space_rel_char lam_replacement_iff_lam_closed[THEN iffD1]
by (simp, rule_tac lam_type[of X "λx. bool_of_o(x∈A)" "λ_. 2", simplified])
auto
from ‹A∈Pow⇗M⇖(X)› ‹M(X)›
show "{y∈X. d(A)y = 1} = A"
using Pow_rel_char by auto
next
fix f
assume "f: X→⇗M⇖ 2"
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: X→2›] 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(x∈A))›
show "M(λx∈Pow⇗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  separation_in, of  "λx. x"]
lam_replacement_identity lam_replacement_constant by auto
with ‹M(A)›
have "{x∈A . x ∉ fx} ∈ Pow⇗M⇖(A)"
by (intro mem_Pow_rel_abs[THEN iffD2]) auto
ultimately
obtain d where "d∈A" "fd = {x∈A . x ∉ fx}"
unfolding surj_def by blast
show False
proof (cases "d ∈ fd")
case True
note ‹d ∈ fd›
also
note ‹fd = {x∈A . x ∉ fx}›
finally
have "d ∉ fd" using ‹d∈A› by simp
then
show False using ‹d ∈ f  d› by simp
next
case False
with ‹d∈A›
have "d ∈ {x∈A . x ∉ fx}" by simp
also from ‹fd = …›
have "… = fd" by simp
finally
show False using ‹d ∉ fd› 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 "λx∈A. 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  lam_replacement_hcomp2]
lam_replacement_identity lam_replacement_constant
lam_replacement_iff_lam_closed by auto

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

end`