Theory Cofinality
section‹Cofinality\label{sec:cofinality}›
theory Cofinality
imports
ZF_Library
begin
subsection‹Basic results and definitions›
text‹A set \<^term>‹X› is ∗‹cofinal› in \<^term>‹A› (with respect to the relation
\<^term>‹r›) if every element of \<^term>‹A› is ``bounded
above'' by some element of \<^term>‹X›. Note that \<^term>‹X› does not need
to be a subset of \<^term>‹A›.›
definition
cofinal :: "[i,i,i] ⇒ o" where
"cofinal(X,A,r) ≡ ∀a∈A. ∃x∈X. ⟨a,x⟩∈r ∨ a = x"
text‹A function is cofinal if it range is.›
definition
cofinal_fun :: "[i,i,i] ⇒ o" where
"cofinal_fun(f,A,r) ≡ ∀a∈A. ∃x∈domain(f). ⟨a,f`x⟩∈r ∨ a = f`x"
lemma cofinal_funI:
assumes "⋀a. a∈A ⟹ ∃x∈domain(f). ⟨a,f`x⟩∈r ∨ a = f`x"
shows "cofinal_fun(f,A,r)"
using assms unfolding cofinal_fun_def by simp
lemma cofinal_funD:
assumes "cofinal_fun(f,A,r)" "a∈A"
shows "∃x∈domain(f). ⟨a,f`x⟩∈r ∨ a = f`x"
using assms unfolding cofinal_fun_def by simp
lemma cofinal_in_cofinal:
assumes
"trans(r)" "cofinal(Y,X,r)" "cofinal(X,A,r)"
shows
"cofinal(Y,A,r)"
unfolding cofinal_def
proof
fix a
assume "a∈A"
moreover from ‹cofinal(X,A,r)›
have "b∈A⟹∃x∈X. ⟨b,x⟩∈r ∨ b=x" for b
unfolding cofinal_def by simp
ultimately
obtain y where "y∈X" "⟨a,y⟩∈r ∨ a=y" by auto
moreover from ‹cofinal(Y,X,r)›
have "c∈X⟹∃y∈Y. ⟨c,y⟩∈r ∨ c=y" for c
unfolding cofinal_def by simp
ultimately
obtain x where "x∈Y" "⟨y,x⟩∈r ∨ y=x" by auto
with ‹a∈A› ‹y∈X› ‹⟨a,y⟩∈r ∨ a=y› ‹trans(r)›
show "∃x∈Y. ⟨a,x⟩∈r ∨ a=x" unfolding trans_def by auto
qed
lemma codomain_is_cofinal:
assumes "cofinal_fun(f,A,r)" "f:C → D"
shows "cofinal(D,A,r)"
unfolding cofinal_def
proof
fix b
assume "b ∈ A"
moreover from assms
have "a∈A ⟹ ∃x∈domain(f). ⟨a, f ` x⟩ ∈ r ∨ a = f`x" for a
unfolding cofinal_fun_def by simp
ultimately
obtain x where "x∈domain(f)" "⟨b, f ` x⟩ ∈ r ∨ b = f`x"
by blast
moreover from ‹f:C → D› ‹x∈domain(f)›
have "f`x∈D"
using domain_of_fun apply_rangeI by simp
ultimately
show "∃y∈D. ⟨b, y⟩ ∈ r ∨ b = y" by auto
qed
lemma cofinal_range_iff_cofinal_fun:
assumes "function(f)"
shows "cofinal(range(f),A,r) ⟷ cofinal_fun(f,A,r)"
unfolding cofinal_fun_def
proof (intro iffI ballI)
fix a
assume "a∈A" ‹cofinal(range(f),A,r)›
then
obtain y where "y∈range(f)" "⟨a,y⟩ ∈ r ∨ a = y"
unfolding cofinal_def by blast
moreover from this
obtain x where "⟨x,y⟩∈f"
unfolding range_def domain_def converse_def by blast
moreover
note ‹function(f)›
ultimately
have "⟨a, f ` x⟩ ∈ r ∨ a = f ` x"
using function_apply_equality by blast
with ‹⟨x,y⟩∈f›
show "∃x∈domain(f). ⟨a, f ` x⟩ ∈ r ∨ a = f ` x" by blast
next
assume "∀a∈A. ∃x∈domain(f). ⟨a, f ` x⟩ ∈ r ∨ a = f ` x"
with assms
show "cofinal(range(f), A, r)"
using function_apply_Pair[of f] unfolding cofinal_def by fast
qed
lemma cofinal_comp:
assumes
"f∈ mono_map(C,s,D,r)" "cofinal_fun(f,D,r)" "h:B → C" "cofinal_fun(h,C,s)"
"trans(r)"
shows "cofinal_fun(f O h,D,r)"
unfolding cofinal_fun_def
proof
fix a
from ‹f∈ mono_map(C,s,D,r)›
have "f:C → D"
using mono_map_is_fun by simp
with ‹h:B → C›
have "domain(f) = C" "domain(h) = B"
using domain_of_fun by simp_all
moreover
assume "a ∈ D"
moreover
note ‹cofinal_fun(f,D,r)›
ultimately
obtain c where "c∈C" "⟨a, f ` c⟩ ∈ r ∨ a = f ` c"
unfolding cofinal_fun_def by blast
with ‹cofinal_fun(h,C,s)› ‹domain(h) = B›
obtain b where "b ∈ B" "⟨c, h ` b⟩ ∈ s ∨ c = h ` b"
unfolding cofinal_fun_def by blast
moreover from this and ‹h:B → C›
have "h`b ∈ C" by simp
moreover
note ‹f ∈ mono_map(C,s,D,r)› ‹c∈C›
ultimately
have "⟨f`c, f` (h ` b)⟩ ∈ r ∨ f`c = f` (h ` b)"
unfolding mono_map_def by blast
with ‹⟨a, f ` c⟩ ∈ r ∨ a = f ` c› ‹trans(r)› ‹h:B → C› ‹b∈B›
have "⟨a, (f O h) ` b⟩ ∈ r ∨ a = (f O h) ` b"
using transD by auto
moreover from ‹h:B → C› ‹domain(f) = C› ‹domain(h) = B›
have "domain(f O h) = B"
using range_fun_subset_codomain by blast
moreover
note ‹b∈B›
ultimately
show "∃x∈domain(f O h). ⟨a, (f O h) ` x⟩ ∈ r ∨ a = (f O h) ` x" by blast
qed
definition
cf_fun :: "[i,i] ⇒ o" where
"cf_fun(f,α) ≡ cofinal_fun(f,α,Memrel(α))"
lemma cf_funI[intro!]: "cofinal_fun(f,α,Memrel(α)) ⟹ cf_fun(f,α)"
unfolding cf_fun_def by simp
lemma cf_funD[dest!]: "cf_fun(f,α) ⟹ cofinal_fun(f,α,Memrel(α))"
unfolding cf_fun_def by simp
lemma cf_fun_comp:
assumes
"Ord(α)" "f∈ mono_map(C,s,α,Memrel(α))" "cf_fun(f,α)"
"h:B → C" "cofinal_fun(h,C,s)"
shows "cf_fun(f O h,α)"
using assms cofinal_comp[OF _ _ _ _ trans_Memrel] by auto
definition
cf :: "i⇒i" where
"cf(γ) ≡ μ β. ∃A. A⊆γ ∧ cofinal(A,γ,Memrel(γ)) ∧ β = ordertype(A,Memrel(γ))"
lemma Ord_cf [TC]: "Ord(cf(β))"
unfolding cf_def using Ord_Least by simp
lemma gamma_cofinal_gamma:
assumes "Ord(γ)"
shows "cofinal(γ,γ,Memrel(γ))"
unfolding cofinal_def by auto
lemma cf_is_ordertype:
assumes "Ord(γ)"
shows "∃A. A⊆γ ∧ cofinal(A,γ,Memrel(γ)) ∧ cf(γ) = ordertype(A,Memrel(γ))"
(is "?P(cf(γ))")
using gamma_cofinal_gamma LeastI[of ?P γ] ordertype_Memrel[symmetric] assms
unfolding cf_def by blast
lemma cf_fun_succ':
assumes "Ord(β)" "Ord(α)" "f:α→succ(β)"
shows "(∃x∈α. f`x=β) ⟷ cf_fun(f,succ(β))"
proof (intro iffI)
assume "(∃x∈α. f`x=β)"
with assms
show "cf_fun(f,succ(β))"
using domain_of_fun[OF ‹f:α→succ(β)›]
unfolding cf_fun_def cofinal_fun_def by auto
next
assume "cf_fun(f,succ(β))"
with assms
obtain x where "x∈α" "⟨β,f`x⟩ ∈ Memrel(succ(β)) ∨ β = f ` x"
using domain_of_fun[OF ‹f:α→succ(β)›]
unfolding cf_fun_def cofinal_fun_def by auto
moreover from ‹Ord(β)›
have "⟨β,y⟩ ∉ Memrel(succ(β))" for y
using foundation unfolding Memrel_def by blast
ultimately
show "∃x∈α. f ` x = β" by blast
qed
lemma cf_fun_succ:
"Ord(β) ⟹ f:1→succ(β) ⟹ f`0=β ⟹ cf_fun(f,succ(β))"
using cf_fun_succ' by blast
lemma ordertype_0_not_cofinal_succ:
assumes "ordertype(A,Memrel(succ(i))) = 0" "A⊆succ(i)" "Ord(i)"
shows "¬cofinal(A,succ(i),Memrel(succ(i)))"
proof
have 1:"ordertype(A,Memrel(succ(i))) = ordertype(0,Memrel(0))"
using ‹ordertype(A,Memrel(succ(i))) = 0› ordertype_0 by simp
from ‹A⊆succ(i)› ‹Ord(i)›
have "∃f. f ∈ ⟨A, Memrel(succ(i))⟩ ≅ ⟨0, Memrel(0)⟩"
using well_ord_Memrel well_ord_subset
ordertype_eq_imp_ord_iso[OF 1] Ord_0 by blast
then
have "A=0"
using ord_iso_is_bij bij_imp_eqpoll eqpoll_0_is_0 by blast
moreover
assume "cofinal(A, succ(i), Memrel(succ(i)))"
moreover
note ‹Ord(i)›
ultimately
show "False"
using not_mem_empty unfolding cofinal_def by auto
qed
text‹I thank Edwin Pacheco Rodríguez for the following lemma.›
lemma cf_succ:
assumes "Ord(α)"
shows "cf(succ(α)) = 1"
proof -
define f where "f ≡ {⟨0,α⟩}"
then
have "f : 1→succ(α)" "f`0 = α"
using fun_extend3[of 0 0 "succ(α)" 0 α] singleton_0 by auto
with assms
have "cf_fun(f,succ(α))"
using cf_fun_succ unfolding cofinal_fun_def by simp
from ‹f:1→succ(α)›
have "0∈domain(f)" using domain_of_fun by simp
define A where "A={f`0}"
with ‹cf_fun(f,succ(α))› ‹0∈domain(f)› ‹f`0=α›
have "cofinal(A,succ(α),Memrel(succ(α)))"
unfolding cofinal_def cofinal_fun_def by simp
moreover from ‹f`0=α› ‹A={f`0}›
have "A ⊆ succ(α)" unfolding succ_def by auto
moreover from ‹Ord(α)› ‹A⊆ succ(α)›
have "well_ord(A,Memrel(succ(α)))"
using Ord_succ well_ord_Memrel well_ord_subset relation_Memrel by blast
moreover from ‹Ord(α)›
have "¬(∃A. A ⊆ succ(α) ∧ cofinal(A, succ(α), Memrel(succ(α))) ∧ 0 = ordertype(A, Memrel(succ(α))))"
(is "¬?P(0)")
using ordertype_0_not_cofinal_succ unfolding cf_def by auto
moreover
have "1 = ordertype(A,Memrel(succ(α)))"
proof -
from ‹A={f`0}›
have "A≈1" using singleton_eqpoll_1 by simp
with ‹well_ord(A,Memrel(succ(α)))›
show ?thesis using nat_1I ordertype_eq_n by simp
qed
ultimately
show "cf(succ(α)) = 1" using Ord_1 Least_equality[of ?P 1]
unfolding cf_def by blast
qed
lemma cf_zero [simp]:
"cf(0) = 0"
unfolding cf_def cofinal_def using
ordertype_0 subset_empty_iff Least_le[of _ 0] by auto
lemma surj_is_cofinal: "f ∈ surj(δ,γ) ⟹ cf_fun(f,γ)"
unfolding surj_def cofinal_fun_def cf_fun_def
using domain_of_fun by force
lemma cf_zero_iff: "Ord(α) ⟹ cf(α) = 0 ⟷ α = 0"
proof (intro iffI)
assume "α = 0" "Ord(α)"
then
show "cf(α) = 0" using cf_zero by simp
next
assume "cf(α) = 0" "Ord(α)"
moreover from this
obtain A where "A⊆α" "cf(α) = ordertype(A,Memrel(α))"
"cofinal(A,α,Memrel(α))"
using cf_is_ordertype by blast
ultimately
have "cofinal(0,α,Memrel(α))"
using ordertype_zero_imp_zero[of A "Memrel(α)"] by simp
then
show "α=0"
unfolding cofinal_def by blast
qed
lemma cf_eq_one_iff:
assumes "Ord(γ)"
shows "cf(γ) = 1 ⟷ (∃α. Ord(α) ∧ γ = succ(α))"
proof (intro iffI)
assume "∃α. Ord(α) ∧ γ = succ(α)"
then
show "cf(γ) = 1" using cf_succ by auto
next
assume "cf(γ) = 1"
moreover from assms
obtain A where "A ⊆ γ" "cf(γ) = ordertype(A,Memrel(γ))"
"cofinal(A,γ,Memrel(γ))"
using cf_is_ordertype by blast
ultimately
have "ordertype(A,Memrel(γ)) = 1" by simp
moreover
define f where "f≡converse(ordermap(A,Memrel(γ)))"
moreover from this ‹ordertype(A,Memrel(γ)) = 1› ‹A ⊆ γ› assms
have "f ∈ surj(1,A)"
using well_ord_subset[OF well_ord_Memrel, THEN ordermap_bij,
THEN bij_converse_bij, of γ A] bij_is_surj
by simp
with ‹cofinal(A,γ,Memrel(γ))›
have "∀a∈γ. ⟨a, f`0⟩ ∈ Memrel(γ) ∨ a = f`0"
unfolding cofinal_def surj_def
by auto
with assms ‹A ⊆ γ› ‹f ∈ surj(1,A)›
show "∃α. Ord(α) ∧ γ = succ(α)"
using Ord_has_max_imp_succ[of γ "f`0"]
surj_is_fun[of f 1 A] apply_type[of f 1 "λ_.A" 0]
unfolding lt_def
by (auto intro:Ord_in_Ord)
qed
lemma ordertype_in_cf_imp_not_cofinal:
assumes
"ordertype(A,Memrel(γ)) ∈ cf(γ)"
"A ⊆ γ"
shows
"¬ cofinal(A,γ,Memrel(γ))"
proof
note ‹A ⊆ γ›
moreover
assume "cofinal(A,γ,Memrel(γ))"
ultimately
have "∃B. B ⊆ γ ∧ cofinal(B, γ, Memrel(γ)) ∧ ordertype(A,Memrel(γ)) = ordertype(B, Memrel(γ))"
(is "?P(ordertype(A,_))")
by blast
moreover from assms
have "ordertype(A,Memrel(γ)) < cf(γ)"
using Ord_cf ltI by blast
ultimately
show "False"
unfolding cf_def using less_LeastE[of ?P "ordertype(A,Memrel(γ))"]
by auto
qed
lemma cofinal_mono_map_cf:
assumes "Ord(γ)"
shows "∃j ∈ mono_map(cf(γ), Memrel(cf(γ)), γ, Memrel(γ)) . cf_fun(j,γ)"
proof -
note assms
moreover from this
obtain A where "A ⊆ γ" "cf(γ) = ordertype(A,Memrel(γ))"
"cofinal(A,γ,Memrel(γ))"
using cf_is_ordertype by blast
moreover
define j where "j ≡ converse(ordermap(A,Memrel(γ)))"
moreover from calculation
have "j :cf(γ) →⇩< γ"
using ordertype_ord_iso[THEN ord_iso_sym,
THEN ord_iso_is_mono_map, THEN mono_map_mono,
of A "Memrel(γ)" γ] well_ord_Memrel[THEN well_ord_subset]
by simp
moreover from calculation
have "j ∈ surj(cf(γ),A)"
using well_ord_Memrel[THEN well_ord_subset, THEN ordertype_ord_iso,
THEN ord_iso_sym, of γ A, THEN ord_iso_is_bij,
THEN bij_is_surj]
by simp
with ‹cofinal(A,γ,Memrel(γ))›
have "cf_fun(j,γ)"
using cofinal_range_iff_cofinal_fun[of j γ "Memrel(γ)"]
surj_range[of j "cf(γ)" A] surj_is_fun fun_is_function
by fastforce
with ‹j ∈ mono_map(_,_,_,_)›
show ?thesis by auto
qed
subsection‹The factorization lemma›
text‹In this subsection we prove a factorization lemma for cofinal functions
into ordinals, which shows that any cofinal function between ordinals can be
``decomposed'' in such a way that a commutative triangle of strictly increasing
maps arises.
The factorization lemma has a kind of
fundamental character, in that the rest of the basic results on cofinality
(for, instance, idempotence) follow easily from it, in a more algebraic way.
This is a consequence that the proof encapsulates uses of transfinite
recursion in the basic theory of cofinality; indeed, only one use is needed.
In the setting of Isabelle/ZF, this is convenient since the machinery of
recursion is pretty clumsy. On the downside, this way of presenting things
results in a longer proof of the factorization lemma. This approach was
taken by the author in the notes \<^cite>‹"apunte_st"› for an introductory course
in Set Theory.
To organize the use of the hypotheses of the factorization lemma,
we set up a locale containing all the relevant ingredients.
›
locale cofinal_factor =
fixes j δ ξ γ f
assumes j_mono: "j :ξ →⇩< γ"
and ords: "Ord(δ)" "Ord(ξ)" "Limit(γ)"
and f_type: "f: δ → γ"
begin
text‹Here, \<^term>‹f› is cofinal function from \<^term>‹δ› to \<^term>‹γ›, and the
ordinal \<^term>‹ξ› is meant to be the cofinality of \<^term>‹γ›. Hence, there exists
an increasing map \<^term>‹j› from \<^term>‹ξ› to \<^term>‹γ› by the last lemma.
The main goal is to construct an increasing function \<^term>‹g:ξ→δ› such that
the composition \<^term>‹f O g› is still cofinal but also increasing.›
definition
factor_body :: "[i,i,i] ⇒ o" where
"factor_body(β,h,x) ≡ (x∈δ ∧ j`β ≤ f`x ∧ (∀α<β . f`(h`α) < f`x)) ∨ x=δ"
definition
factor_rec :: "[i,i] ⇒ i" where
"factor_rec(β,h) ≡ μ x. factor_body(β,h,x)"
text‹\<^term>‹factor_rec› is the inductive step for the definition by transfinite
recursion of the ∗‹factor› function (called \<^term>‹g› above), which in
turn is obtained by minimizing the predicate \<^term>‹factor_body›. Next we show
that this predicate is monotonous.›
lemma factor_body_mono:
assumes
"β∈ξ" "α<β"
"factor_body(β,λx∈β. G(x),x)"
shows
"factor_body(α,λx∈α. G(x),x)"
proof -
from ‹α<β›
have "α∈β" using ltD by simp
moreover
note ‹β∈ξ›
moreover from calculation
have "α∈ξ" using ords ltD Ord_cf Ord_trans by blast
ultimately
have "j`α ∈ j`β" using j_mono mono_map_increasing by blast
moreover from ‹β∈ξ›
have "j`β∈γ"
using j_mono domain_of_fun apply_rangeI mono_map_is_fun by force
moreover from this
have "Ord(j`β)"
using Ord_in_Ord ords Limit_is_Ord by auto
ultimately
have "j`α ≤ j`β" unfolding lt_def by blast
then
have "j`β ≤ f`θ ⟹ j`α ≤ f`θ" for θ using le_trans by blast
moreover
have "f`((λw∈α. G(w))`y) < f`z" if "z∈δ" "∀x<β. f`((λw∈β. G(w))`x) < f`z" "y<α" for y z
proof -
note ‹y<α›
also
note ‹α<β›
finally
have "y<β" by simp
with ‹∀x<β. f`((λw∈β. G(w))`x) < f`z›
have "f ` ((λw∈β. G(w)) ` y) < f ` z" by simp
moreover from ‹y<α› ‹y<β›
have "(λw∈β. G(w)) ` y = (λw∈α. G(w)) ` y"
using beta_if by (auto dest:ltD)
ultimately show ?thesis by simp
qed
moreover
note ‹factor_body(β,λx∈β. G(x),x)›
ultimately
show ?thesis
unfolding factor_body_def by blast
qed
lemma factor_body_simp[simp]: "factor_body(α,g,δ)"
unfolding factor_body_def by simp
lemma factor_rec_mono:
assumes
"β∈ξ" "α<β"
shows
"factor_rec(α,λx∈α. G(x)) ≤ factor_rec(β,λx∈β. G(x))"
unfolding factor_rec_def
using assms ords factor_body_mono Least_antitone by simp
text‹We now define the factor as higher-order function.
Later it will be restricted to a set to obtain a bona fide function of
type @{typ i}.›
definition
factor :: "i ⇒ i" where
"factor(β) ≡ transrec(β,factor_rec)"
lemma factor_unfold:
"factor(α) = factor_rec(α,λx∈α. factor(x))"
using def_transrec[OF factor_def] .
lemma factor_mono:
assumes "β∈ξ" "α<β" "factor(α)≠δ" "factor(β)≠δ"
shows "factor(α) ≤ factor(β)"
proof -
have "factor(α) = factor_rec(α, λx∈α. factor(x))"
using factor_unfold .
also from assms and factor_rec_mono
have "... ≤ factor_rec(β, λx∈β. factor(x))"
by simp
also
have "factor_rec(β, λx∈β. factor(x)) = factor(β)"
using def_transrec[OF factor_def, symmetric] .
finally show ?thesis .
qed
text‹The factor satisfies the predicate body of the minimization.›
lemma factor_body_factor:
"factor_body(α,λx∈α. factor(x),factor(α))"
using ords factor_unfold[of α]
LeastI[of "factor_body(_,_)" δ]
unfolding factor_rec_def by simp
lemma factor_type [TC]: "Ord(factor(α))"
using ords factor_unfold[of α]
unfolding factor_rec_def by simp
text‹The value \<^term>‹δ› in \<^term>‹factor_body› (and therefore, in
\<^term>‹factor›) is meant to be a ``default value''. Whenever it is not
attained, the factor function behaves as expected: It is increasing
and its composition with \<^term>‹f› also is.›
lemma f_factor_increasing:
assumes "β∈ξ" "α<β" "factor(β)≠δ"
shows "f`factor(α) < f`factor(β)"
proof -
from assms
have "f ` ((λx∈β. factor(x)) ` α) < f ` factor(β)"
using factor_unfold[of β] ords LeastI[of "factor_body(β,λx∈β. factor(x))"]
unfolding factor_rec_def factor_body_def
by (auto simp del:beta_if)
with ‹α<β›
show ?thesis using ltD by auto
qed
lemma factor_increasing:
assumes "β∈ξ" "α<β" "factor(α)≠δ" "factor(β)≠δ"
shows "factor(α)<factor(β)"
using assms f_factor_increasing factor_mono by (force intro:le_neq_imp_lt)
lemma factor_in_delta:
assumes "factor(β) ≠ δ"
shows "factor(β) ∈ δ"
using assms factor_body_factor ords
unfolding factor_body_def by auto
text‹Finally, we define the (set) factor function as the restriction of
factor to the ordinal \<^term>‹ξ›.›
definition
fun_factor :: "i" where
"fun_factor ≡ λβ∈ξ. factor(β)"
lemma fun_factor_is_mono_map:
assumes "⋀β. β ∈ ξ ⟹ factor(β) ≠ δ"
shows "fun_factor ∈ mono_map(ξ, Memrel(ξ), δ, Memrel(δ))"
unfolding mono_map_def
proof (intro CollectI ballI impI)
text‹Proof that \<^term>‹fun_factor› respects membership:›
fix α β
assume "α∈ξ" "β∈ξ"
moreover
note assms
moreover from calculation
have "factor(α)≠δ" "factor(β)≠δ" "Ord(β)"
using factor_in_delta Ord_in_Ord ords by auto
moreover
assume "⟨α, β⟩ ∈ Memrel(ξ)"
ultimately
show "⟨fun_factor ` α, fun_factor ` β⟩ ∈ Memrel(δ)"
unfolding fun_factor_def
using ltI factor_increasing[THEN ltD] factor_in_delta
by simp
next
text‹Proof that it has the appropriate type:›
from assms
show "fun_factor : ξ → δ"
unfolding fun_factor_def
using ltI lam_type factor_in_delta by simp
qed
lemma f_fun_factor_is_mono_map:
assumes "⋀β. β ∈ ξ ⟹ factor(β) ≠ δ"
shows "f O fun_factor ∈ mono_map(ξ, Memrel(ξ), γ, Memrel(γ))"
unfolding mono_map_def
using f_type
proof (intro CollectI ballI impI comp_fun[of _ _ δ])
from assms
show "fun_factor : ξ → δ"
using fun_factor_is_mono_map mono_map_is_fun by simp
text‹Proof that \<^term>‹f O fun_factor› respects membership›
fix α β
assume "⟨α, β⟩ ∈ Memrel(ξ)"
then
have "α<β"
using Ord_in_Ord[of "ξ"] ltI ords by blast
assume "α∈ξ" "β∈ξ"
moreover from this and assms
have "factor(α)≠δ" "factor(β)≠δ" by auto
moreover
have "Ord(γ)" "γ≠0" using ords Limit_is_Ord by auto
moreover
note ‹α<β› ‹fun_factor : ξ → δ›
ultimately
show "⟨(f O fun_factor) ` α, (f O fun_factor) ` β⟩ ∈ Memrel(γ)"
using ltD[of "f ` factor(α)" "f ` factor(β)"]
f_factor_increasing apply_in_codomain_Ord f_type
unfolding fun_factor_def by auto
qed
end
text‹We state next the factorization lemma.›
lemma cofinal_fun_factorization:
notes le_imp_subset [dest] lt_trans2 [trans]
assumes
"Ord(δ)" "Limit(γ)" "f: δ → γ" "cf_fun(f,γ)"
shows
"∃g ∈ cf(γ) →⇩< δ. f O g : cf(γ) →⇩< γ ∧
cofinal_fun(f O g,γ,Memrel(γ))"
proof -
from ‹Limit(γ)›
have "Ord(γ)" using Limit_is_Ord by simp
then
obtain j where "j :cf(γ) →⇩< γ" "cf_fun(j,γ)"
using cofinal_mono_map_cf by blast
then
have "domain(j) = cf(γ)"
using domain_of_fun mono_map_is_fun by force
from ‹j ∈ _› assms
interpret cofinal_factor j δ "cf(γ)"
by (unfold_locales) (simp_all)
text‹The core of the argument is to show that the factor function
indeed maps into \<^term>‹δ›, therefore its values satisfy the first
disjunct of \<^term>‹factor_body›. This holds in turn because no
restriction of the factor composed with \<^term>‹f› to a proper initial
segment of \<^term>‹cf(γ)› can be cofinal in \<^term>‹γ› by definition of
cofinality. Hence there must be a witness that satisfies the first
disjunct.›
have factor_not_delta: "factor(β)≠δ" if "β ∈ cf(γ)" for β
text‹For this, we induct on \<^term>‹β› ranging over \<^term>‹cf(γ)›.›
proof (induct β rule:Ord_induct[OF _ Ord_cf[of γ]])
case 1 with that show ?case .
next
case (2 β)
then
have IH: "z∈β ⟹ factor(z)≠δ" for z by simp
define h where "h ≡ λx∈β. f`factor(x)"
from IH
have "z∈β ⟹ factor(z) ∈ δ" for z
using factor_in_delta by blast
with ‹f:δ→γ›
have "h : β → γ" unfolding h_def using apply_funtype lam_type by auto
then
have "h : β →⇩< γ"
unfolding mono_map_def
proof (intro CollectI ballI impI)
fix x y
assume "x∈β" "y∈β"
moreover from this and IH
have "factor(y) ≠ δ" by simp
moreover from calculation and ‹h ∈ β → γ›
have "h`x ∈ γ" "h`y ∈ γ" by simp_all
moreover from ‹β∈cf(γ)› and ‹y∈β›
have "y ∈ cf(γ)"
using Ord_trans Ord_cf by blast
moreover from this
have "Ord(y)"
using Ord_cf Ord_in_Ord by blast
moreover
assume "⟨x,y⟩ ∈ Memrel(β)"
moreover from calculation
have "x<y" by (blast intro:ltI)
ultimately
show "⟨h ` x, h ` y⟩ ∈ Memrel(γ)"
unfolding h_def using f_factor_increasing ltD by (auto)
qed
with ‹β∈cf(γ)› ‹Ord(γ)›
have "ordertype(h``β,Memrel(γ)) = β"
using mono_map_ordertype_image[of β] Ord_cf Ord_in_Ord by blast
also
note ‹β ∈cf(γ)›
finally
have "ordertype(h``β,Memrel(γ)) ∈ cf(γ)" by simp
moreover from ‹h ∈ β → γ›
have "h``β ⊆ γ"
using mono_map_is_fun Image_sub_codomain by blast
ultimately
have "¬ cofinal(h``β,γ,Memrel(γ))"
using ordertype_in_cf_imp_not_cofinal by simp
then
obtain α_0 where "α_0∈γ" "∀x∈h `` β. ¬ ⟨α_0, x⟩ ∈ Memrel(γ) ∧ α_0 ≠ x"
unfolding cofinal_def by auto
with ‹Ord(γ)› ‹h``β ⊆ γ›
have "∀x∈h `` β. x ∈ α_0"
using well_ord_Memrel[of γ] well_ord_is_linear[of γ "Memrel(γ)"]
unfolding linear_def by blast
from ‹α_0 ∈ γ› ‹j ∈ mono_map(_,_,γ,_)› ‹Ord(γ)›
have "j`β ∈ γ"
using mono_map_is_fun apply_in_codomain_Ord by force
with ‹α_0 ∈ γ› ‹Ord(γ)›
have "α_0 ∪ j`β ∈ γ"
using Un_least_mem_iff Ord_in_Ord by auto
with ‹cf_fun(f,γ)›
obtain θ where "θ∈domain(f)" "⟨α_0 ∪ j`β, f ` θ⟩ ∈ Memrel(γ) ∨ α_0 ∪ j`β = f ` θ"
by (auto simp add:cofinal_fun_def) blast
moreover from this and ‹f:δ→γ›
have "θ ∈ δ" using domain_of_fun by auto
moreover
note ‹Ord(γ)›
moreover from this and ‹f:δ→γ› ‹α_0 ∈ γ›
have "Ord(f`θ)"
using apply_in_codomain_Ord Ord_in_Ord by blast
moreover from calculation and ‹α_0 ∈ γ› and ‹Ord(δ)› and ‹j`β ∈ γ›
have "Ord(α_0)" "Ord(j`β)" "Ord(θ)"
using Ord_in_Ord by auto
moreover from ‹∀x∈h `` β. x ∈ α_0› ‹Ord(α_0)› ‹h:β→γ›
have "x∈β ⟹ h`x < α_0" for x
using fun_is_function[of h β "λ_. γ"]
Image_subset_Ord_imp_lt domain_of_fun[of h β "λ_. γ"]
by blast
moreover
have "x∈β ⟹ h`x < f`θ" for x
proof -
fix x
assume "x∈β"
with ‹∀x∈h `` β. x ∈ α_0› ‹Ord(α_0)› ‹h:β→γ›
have "h`x < α_0"
using fun_is_function[of h β "λ_. γ"]
Image_subset_Ord_imp_lt domain_of_fun[of h β "λ_. γ"]
by blast
also from ‹⟨α_0 ∪ _, f ` θ⟩ ∈ Memrel(γ) ∨ α_0 ∪ _= f ` θ›
‹Ord(f`θ)› ‹Ord(α_0)› ‹Ord(j`β)›
have "α_0 ≤ f`θ"
using Un_leD1[OF leI [OF ltI]] Un_leD1[OF le_eqI] by blast
finally
show "h`x < f`θ" .
qed
ultimately
have "factor_body(β,λx∈β. factor(x),θ)"
unfolding h_def factor_body_def using ltD
by (auto dest:Un_memD2 Un_leD2[OF le_eqI])
with ‹Ord(θ)›
have "factor(β) ≤ θ"
using factor_unfold[of β] Least_le unfolding factor_rec_def by auto
with ‹θ∈δ› ‹Ord(δ)›
have "factor(β) ∈ δ"
using leI[of θ] ltI[of θ] by (auto dest:ltD)
then
show ?case by (auto elim:mem_irrefl)
qed
moreover
have "cofinal_fun(f O fun_factor, γ, Memrel(γ))"
proof (intro cofinal_funI)
fix a
assume "a ∈ γ"
with ‹cf_fun(j,γ)› ‹domain(j) = cf(γ)›
obtain x where "x∈cf(γ)" "a ∈ j`x ∨ a = j`x"
by (auto simp add:cofinal_fun_def) blast
with factor_not_delta
have "x ∈ domain(f O fun_factor)"
using f_fun_factor_is_mono_map mono_map_is_fun domain_of_fun by force
moreover
have "a ∈ (f O fun_factor) `x ∨ a = (f O fun_factor) `x"
proof -
from ‹x∈cf(γ)› factor_not_delta
have "j ` x ≤ f ` factor(x)"
using mem_not_refl factor_body_factor factor_in_delta
unfolding factor_body_def by auto
with ‹a ∈ j`x ∨ a = j`x›
have "a ∈ f ` factor(x) ∨ a = f ` factor(x)"
using ltD by blast
with ‹x∈cf(γ)›
show ?thesis using lam_funtype[of "cf(γ)" factor]
unfolding fun_factor_def by auto
qed
moreover
note ‹a ∈ γ›
moreover from calculation and ‹Ord(γ)› and factor_not_delta
have "(f O fun_factor) `x ∈ γ"
using Limit_nonzero apply_in_codomain_Ord mono_map_is_fun[of "f O fun_factor"]
f_fun_factor_is_mono_map by blast
ultimately
show "∃x ∈ domain(f O fun_factor). ⟨a, (f O fun_factor) ` x⟩ ∈ Memrel(γ)
∨ a = (f O fun_factor) `x"
by blast
qed
ultimately
show ?thesis
using fun_factor_is_mono_map f_fun_factor_is_mono_map by blast
qed
text‹As a final observation in this part, we note that if the original
cofinal map was increasing, then the factor function is also cofinal.›
lemma factor_is_cofinal:
assumes
"Ord(δ)" "Ord(γ)"
"f :δ →⇩< γ" "f O g ∈ mono_map(α,r,γ,Memrel(γ))"
"cofinal_fun(f O g,γ,Memrel(γ))" "g: α → δ"
shows
"cf_fun(g,δ)"
unfolding cf_fun_def cofinal_fun_def
proof
fix a
assume "a ∈ δ"
with ‹f ∈ mono_map(δ,_,γ,_)›
have "f`a ∈ γ"
using mono_map_is_fun by force
with ‹cofinal_fun(f O g,γ,_)›
obtain y where "y∈α" "⟨f`a, (f O g) ` y⟩ ∈ Memrel(γ) ∨ f`a = (f O g) ` y"
unfolding cofinal_fun_def using domain_of_fun[OF ‹g:α → δ›] by blast
with ‹g:α → δ›
have "⟨f`a, f ` (g ` y)⟩ ∈ Memrel(γ) ∨ f`a = f ` (g ` y)" "g`y ∈ δ"
using comp_fun_apply[of g α δ y f] by auto
with assms(1-3) and ‹a∈δ›
have "⟨a, g ` y⟩ ∈ Memrel(δ) ∨ a = g ` y"
using Memrel_mono_map_reflects Memrel_mono_map_is_inj[of δ f γ γ]
inj_apply_equality[of f δ γ] by blast
with ‹y∈α›
show "∃x∈domain(g). ⟨a, g ` x⟩ ∈ Memrel(δ) ∨ a = g ` x"
using domain_of_fun[OF ‹g:α → δ›] by blast
qed
subsection‹Classical results on cofinalities›
text‹Now the rest of the results follow in a more algebraic way. The
next proof one invokes a case analysis on whether the argument is zero,
a successor ordinal or a limit one; the last case being the most
relevant one and is immediate from the factorization lemma.›
lemma cf_le_domain_cofinal_fun:
assumes
"Ord(γ)" "Ord(δ)" "f:δ → γ" "cf_fun(f,γ)"
shows
"cf(γ)≤δ"
using assms
proof (cases rule:Ord_cases)
case 0
with ‹Ord(δ)›
show ?thesis using Ord_0_le by simp
next
case (succ γ)
with assms
obtain x where "x∈δ" "f`x=γ" using cf_fun_succ' by blast
then
have "δ≠0" by blast
let ?f="{⟨0,f`x⟩}"
from ‹f`x=γ›
have "?f:1→succ(γ)"
using singleton_0 singleton_fun[of 0 γ] singleton_subsetI fun_weaken_type by simp
with ‹Ord(γ)› ‹f`x=γ›
have "cf(succ(γ)) = 1" using cf_succ by simp
with ‹δ≠0› succ
show ?thesis using Ord_0_lt_iff succ_leI ‹Ord(δ)› by simp
next
case (limit)
with assms
obtain g where "g :cf(γ) →⇩< δ"
using cofinal_fun_factorization by blast
with assms
show ?thesis using mono_map_imp_le by simp
qed
lemma cf_ordertype_cofinal:
assumes
"Limit(γ)" "A⊆γ" "cofinal(A,γ,Memrel(γ))"
shows
"cf(γ) = cf(ordertype(A,Memrel(γ)))"
proof (intro le_anti_sym)
text‹We show the result by proving the two inequalities.›
from ‹Limit(γ)›
have "Ord(γ)"
using Limit_is_Ord by simp
with ‹A ⊆ γ›
have "well_ord(A,Memrel(γ))"
using well_ord_Memrel well_ord_subset by blast
then
obtain f α where "f:⟨α, Memrel(α)⟩ ≅ ⟨A,Memrel(γ)⟩" "Ord(α)" "α = ordertype(A,Memrel(γ))"
using ordertype_ord_iso Ord_ordertype ord_iso_sym by blast
moreover from this
have "f: α → A"
using ord_iso_is_mono_map mono_map_is_fun[of f _ "Memrel(α)"] by blast
moreover from this
have "function(f)"
using fun_is_function by simp
moreover from ‹f:⟨α, Memrel(α)⟩ ≅ ⟨A,Memrel(γ)⟩›
have "range(f) = A"
using ord_iso_is_bij bij_is_surj surj_range by blast
moreover note ‹cofinal(A,γ,_)›
ultimately
have "cf_fun(f,γ)"
using cofinal_range_iff_cofinal_fun by blast
moreover from ‹Ord(α)›
obtain h where "h :cf(α) →⇩< α" "cf_fun(h,α)"
using cofinal_mono_map_cf by blast
moreover from ‹Ord(γ)›
have "trans(Memrel(γ))"
using trans_Memrel by simp
moreover
note ‹A⊆γ›
ultimately
have "cofinal_fun(f O h,γ,Memrel(γ))"
using cofinal_comp ord_iso_is_mono_map[OF ‹f:⟨α,_⟩ ≅ ⟨A,_⟩›] mono_map_is_fun
mono_map_mono by blast
moreover from ‹f:α→A› ‹A⊆γ› ‹h∈mono_map(cf(α),_,α,_)›
have "f O h : cf(α) → γ"
using Pi_mono[of A γ] comp_fun mono_map_is_fun by blast
moreover
note ‹Ord(γ)› ‹Ord(α)› ‹α = ordertype(A,Memrel(γ))›
ultimately
show "cf(γ) ≤ cf(ordertype(A,Memrel(γ)))"
using cf_le_domain_cofinal_fun[of _ _ "f O h"]
by (auto simp add:cf_fun_def)
text‹That finishes the first inequality. Now we go the other side.›
from ‹f:⟨α, _⟩ ≅ ⟨A,_⟩› ‹A⊆γ›
have "f :α →⇩< γ"
using mono_map_mono[OF ord_iso_is_mono_map] by simp
then
have "f: α → γ"
using mono_map_is_fun by simp
with ‹cf_fun(f,γ)› ‹Limit(γ)› ‹Ord(α)›
obtain g where "g :cf(γ) →⇩< α"
"f O g :cf(γ) →⇩< γ"
"cofinal_fun(f O g,γ,Memrel(γ))"
using cofinal_fun_factorization by blast
moreover from this
have "g:cf(γ)→α"
using mono_map_is_fun by simp
moreover
note ‹Ord(α)›
moreover from calculation and ‹f :α →⇩< γ› ‹Ord(γ)›
have "cf_fun(g,α)"
using factor_is_cofinal by blast
moreover
note ‹α = ordertype(A,Memrel(γ))›
ultimately
show "cf(ordertype(A,Memrel(γ))) ≤ cf(γ)"
using cf_le_domain_cofinal_fun[OF _ Ord_cf mono_map_is_fun] by simp
qed
lemma cf_idemp:
assumes "Limit(γ)"
shows "cf(γ) = cf(cf(γ))"
proof -
from assms
obtain A where "A⊆γ" "cofinal(A,γ,Memrel(γ))" "cf(γ) = ordertype(A,Memrel(γ))"
using Limit_is_Ord cf_is_ordertype by blast
with assms
have "cf(γ) = cf(ordertype(A,Memrel(γ)))" using cf_ordertype_cofinal by simp
also
have "... = cf(cf(γ))"
using ‹cf(γ) = ordertype(A,Memrel(γ))› by simp
finally
show "cf(γ) = cf(cf(γ))" .
qed
lemma cf_le_cardinal:
assumes "Limit(γ)"
shows "cf(γ) ≤ |γ|"
proof -
from assms
have ‹Ord(γ)› using Limit_is_Ord by simp
then
obtain f where "f ∈ surj(|γ|,γ)"
using Ord_cardinal_eqpoll unfolding eqpoll_def bij_def by blast
with ‹Ord(γ)›
show ?thesis
using Card_is_Ord[OF Card_cardinal] surj_is_cofinal
cf_le_domain_cofinal_fun[of γ] surj_is_fun by blast
qed
lemma regular_is_Card:
notes le_imp_subset [dest]
assumes "Limit(γ)" "γ = cf(γ)"
shows "Card(γ)"
proof -
from assms
have "|γ| ⊆ γ"
using Limit_is_Ord Ord_cardinal_le by blast
also from ‹γ = cf(γ)›
have "γ ⊆ cf(γ)" by simp
finally
have "|γ| ⊆ cf(γ)" .
with assms
show ?thesis unfolding Card_def using cf_le_cardinal by force
qed
lemma Limit_cf: assumes "Limit(κ)" shows "Limit(cf(κ))"
using Ord_cf[of κ, THEN Ord_cases]
proof (cases)
case 1
with ‹Limit(κ)›
show ?thesis using cf_zero_iff Limit_is_Ord by simp
next
case (2 α)
moreover
note ‹Limit(κ)›
moreover from calculation
have "cf(κ) = 1"
using cf_idemp cf_succ by fastforce
ultimately
show ?thesis
using succ_LimitE cf_eq_one_iff Limit_is_Ord
by auto
qed
lemma InfCard_cf: "Limit(κ) ⟹ InfCard(cf(κ))"
using regular_is_Card cf_idemp Limit_cf nat_le_Limit Limit_cf
unfolding InfCard_def by simp
lemma cf_le_cf_fun:
notes [dest] = Limit_is_Ord
assumes "cf(κ) ≤ ν" "Limit(κ)"
shows "∃f. f:ν → κ ∧ cf_fun(f, κ)"
proof -
note assms
moreover from this
obtain h where h_cofinal_mono: "cf_fun(h,κ)"
"h :cf(κ) →⇩< κ"
"h : cf(κ) → κ"
using cofinal_mono_map_cf mono_map_is_fun by force
moreover from calculation
obtain g where "g ∈ inj(cf(κ), ν)"
using le_imp_lepoll by blast
from this and calculation(2,3,5)
obtain f where "f ∈ surj(ν, cf(κ))" "f: ν → cf(κ)"
using inj_imp_surj[OF _ Limit_has_0[THEN ltD]]
surj_is_fun Limit_cf by blast
moreover from this
have "cf_fun(f,cf(κ))"
using surj_is_cofinal by simp
moreover
note h_cofinal_mono ‹Limit(κ)›
moreover from calculation
have "cf_fun(h O f,κ)"
using cf_fun_comp by blast
moreover from calculation
have "h O f ∈ ν -> κ"
using comp_fun by simp
ultimately
show ?thesis by blast
qed
lemma Limit_cofinal_fun_lt:
notes [dest] = Limit_is_Ord
assumes "Limit(κ)" "f: ν → κ" "cf_fun(f,κ)" "n∈κ"
shows "∃α∈ν. n < f`α"
proof -
from ‹Limit(κ)› ‹n∈κ›
have "succ(n) ∈ κ"
using Limit_has_succ[OF _ ltI, THEN ltD] by auto
moreover
note ‹f: ν → _›
moreover from this
have "domain(f) = ν"
using domain_of_fun by simp
moreover
note ‹cf_fun(f,κ)›
ultimately
obtain α where "α ∈ ν" "succ(n) ∈ f`α ∨ succ(n) = f `α"
using cf_funD[THEN cofinal_funD] by blast
moreover from this
consider (1) "succ(n) ∈ f`α" | (2) "succ(n) = f `α"
by blast
then
have "n < f`α"
proof (cases)
case 1
moreover
have "n ∈ succ(n)" by simp
moreover
note ‹Limit(κ)› ‹f: ν → _› ‹α ∈ ν›
moreover from this
have "Ord(f ` α)"
using apply_type[of f ν "λ_. κ", THEN [2] Ord_in_Ord]
by blast
ultimately
show ?thesis
using Ord_trans[of n "succ(n)" "f ` α"] ltI by blast
next
case 2
have "n ∈ f ` α" by (simp add:2[symmetric])
with ‹Limit(κ)› ‹f: ν → _› ‹α ∈ ν›
show ?thesis
using ltI
apply_type[of f ν "λ_. κ", THEN [2] Ord_in_Ord]
by blast
qed
ultimately
show ?thesis by blast
qed
context
includes Ord_dests and Aleph_dests and Aleph_intros and Aleph_mem_dests and mono_map_rules
begin
text‹We end this section by calculating the cofinality of Alephs, for
the zero and limit case. The successor case depends on $\AC$.›
lemma cf_nat: "cf(ω) = ω"
using Limit_nat[THEN InfCard_cf] cf_le_cardinal[of ω]
Card_nat[THEN Card_cardinal_eq] le_anti_sym
unfolding InfCard_def by auto
lemma cf_Aleph_zero: "cf(ℵ⇘0⇙) = ℵ⇘0⇙"
using cf_nat unfolding Aleph_def by simp
lemma cf_Aleph_Limit:
assumes "Limit(γ)"
shows "cf(ℵ⇘γ⇙) = cf(γ)"
proof -
note ‹Limit(γ)›
moreover from this
have "(λx∈γ. ℵ⇘x⇙) : γ → ℵ⇘γ⇙" (is "?f : _ → _")
using lam_funtype[of _ Aleph] fun_weaken_type[of _ _ _ "ℵ⇘γ⇙"] by blast
moreover from ‹Limit(γ)›
have "x ∈ y ⟹ ℵ⇘x⇙ ∈ ℵ⇘y⇙" if "x ∈ γ" "y ∈ γ" for x y
using that Ord_in_Ord[of γ] Ord_trans[of _ _ γ] by blast
ultimately
have "?f ∈ mono_map(γ,Memrel(γ),ℵ⇘γ⇙, Memrel(ℵ⇘γ⇙))"
by auto
with ‹Limit(γ)›
have "?f ∈ ⟨γ, Memrel(γ)⟩ ≅ ⟨?f``γ, Memrel(ℵ⇘γ⇙)⟩"
using mono_map_imp_ord_iso_Memrel[of γ "ℵ⇘γ⇙" ?f]
Card_Aleph
by blast
then
have "converse(?f) ∈ ⟨?f``γ, Memrel(ℵ⇘γ⇙)⟩ ≅ ⟨γ, Memrel(γ)⟩"
using ord_iso_sym by simp
with ‹Limit(γ)›
have "ordertype(?f``γ, Memrel(ℵ⇘γ⇙)) = γ"
using ordertype_eq[OF _ well_ord_Memrel]
ordertype_Memrel by auto
moreover from ‹Limit(γ)›
have "cofinal(?f``γ, ℵ⇘γ⇙, Memrel(ℵ⇘γ⇙))"
unfolding cofinal_def
proof (standard, intro ballI)
fix a
assume "a∈ℵ⇘γ⇙" "ℵ⇘γ⇙ = (⋃i<γ. ℵ⇘i⇙)"
moreover from this
obtain i where "i<γ" "a∈ℵ⇘i⇙"
by auto
moreover from this and ‹Limit(γ)›
have "Ord(i)" using ltD Ord_in_Ord by blast
moreover from ‹Limit(γ)› and calculation
have "succ(i) ∈ γ" using ltD by auto
moreover from this and ‹Ord(i)›
have "ℵ⇘i⇙ < ℵ⇘succ(i)⇙"
by (auto)
ultimately
have "⟨a,ℵ⇘i⇙⟩ ∈ Memrel(ℵ⇘γ⇙)"
using ltD by (auto dest:Aleph_increasing)
moreover from ‹i<γ›
have "ℵ⇘i⇙ ∈ ?f``γ"
using ltD apply_in_image[OF ‹?f : _ → _›] by auto
ultimately
show "∃x∈?f `` γ. ⟨a, x⟩ ∈ Memrel(ℵ⇘γ⇙) ∨ a = x" by blast
qed
moreover
note ‹?f: γ → ℵ⇘γ⇙› ‹Limit(γ)›
ultimately
show "cf(ℵ⇘γ⇙) = cf(γ)"
using cf_ordertype_cofinal[OF Limit_Aleph Image_sub_codomain, of γ ?f γ γ ]
Limit_is_Ord by simp
qed
end
end