# Theory Partial_Functions_Relative

```section‹Cohen forcing notions›

theory Partial_Functions_Relative
imports
Cardinal_Library_Relative
begin

text‹In this theory we introduce bounded partial functions and its relative
version; for historical reasons the relative version is based on a proper
definition of partial functions.

We note that finite partial functions are easier and are used to prove
some lemmas about finite sets in the theory
\<^theory>‹Transitive_Models.ZF_Library_Relative›.›

definition
Fn :: "[i,i,i] ⇒ i" where
"Fn(κ,I,J) ≡ ⋃{y . d ∈ Pow(I), y=(d→J) ∧ d≺κ}"

lemma domain_function_lepoll :
assumes "function(r)"
shows "domain(r) ≲ r"
proof -
let ?f="λx∈domain(r) . ⟨x,r`x⟩"
have "⟨x, r ` x⟩ ∈ r" if "⟨x, y⟩ ∈ r" for x y
proof -
have "x∈domain(r)" using that by auto
with assms
show ?thesis using function_apply_Pair by auto
qed
then
have "?f ∈ inj(domain(r), r)"
by(rule_tac lam_injective,auto)
then
show ?thesis unfolding lepoll_def
by force
qed

lemma function_lepoll:
assumes "r:d→J"
shows "r ≲ d"
proof -
let ?f="λx∈r . fst(x)"
note assms Pi_iff[THEN iffD1,OF assms]
moreover from calculation
have "r`fst(x) = snd(x)" if "x∈r" for x
using that apply_equality
by auto
ultimately
have "?f∈inj(r,d)"
by(rule_tac d= "λu . ⟨u, r`u⟩" in lam_injective,auto)
then
show ?thesis
unfolding lepoll_def
by auto
qed

lemma function_eqpoll :
assumes "r:d→J"
shows "r ≈ d"
using assms domain_of_fun domain_function_lepoll Pi_iff[THEN iffD1,OF assms]
eqpollI[OF function_lepoll[OF assms]] subset_imp_lepoll
by force

lemma Fn_char : "Fn(κ,I,J) = {f ∈ Pow(I×J) . function(f) ∧ f ≺ κ}" (is "?L=?R")
proof (intro equalityI subsetI)
fix x
assume "x ∈ ?R"
moreover from this
have "domain(x) ∈ Pow(I)" "domain(x) ≲ x" "x≺ κ"
using domain_function_lepoll
by auto
ultimately
show "x ∈ ?L"
unfolding Fn_def
using lesspoll_trans1 Pi_iff
by (auto,rule_tac rev_bexI[of "domain(x) → J"],auto)
next
fix x
assume "x ∈ ?L"
then
obtain d where "x:d→J" "d ∈ Pow(I)" "d≺κ"
unfolding Fn_def
by auto
moreover from this
have "x≺κ"
using function_lepoll[THEN lesspoll_trans1] by auto
moreover from calculation
have "x ∈ Pow(I×J)" "function(x)"
using Pi_iff by auto
ultimately
show "x ∈ ?R" by simp
qed

lemma zero_in_Fn:
assumes "0 < κ"
shows "0 ∈ Fn(κ, I, J)"
using lt_Card_imp_lesspoll assms zero_lesspoll
unfolding Fn_def
by (simp,rule_tac x="0→J" in bexI,simp)
(rule ReplaceI[of _ 0],simp_all)

lemma Fn_nat_eq_FiniteFun: "Fn(nat,I,J) = I -||> J"
proof (intro equalityI subsetI)
fix x
assume "x ∈ I -||> J"
then
show "x ∈ Fn(nat,I,J)"
proof (induct)
case emptyI
then
show ?case
using zero_in_Fn ltI
by simp
next
case (consI a b h)
then
obtain d where "h:d→J" "d≺nat" "d⊆I"
unfolding Fn_def by auto
moreover from this
have "Finite(d)"
using lesspoll_nat_is_Finite by simp
ultimately
have "h : d -||> J"
using fun_FiniteFunI Finite_into_Fin by blast
note ‹h:d→J›
moreover from this
have "domain(cons(⟨a, b⟩, h)) = cons(a,d)" (is "domain(?h) = ?d")
and "domain(h) = d"
using domain_of_fun by simp_all
moreover
note consI
moreover from calculation
have "cons(⟨a, b⟩, h) ∈ cons(a,d) → J"
using fun_extend3 by simp
moreover from ‹Finite(d)›
have "Finite(cons(a,d))" by simp
moreover from this
have "cons(a,d) ≺ nat" using Finite_imp_lesspoll_nat by simp
ultimately
show ?case
unfolding Fn_def
by (simp,rule_tac x="?d→J" in bexI)
(force dest:app_fun)+
qed
next
fix x
assume "x ∈ Fn(nat,I,J)"
then
obtain d where "x:d→J" "d ∈ Pow(I)" "d≺nat"
unfolding Fn_def
by auto
moreover from this
have "Finite(d)"
using lesspoll_nat_is_Finite by simp
moreover from calculation
have "d ∈ Fin(I)"
using Finite_into_Fin[of d] Fin_mono by auto
ultimately
show "x ∈ I -||> J" using fun_FiniteFunI FiniteFun_mono by blast
qed

lemma Fn_nat_subset_Pow: "Fn(κ,I,J) ⊆ Pow(I×J)"
using Fn_char by auto

lemma FnI:
assumes "p : d → J" "d ⊆ I" "d ≺ κ"
shows "p ∈ Fn(κ,I,J)"
using assms
unfolding Fn_def by auto

lemma FnD[dest]:
assumes "p ∈ Fn(κ,I,J)"
shows "∃d. p : d → J ∧ d ⊆ I ∧ d ≺ κ"
using assms
unfolding Fn_def by auto

lemma Fn_is_function: "p ∈ Fn(κ,I,J) ⟹ function(p)"
unfolding Fn_def using fun_is_function by auto

lemma Fn_csucc:
assumes "Ord(κ)"
shows "Fn(csucc(κ),I,J) = ⋃{y . d ∈ Pow(I), y=(d→J) ∧ d≲κ}"
using assms
unfolding Fn_def using lesspoll_csucc by (simp)

definition
FnleR :: "i ⇒ i ⇒ o" (infixl ‹⊇› 50) where
"f ⊇ g ≡ g ⊆ f"

lemma FnleR_iff_subset [iff]: "f ⊇ g ⟷ g ⊆ f"
unfolding FnleR_def ..

definition
Fnlerel :: "i ⇒ i" where
"Fnlerel(A) ≡ Rrel(λx y. x ⊇ y,A)"

definition
Fnle :: "[i,i,i] ⇒ i" where
"Fnle(κ,I,J) ≡ Fnlerel(Fn(κ,I,J))"

lemma FnleI[intro]:
assumes "p ∈ Fn(κ,I,J)" "q ∈ Fn(κ,I,J)" "p ⊇ q"
shows "⟨p,q⟩ ∈ Fnle(κ,I,J)"
using assms unfolding Fnlerel_def Fnle_def FnleR_def Rrel_def
by auto

lemma FnleD[dest]:
assumes "⟨p,q⟩ ∈ Fnle(κ,I,J)"
shows "p ∈ Fn(κ,I,J)" "q ∈ Fn(κ,I,J)" "p ⊇ q"
using assms unfolding Fnlerel_def Fnle_def FnleR_def Rrel_def
by auto

definition PFun_Space_Rel :: "[i,i⇒o, i] ⇒ i"  ("_⇀⇗_⇖_")
where "A ⇀⇗M⇖ B ≡ {f ∈ Pow(A×B) . M(f) ∧ function(f)}"

lemma (in M_library) PFun_Space_subset_Powrel :
assumes "M(A)" "M(B)"
shows "A ⇀⇗M⇖ B = {f ∈ Pow⇗M⇖(A×B) . function(f)}"
using Pow_rel_char assms
unfolding PFun_Space_Rel_def
by auto

lemma (in M_library) PFun_Space_closed :
assumes "M(A)" "M(B)"
shows "M(A ⇀⇗M⇖ B)"
using assms PFun_Space_subset_Powrel separation_is_function
by auto

lemma pfun_is_function :
"f ∈ A⇀⇗M⇖ B ⟹ function(f)"
unfolding PFun_Space_Rel_def by simp

lemma pfun_range :
"f ∈ A ⇀⇗M⇖ B ⟹ range(f) ⊆ B"
unfolding PFun_Space_Rel_def by auto

lemma pfun_domain :
"f ∈ A ⇀⇗M⇖ B ⟹ domain(f) ⊆ A"
unfolding PFun_Space_Rel_def by auto

lemma Un_filter_fun_space_closed:
assumes "G ⊆ I → J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I→ J . d ⊇ f ∧ d ⊇ g"
shows "⋃G ∈ Pow(I×J)" "function(⋃G)"
proof -
from assms
show "⋃G ∈ Pow(I×J)"
using Union_Pow_iff
unfolding Pi_def
by auto
next
show "function(⋃G)"
unfolding function_def
proof(auto)
fix B B' x y y'
assume "B ∈ G" "⟨x, y⟩ ∈ B" "B' ∈ G" "⟨x, y'⟩ ∈ B'"
moreover from assms this
have "B ∈ I → J" "B' ∈ I → J"
by auto
moreover from calculation assms(2)[of B B']
obtain d where "d ⊇ B"  "d ⊇ B'" "d∈I → J"  "⟨x, y⟩ ∈ d" "⟨x, y'⟩ ∈ d"
using subsetD[OF ‹G⊆_›]
by auto
then
show "y=y'"
using fun_is_function[OF ‹d∈_›]
unfolding function_def
by force
qed
qed

lemma Un_filter_is_fun :
assumes "G ⊆ I → J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I→ J . d⊇f ∧ d⊇g" "G≠0"
shows "⋃G ∈ I → J"
using assms Un_filter_fun_space_closed Pi_iff
proof(simp_all)
show "I⊆domain(⋃G)"
proof -
from ‹G≠0›
obtain f where "f⊆⋃G" "f∈G"
by auto
with ‹G⊆_›
have "f∈I→J" by auto
then
show ?thesis
using subset_trans[OF _ domain_mono[OF ‹f⊆⋃G›],of I]
unfolding Pi_def by auto
qed
qed

context M_Pi
begin

lemma mem_function_space_relD:
assumes "f ∈ function_space_rel(M,A,y)" "M(A)" "M(y)"
shows "f ∈ A → y" and "M(f)"
using assms function_space_rel_char by simp_all

lemma pfunI :
assumes "C⊆A" "f ∈ C →⇗M⇖ B" "M(C)" "M(B)"
shows "f∈ A ⇀⇗M⇖ B"
proof -
from assms
have "f ∈ C→B" "M(f)"
using mem_function_space_relD
by simp_all
with assms
show ?thesis
using Pi_iff
unfolding PFun_Space_Rel_def
by auto
qed

lemma zero_in_PFun_rel:
assumes "M(I)" "M(J)"
shows "0 ∈ I ⇀⇗M⇖ J"
using pfunI[of 0] nonempty mem_function_space_rel_abs assms
by simp

lemma pfun_subsetI :
assumes "f ∈ A ⇀⇗M⇖ B" "g⊆f" "M(g)"
shows "g∈ A ⇀⇗M⇖ B"
using assms function_subset
unfolding PFun_Space_Rel_def
by auto

lemma pfun_Un_filter_closed:
assumes "G ⊆I⇀⇗M⇖ J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I⇀⇗M⇖ J . d⊇f ∧ d⊇g"
shows "⋃G ∈ Pow(I×J)" "function(⋃G)"
proof -
from assms
show "⋃G ∈ Pow(I×J)"
using Union_Pow_iff
unfolding PFun_Space_Rel_def
by auto
next
show "function(⋃G)"
unfolding function_def
proof(auto)
fix B B' x y y'
assume "B ∈ G" "⟨x, y⟩ ∈ B" "B' ∈ G" "⟨x, y'⟩ ∈ B'"
moreover from calculation assms
obtain d where "d ∈ I ⇀⇗M⇖ J" "function(d)" "⟨x, y⟩ ∈ d"  "⟨x, y'⟩ ∈ d"
using pfun_is_function
by force
ultimately
show "y=y'"
unfolding function_def
by auto
qed
qed

lemma pfun_Un_filter_closed'':
assumes "G ⊆I⇀⇗M⇖ J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈G . d⊇f ∧ d⊇g"
shows "⋃G ∈ Pow(I×J)" "function(⋃G)"
proof -
from assms
have "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈I⇀⇗M⇖ J . d⊇f ∧ d⊇g"
using subsetD[OF assms(1),THEN  bexI]
by force
then
show "⋃G ∈ Pow(I×J)"  "function(⋃G)"
using assms pfun_Un_filter_closed
unfolding PFun_Space_Rel_def
by auto
qed

lemma pfun_Un_filter_closed':
assumes "G ⊆I⇀⇗M⇖ J" "⋀ f g . f∈G ⟹ g∈G ⟹ ∃d∈G . d⊇f ∧ d⊇g" "M(G)"
shows "⋃G ∈ I⇀⇗M⇖ J"
using assms pfun_Un_filter_closed''
unfolding PFun_Space_Rel_def
by auto

lemma pfunD :
assumes "f ∈ A⇀⇗M⇖ B"
shows "∃C[M]. C⊆A ∧ f ∈ C→B"
proof -
note assms
moreover from this
have "f∈Pow(A×B)" "function(f)" "M(f)"
unfolding PFun_Space_Rel_def
by simp_all
moreover from this
have "domain(f) ⊆ A" "f ∈ domain(f) → B" "M(domain(f))"
using assms Pow_iff[of f "A×B"] domain_subset Pi_iff
by auto
ultimately
show ?thesis by auto
qed

lemma pfunD_closed :
assumes "f ∈ A⇀⇗M⇖ B"
shows "M(f)"
using assms
unfolding PFun_Space_Rel_def by simp

lemma pfun_singletonI :
assumes "x ∈ A" "b ∈ B" "M(A)" "M(B)"
shows "{⟨x,b⟩} ∈ A⇀⇗M⇖ B"
using assms transM[of x A] transM[of b B]
unfolding PFun_Space_Rel_def function_def
by auto

lemma pfun_unionI :
assumes "f ∈ A⇀⇗M⇖ B" "g ∈ A⇀⇗M⇖ B" "domain(f)∩domain(g)=0"
shows "f∪g ∈ A⇀⇗M⇖ B"
using assms
unfolding PFun_Space_Rel_def function_def
by blast

lemma (in M_library) pfun_restrict_eq_imp_compat:
assumes "f ∈ I⇀⇗M⇖ J" "g ∈ I⇀⇗M⇖ J" "M(J)"
"restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))"
shows "f ∪ g ∈ I⇀⇗M⇖ J"
proof -
note assms
moreover from this
obtain C D where "f : C → J" "C ⊆ I" "D ⊆ I" "M(C)" "M(D)" "g : D → J"
using pfunD[of f] pfunD[of g] by force
moreover from calculation
have "f∪g ∈ C∪D → J"
using restrict_eq_imp_Un_into_Pi'[OF ‹f∈C→_› ‹g∈D→_›]
by auto
ultimately
show ?thesis
using pfunI[of "C∪D" _ "f∪g"] Un_subset_iff pfunD_closed function_space_rel_char
by auto
qed

lemma FiniteFun_pfunI :
assumes "f ∈ A-||> B" "M(A)" "M(B)"
shows "f ∈ A ⇀⇗M⇖ B"
using assms(1)
proof(induct)
case emptyI
then
show ?case
using assms nonempty mem_function_space_rel_abs pfunI[OF empty_subsetI, of 0]
by simp
next
case (consI a b h)
note consI
moreover from this
have "M(a)" "M(b)" "M(h)" "domain(h) ⊆ A"
using transM[OF _ ‹M(A)›] transM[OF _ ‹M(B)›]
FinD
FiniteFun_domain_Fin
pfunD_closed
by simp_all
moreover from calculation
have "{a}∪domain(h)⊆A" "M({a}∪domain(h))" "M(cons(<a,b>,h))" "domain(cons(<a,b>,h)) = {a}∪domain(h)"
by auto
moreover from calculation
have "cons(<a,b>,h) ∈ {a}∪domain(h) → B"
using FiniteFun_is_fun[OF FiniteFun.consI, of a A b B h]
by auto
ultimately
show "cons(<a,b>,h) ∈ A ⇀⇗M⇖ B"
using assms  mem_function_space_rel_abs pfunI
by simp_all
qed

lemma PFun_FiniteFunI :
assumes "f ∈ A ⇀⇗M⇖ B" "Finite(f)"
shows  "f ∈ A-||> B"
proof -
from assms
have "f∈Fin(A×B)" "function(f)"
using Finite_Fin Pow_iff
unfolding PFun_Space_Rel_def
by auto
then
show ?thesis
using FiniteFunI by simp
qed

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

definition
Fn_rel :: "[i⇒o,i,i,i] ⇒ i" (‹Fn⇗_⇖'(_,_,_')›) where
"Fn_rel(M,κ,I,J) ≡ {f ∈ I⇀⇗M⇖ J . f ≺⇗M⇖ κ}"
― ‹Eventually we can define \<^term>‹Fn_rel› as the relativization of \<^term>‹Fn››

context  M_library
begin

lemma Fn_rel_subset_PFun_rel : "Fn⇗M⇖(κ,I,J) ⊆ I⇀⇗M⇖ J"
unfolding Fn_rel_def by auto

lemma Fn_relI[intro]:
assumes "f : d → J" "d ⊆ I" "f ≺⇗M⇖ κ" "M(d)" "M(J)" "M(f)"
shows "f ∈ Fn_rel(M,κ,I,J)"
using assms pfunI mem_function_space_rel_abs
unfolding Fn_rel_def
by auto

lemma Fn_relD[dest]:
assumes "p ∈ Fn_rel(M,κ,I,J)"
shows "∃C[M]. C⊆I ∧ p : C → J ∧ p ≺⇗M⇖ κ"
using assms pfunD
unfolding Fn_rel_def
by simp

lemma Fn_rel_is_function:
assumes "p ∈ Fn_rel(M,κ,I,J)"
shows "function(p)" "M(p)" "p ≺⇗M⇖ κ" "p∈ I⇀⇗M⇖ J"
using assms
unfolding Fn_rel_def PFun_Space_Rel_def by simp_all

lemma Fn_rel_mono:
assumes "p ∈ Fn_rel(M,κ,I,J)" "κ ≺⇗M⇖ κ'" "M(κ)" "M(κ')"
shows "p ∈ Fn_rel(M,κ',I,J)"
using assms lesspoll_rel_trans[OF _ assms(2)] cardinal_rel_closed
Fn_rel_is_function(2)[OF assms(1)]
unfolding Fn_rel_def
by simp

lemma Fn_rel_mono':
assumes "p ∈ Fn_rel(M,κ,I,J)" "κ ≲⇗M⇖ κ'" "M(κ)" "M(κ')"
shows "p ∈ Fn_rel(M,κ',I,J)"
proof -
note assms
then
consider "κ ≺⇗M⇖ κ'"  | "κ ≈⇗M⇖ κ'"
using lepoll_rel_iff_leqpoll_rel
by auto
then
show ?thesis
proof(cases)
case 1
with assms show ?thesis using Fn_rel_mono by simp
next
case 2
then show ?thesis
using assms cardinal_rel_closed Fn_rel_is_function[OF assms(1)]
lesspoll_rel_eq_trans
unfolding Fn_rel_def
by simp
qed
qed

lemma Fn_csucc:
assumes "Ord(κ)" "M(κ)"
shows "Fn_rel(M,(κ⇧+)⇗M⇖,I,J) = {p∈ I⇀⇗M⇖ J . p  ≲⇗M⇖ κ}"   (is "?L=?R")
using assms
proof(intro equalityI)
show "?L ⊆ ?R"
proof(intro subsetI)
fix p
assume "p∈?L"
then
have "p ≺⇗M⇖ csucc_rel(M,κ)" "M(p)" "p∈ I⇀⇗M⇖ J"
using Fn_rel_is_function by simp_all
then
show "p∈?R"
using  assms lesspoll_rel_csucc_rel by simp
qed
next
show "?R⊆?L"
proof(intro subsetI)
fix p
assume "p∈?R"
then
have  "p∈ I⇀⇗M⇖ J" "p ≲⇗M⇖ κ"
using assms lesspoll_rel_csucc_rel by simp_all
then
show "p∈?L"
using  assms lesspoll_rel_csucc_rel pfunD_closed
unfolding Fn_rel_def
by simp
qed
qed

lemma Finite_imp_lesspoll_nat:
assumes "Finite(A)"
shows "A ≺ nat"
using assms subset_imp_lepoll[OF naturals_subset_nat] eq_lepoll_trans
n_lesspoll_nat eq_lesspoll_trans
unfolding Finite_def lesspoll_def by auto

lemma FinD_Finite :
assumes "a∈Fin(A)"
shows "Finite(a)"
using assms
by(induct,simp_all)

lemma Fn_rel_nat_eq_FiniteFun:
assumes "M(I)" "M(J)"
shows "I -||> J = Fn_rel(M,ω,I,J)"
proof(intro equalityI subsetI)
fix p
assume "p∈I -||> J"
with assms
have "p∈ I ⇀⇗M⇖ J" "Finite(p)"
using FiniteFun_pfunI FinD_Finite[OF subsetD[OF FiniteFun.dom_subset,OF ‹p∈_›]]
by auto
moreover from this
have "p ≺⇗M⇖ ω"
using Finite_lesspoll_rel_nat pfunD_closed[of p] n_lesspoll_rel_nat
by simp
ultimately
show "p∈ Fn_rel(M,ω,I,J)"
unfolding Fn_rel_def by simp
next
fix p
assume "p∈ Fn_rel(M,ω,I,J)"
then
have "p∈ I ⇀⇗M⇖ J"  "p ≺⇗M⇖ ω"
unfolding Fn_rel_def by simp_all
moreover from this
have "Finite(p)"
using Finite_cardinal_rel_Finite lesspoll_rel_nat_is_Finite_rel pfunD_closed
cardinal_rel_closed[of p]  Finite_cardinal_rel_iff'[THEN iffD1]
by simp
ultimately
show "p∈I -||> J"
using PFun_FiniteFunI
by simp
qed

lemma Fn_nat_abs:
assumes "M(I)" "M(J)"
shows "Fn(nat,I,J) = Fn_rel(M,ω,I,J)"
using assms Fn_rel_nat_eq_FiniteFun Fn_nat_eq_FiniteFun
by simp

lemma Fn_rel_singletonI:
assumes "x ∈ I" "j ∈ J" "1 ≺⇗M⇖ κ" "M(κ)" "M(I)" "M(J)"
shows "{⟨x,j⟩} ∈ Fn⇗M⇖(κ,I,J)"
using pfun_singletonI transM[of x] transM[of j] assms
eq_lesspoll_rel_trans[OF singleton_eqpoll_rel_1]
unfolding Fn_rel_def
by auto

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

definition
Fnle_rel :: "[i⇒o,i,i,i] ⇒ i" (‹Fnle⇗_⇖'(_,_,_')›) where
"Fnle_rel(M,κ,I,J) ≡ Fnlerel(Fn⇗M⇖(κ,I,J))"

abbreviation
Fn_r_set ::  "[i,i,i,i] ⇒ i" (‹Fn⇗_⇖'(_,_,_')›) where
"Fn_r_set(M) ≡ Fn_rel(##M)"

abbreviation
Fnle_r_set ::  "[i,i,i,i] ⇒ i" (‹Fnle⇗_⇖'(_,_,_')›) where
"Fnle_r_set(M) ≡ Fnle_rel(##M)"

context M_library
begin

lemma Fnle_relI[intro]:
assumes "p ∈ Fn_rel(M,κ,I,J)" "q ∈ Fn_rel(M,κ,I,J)" "p ⊇ q"
shows "⟨p, q⟩ ∈ Fnle_rel(M,κ,I,J)"
using assms unfolding Fnlerel_def Fnle_rel_def FnleR_def Rrel_def
by auto

lemma Fnle_relD[dest]:
assumes "⟨p, q⟩ ∈ Fnle_rel(M,κ,I,J)"
shows "p ∈ Fn_rel(M,κ,I,J)" "q ∈ Fn_rel(M,κ,I,J)" "p ⊇ q"
using assms unfolding Fnlerel_def Fnle_rel_def FnleR_def Rrel_def
by auto

lemma Fn_rel_closed[intro,simp]:
assumes "M(κ)" "M(I)" "M(J)"
shows "M(Fn⇗M⇖(κ,I,J))"
using assms separation_cardinal_rel_lesspoll_rel PFun_Space_closed
unfolding Fn_rel_def
by auto

lemma Fn_rel_subset_Pow:
assumes "M(κ)" "M(I)" "M(J)"
shows "Fn⇗M⇖(κ,I,J) ⊆ Pow(I×J)"
unfolding Fn_rel_def PFun_Space_Rel_def
by auto

lemma Fnle_rel_closed[intro,simp]:
assumes "M(κ)" "M(I)" "M(J)"
shows "M(Fnle⇗M⇖(κ,I,J))"
unfolding Fnle_rel_def Fnlerel_def Rrel_def FnleR_def
using assms supset_separation Fn_rel_closed
by auto

lemma zero_in_Fn_rel:
assumes "0<κ" "M(κ)" "M(I)" "M(J)"
shows "0 ∈ Fn⇗M⇖(κ, I, J)"
unfolding Fn_rel_def
using zero_in_PFun_rel zero_lesspoll_rel assms
by simp

lemma zero_top_Fn_rel:
assumes "p∈Fn⇗M⇖(κ, I, J)" "0<κ" "M(κ)" "M(I)" "M(J)"
shows "⟨p, 0⟩ ∈ Fnle⇗M⇖(κ, I, J)"
using assms zero_in_Fn_rel unfolding preorder_on_def refl_def trans_on_def
by auto

lemma preorder_on_Fnle_rel:
assumes "M(κ)" "M(I)" "M(J)"
shows "preorder_on(Fn⇗M⇖(κ, I, J), Fnle⇗M⇖(κ, I, J))"
unfolding preorder_on_def refl_def trans_on_def
by blast

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

context M_cardinal_library
begin

lemma lesspoll_nat_imp_lesspoll_rel:
assumes "A ≺ ω" "M(A)"
shows "A ≺⇗M⇖ ω"
proof -
note assms
moreover from this
obtain f n where "f∈bij⇗M⇖(A,n)" "n∈ω" "A ≈⇗M⇖ n"
using lesspoll_nat_is_Finite Finite_rel_def[of M A]
by auto
moreover from calculation
have "A ≲⇗M⇖ ω"
using lesspoll_nat_is_Finite Infinite_imp_nats_lepoll_rel[of ω n]
nat_not_Finite eq_lepoll_rel_trans[of A n ω]
by auto
moreover from calculation
have "¬ g ∈ bij⇗M⇖(A,ω)" for g
using mem_bij_rel unfolding lesspoll_def by auto
ultimately
show ?thesis
unfolding lesspoll_rel_def
by auto
qed

lemma Finite_imp_lesspoll_rel_nat:
assumes "Finite(A)" "M(A)"
shows "A ≺⇗M⇖ ω"
using Finite_imp_lesspoll_nat assms lesspoll_nat_imp_lesspoll_rel
by auto

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

context M_cardinal_library_extra
begin

lemma InfCard_rel_lesspoll_rel_Un:
includes Ord_dests
assumes "InfCard_rel(M,κ)" "A ≺⇗M⇖ κ" "B ≺⇗M⇖ κ"
and types: "M(κ)" "M(A)" "M(B)"
shows "A ∪ B ≺⇗M⇖ κ"
proof -
from assms
have "|A|⇗M⇖ < κ" "|B|⇗M⇖ < κ"
using lesspoll_rel_cardinal_rel_lt InfCard_rel_is_Card_rel
by auto
show ?thesis
proof (cases "Finite(A) ∧ Finite(B)")
case True
with assms
show ?thesis
using lesspoll_rel_trans2[OF _ le_imp_lepoll_rel, of _ nat κ]
Finite_imp_lesspoll_rel_nat[OF Finite_Un]
unfolding InfCard_rel_def
by simp
next
case False
with types
have "InfCard_rel(M,max(|A|⇗M⇖,|B|⇗M⇖))"
using Infinite_InfCard_rel_cardinal_rel InfCard_rel_is_Card_rel
le_trans[of nat] not_le_iff_lt[THEN iffD1, THEN leI, of "|A|⇗M⇖" "|B|⇗M⇖"]
unfolding max_def InfCard_rel_def
by auto
with ‹M(A)› ‹M(B)›
have "|A ∪ B|⇗M⇖ ≤ max(|A|⇗M⇖,|B|⇗M⇖)"
using cardinal_rel_Un_le[of "max(|A|⇗M⇖,|B|⇗M⇖)" A B]
not_le_iff_lt[THEN iffD1, THEN leI, of "|A|⇗M⇖" "|B|⇗M⇖" ]
unfolding max_def
by simp
moreover from ‹|A|⇗M⇖ < κ› ‹|B|⇗M⇖ < κ›
have "max(|A|⇗M⇖,|B|⇗M⇖) < κ"
unfolding max_def
by simp
ultimately
have "|A ∪ B|⇗M⇖ <  κ"
using lt_trans1
by blast
moreover
note ‹InfCard_rel(M,κ)›
moreover from calculation types
have "|A ∪ B|⇗M⇖ ≺⇗M⇖ κ"
using lt_Card_rel_imp_lesspoll_rel InfCard_rel_is_Card_rel
by simp
ultimately
show ?thesis
using cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[of "A ∪ B" "|A ∪ B|⇗M⇖" κ]
eqpoll_rel_sym types
by simp
qed
qed

lemma Fn_rel_unionI:
assumes "p ∈ Fn⇗M⇖(κ,I,J)" "q∈Fn⇗M⇖(κ,I,J)" "InfCard⇗M⇖(κ)"
"M(κ)" "M(I)" "M(J)" "domain(p) ∩ domain(q) = 0"
shows "p∪q ∈ Fn⇗M⇖(κ,I,J)"
proof -
note assms
moreover from calculation
have "p ≺⇗M⇖ κ" "q ≺⇗M⇖ κ" "M(p)" "M(q)"
using Fn_rel_is_function by simp_all
moreover from calculation
have "p∪q ≺⇗M⇖ κ"
using eqpoll_rel_sym cardinal_rel_eqpoll_rel InfCard_rel_lesspoll_rel_Un
by simp_all
ultimately
show ?thesis
unfolding Fn_rel_def
using pfun_unionI cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[OF _ ‹p∪q ≺⇗M⇖ _›]
by auto
qed

lemma restrict_eq_imp_compat_rel:
assumes "p ∈ Fn⇗M⇖(κ, I, J)" "q ∈ Fn⇗M⇖(κ, I, J)" "InfCard⇗M⇖(κ)" "M(J)" "M(κ)"
"restrict(p, domain(p) ∩ domain(q)) = restrict(q, domain(p) ∩ domain(q))"
shows "p ∪ q ∈ Fn⇗M⇖(κ, I, J)"
proof -
note assms
moreover from calculation
have "p ≺⇗M⇖ κ" "q ≺⇗M⇖ κ" "M(p)" "M(q)"
using Fn_rel_is_function by simp_all
moreover from calculation
have "p∪q ≺⇗M⇖ κ"
using InfCard_rel_lesspoll_rel_Un cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym]
by auto
ultimately
show ?thesis
unfolding Fn_rel_def
using pfun_restrict_eq_imp_compat cardinal_rel_eqpoll_rel
eq_lesspoll_rel_trans[OF _ ‹p∪q ≺⇗M⇖ _›]
by auto
qed

lemma InfCard_rel_imp_n_lesspoll_rel :
assumes "InfCard⇗M⇖(κ)" "M(κ)" "n∈ω"
shows "n ≺⇗M⇖ κ"
proof -
note assms
moreover from this
have "n ≺⇗M⇖ ω"
using n_lesspoll_rel_nat by simp
ultimately
show ?thesis
using lesspoll_rel_trans2 Infinite_iff_lepoll_rel_nat InfCard_rel_imp_Infinite nat_into_M
by simp
qed

lemma cons_in_Fn_rel:
assumes "x ∉ domain(p)" "p ∈ Fn⇗M⇖(κ,I,J)" "x ∈ I" "j ∈ J" "InfCard⇗M⇖(κ)"
"M(κ)" "M(I)" "M(J)"
shows "cons(⟨x,j⟩, p) ∈ Fn⇗M⇖(κ,I,J)"
using assms cons_eq Fn_rel_unionI[OF Fn_rel_singletonI[of x I j J] ‹p∈_›]
InfCard_rel_imp_n_lesspoll_rel
by auto

lemma dense_dom_dense:
assumes "x ∈ I" "InfCard⇗M⇖(κ)" "M(I)" "M(J)" "z∈J" "M(κ)" "p∈Fn⇗M⇖(κ, I, J)"
shows "∃d∈{ p ∈ Fn⇗M⇖(κ, I, J) . x ∈ domain(p) }. ⟨d,p⟩ ∈ Fnle⇗M⇖(κ, I, J)"
proof (cases "x ∈ domain(p)")
case True
with ‹x ∈ I› ‹p ∈ Fn⇗M⇖(κ, I, J)›
show ?thesis by auto
next
case False
note ‹p ∈ Fn⇗M⇖(κ, I, J)›
moreover from this and False and assms
have "cons(⟨x,z⟩, p) ∈ Fn⇗M⇖(κ, I, J)" "M(x)"
using cons_in_Fn_rel by (auto dest:transM)
ultimately
show ?thesis using Fn_relD by blast
qed

lemma (in M_cardinal_library) domain_lepoll_rel :
assumes "function(r)" "M(r)"
shows "domain(r) ≲⇗M⇖ r"
proof -
let ?f="λx∈domain(r) . ⟨x,r`x⟩"
have "⟨x, r ` x⟩ ∈ r" if "⟨x, y⟩ ∈ r" for x y
proof -
have "x∈domain(r)" using that by auto
with assms
show ?thesis using function_apply_Pair by auto
qed
then
have "?f ∈ inj(domain(r), r)"
by(rule_tac lam_injective,auto)
moreover note assms
moreover from calculation
have "M(?f)"
using lam_replacement_constant[of r] lam_replacement_identity assms
lam_replacement_apply lam_replacement_Pair[THEN  lam_replacement_hcomp2]
by(rule_tac lam_replacement_imp_lam_closed,auto dest:transM[of _ r])
ultimately
have "?f ∈ inj⇗M⇖(domain(r),r)" using inj_rel_char
by auto
with ‹M(?f)›
show ?thesis
using lepoll_relI by simp
qed

lemma dense_surj_dense:
assumes "x ∈ J" "InfCard⇗M⇖(κ)" "M(I)" "M(J)" "M(κ)" "p∈Fn⇗M⇖(κ, I, J)" "κ ≲⇗M⇖ I"
shows "∃d∈{ p ∈ Fn⇗M⇖(κ, I, J) . x ∈ range(p) }. ⟨d,p⟩ ∈ Fnle⇗M⇖(κ, I, J)"
proof -
from ‹p ∈ _› ‹M(J)› ‹x∈_› lesspoll_rel_def
have "domain(p) ⊆ I" "M(p)" "p ≺⇗M⇖ κ" "M(x)" "function(p)"
using pfun_domain[OF Fn_rel_is_function(4)] Fn_rel_is_function transM[of x J]
by simp_all
moreover from calculation assms
have 1:"domain(p) ≺⇗M⇖ κ" "M(domain(p))" "domain(p) ≺⇗M⇖ I"
using domain_lepoll_rel lesspoll_rel_trans1[of "domain(p)" p κ] lesspoll_rel_trans2
by auto
with calculation ‹κ ≲⇗M⇖ I› ‹M(I)› ‹M(κ)›
have "domain(p) ≠ I"
proof -
{assume "domain(p) = I"
with 1
have "domain(p) ≺⇗M⇖ domain(p)"
by auto
with ‹M(domain(p))›
have False
using lesspoll_rel_irrefl[of "domain(p)"] by simp
}
then show ?thesis by auto
qed
ultimately
obtain α where "α ∉ domain(p)" "α∈I"
by force
moreover note assms
moreover from calculation
have "cons(⟨α,x⟩, p) ∈ Fn⇗M⇖(κ, I, J)"
using InfCard_rel_Aleph_rel cons_in_Fn_rel[of α p κ I J x]
by auto
ultimately
show ?thesis
using Fnle_relI by blast
qed

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

end
```