Theory Kappa_Closed_Notions

section‹Preservation results for $\kappa$-closed forcing notions›

theory Kappa_Closed_Notions
  imports
    Not_CH
begin

definition
  lerel :: "ii" where
  "lerel(α)  Memrel(α)  id(α)"

lemma lerelI[intro!]: "xy  yα  Ord(α)  x,y  lerel(α)"
  using Ord_trans[of x y α] ltD unfolding lerel_def by auto

lemma lerelD[dest]: "x,y  lerel(α)  Ord(α)  xy"
  using ltI[THEN leI] Ord_in_Ord unfolding lerel_def by auto

definition
  mono_seqspace :: "[i,i,i]  i" (‹_ < '(_,_') [61] 60) where
  "α < (P,leq)  mono_map(α,Memrel(α),P,leq)"

relativize functional "mono_seqspace" "mono_seqspace_rel"
relationalize "mono_seqspace_rel" "is_mono_seqspace"
synthesize "is_mono_seqspace" from_definition assuming "nonempty"

context M_ZF_library
begin

rel_closed for "mono_seqspace"
  unfolding mono_seqspace_rel_def mono_map_rel_def
  using separation_closed separation_ball separation_imp separation_in
    lam_replacement_fst lam_replacement_snd lam_replacement_hcomp lam_replacement_constant
    lam_replacement_product
    lam_replacement_apply2[THEN[5] lam_replacement_hcomp2]
  by simp_all

end ― ‹localeM_ZF_library

abbreviation
  mono_seqspace_r (‹_ <→⇗_ '(_,_') [61] 60) where
  "α <→⇗M(P,leq)  mono_seqspace_rel(M,α,P,leq)"

abbreviation
  mono_seqspace_r_set (‹_ <→⇗_ '(_,_') [61] 60) where
  "α <→⇗M(P,leq)  mono_seqspace_rel(##M,α,P,leq)"

lemma mono_seqspaceI[intro!]:
  includes mono_map_rules
  assumes "f: AP" "x y. xA  yA  x<y  f`x, f`y  leq" "Ord(A)"
  shows  "f: A < (P,leq)"
  using ltI[OF _ Ord_in_Ord[of A], THEN [3] assms(2)] assms(1,3)
  unfolding mono_seqspace_def by auto

lemma (in M_ZF_library) mono_seqspace_rel_char:
  assumes "M(A)" "M(P)" "M(leq)"
  shows "A <→⇗M(P,leq) = {fA < (P,leq). M(f)}"
  using assms mono_map_rel_char
  unfolding mono_seqspace_def mono_seqspace_rel_def by simp

lemma (in M_ZF_library) mono_seqspace_relI[intro!]:
  assumes "f: A→⇗MP" "x y. xA  yA  x<y  f`x, f`y  leq"
    "Ord(A)" "M(A)" "M(P)" "M(leq)"
  shows  "f: A <→⇗M(P,leq)"
  using mono_seqspace_rel_char function_space_rel_char assms by auto

lemma mono_seqspace_is_fun[dest]:
  includes mono_map_rules
  shows "j: A < (P,leq)  j: A P"
  unfolding mono_seqspace_def by auto

lemma mono_map_lt_le_is_mono[dest]:
  includes mono_map_rules
  assumes "j: A < (P,leq)" "aA" "cA" "ac" "Ord(A)" "refl(P,leq)"
  shows "j`a,j`c  leq"
  using assms mono_map_increasing unfolding mono_seqspace_def refl_def
  by (cases "a=c") (auto dest:ltD)

lemma (in M_ZF_library) mem_mono_seqspace_abs[absolut]:
  assumes "M(f)" "M(A)" "M(P)" "M(leq)"
  shows  "f:A <→⇗M(P,leq)   f: A < (P,leq)"
  using assms mono_map_rel_char unfolding mono_seqspace_def mono_seqspace_rel_def
  by (simp)

definition
  mono_map_lt_le :: "[i,i]  i" (infixr < 60) where
  "α < β  α < (β,lerel(β))"

lemma mono_map_lt_leI[intro!]:
  includes mono_map_rules
  assumes "f: AB" "x y. xA  yA  x<y  f`x  f`y" "Ord(A)" "Ord(B)"
  shows  "f: A < B"
  using assms
  unfolding mono_map_lt_le_def by auto

― ‹Kunen IV.7.13, with ``$\kappa$'' in place of ``$\lambda$''›
definition
  kappa_closed :: "[i,i,i]  o" (‹_-closed'(_,_')) where
  "κ-closed(P,leq)  δ. δ<κ  (fδ < (P,converse(leq)). qP. αδ. q,f`αleq)"

relativize functional "kappa_closed" "kappa_closed_rel"
relationalize "kappa_closed_rel" "is_kappa_closed"
synthesize "is_kappa_closed" from_definition assuming "nonempty"

abbreviation
  kappa_closed_r (‹_-closed⇗_⇖'(_,_') [61] 60) where
  "κ-closed⇗M⇖(P,leq)  kappa_closed_rel(M,κ,P,leq)"

abbreviation
  kappa_closed_r_set (‹_-closed⇗_⇖'(_,_') [61] 60) where
  "κ-closed⇗M⇖(P,leq)  kappa_closed_rel(##M,κ,P,leq)"

lemma (in forcing_data3) forcing_a_value:
  assumes "p  0:12 [f_dot, Av, Bv]" "a  A"
    "q  p" "q  " "p" "f_dot  M" "AM" "BM"
  shows "d. bB. d  q  d  0`1 is 2 [f_dot, av, bv]"
    (* ― ‹Old neater version, but harder to use
    (without the assumptions on term‹q›):›
    "dense_below({q ∈ ℙ. ∃b∈B. q ⊩ ⋅0`1 is 2⋅ [f_dot, av, bv]}, p)" *)
proof -
  from assms
  have "q  0:12 [f_dot, Av, Bv]"
    using strengthening_lemma[of p "0:12" q "[f_dot, Av, Bv]"]
      typed_function_type arity_typed_function_fm
    by (auto simp: union_abs2 union_abs1)
  from aA AM
  have "aM" by (auto dest:transitivity)
  from q
  text‹Here we're using countability (via the existence of generic filters)
    of termM as a shortcut, to avoid a further density argument.›
  obtain G where "M_generic(G)" "qG"
    using generic_filter_existence by blast
  then
  interpret G_generic3_AC _ _ _ _ _ G by unfold_locales
  include G_generic1_lemmas
  note qG
  moreover
  note q  0:12 [f_dot, Av, Bv] M_generic(G)
  moreover
  note q f_dotM BM AM
  moreover from this
  have "map(val( G), [f_dot, Av, Bv])  list(M[G])" by simp
  moreover from calculation
  have "val(G,f_dot) : A →⇗M[G]B"
    using truth_lemma[of "0:12" "[f_dot, Av, Bv]", THEN iffD1]
      typed_function_type arity_typed_function_fm val_check[OF one_in_G one_in_P]
    by (auto simp: union_abs2 union_abs1 ext.mem_function_space_rel_abs)
  moreover
  note a  M
  moreover from calculation and aA
  have "val(G,f_dot) ` a  B" (is "?b  B")
    by (simp add: ext.mem_function_space_rel_abs)
  moreover from calculation
  have "?b  M" by (auto dest:transitivity)
  moreover from calculation
  have "M[G], map(val(G), [f_dot, av, ?bv])  0`1 is 2"
    by simp
  ultimately
  obtain r where "r  0`1 is 2 [f_dot, av, ?bv]" "rG" "r"
    using truth_lemma[of "0`1 is 2" "[f_dot, av, ?bv]", THEN iffD2]
      fun_apply_type arity_fun_apply_fm val_check[OF one_in_G one_in_P]
      G_subset_P
    by (auto simp: union_abs2 union_abs1 ext.mem_function_space_rel_abs)
  moreover from this and qG
  obtain d where "dq" "dr" "d" by force
  moreover
  note f_dotM aM ?bB BM
  moreover from calculation
  have "d  q  d  0`1 is 2 [f_dot, av, ?bv]"
    using fun_apply_type arity_fun_apply_fm
      strengthening_lemma[of r "0`1 is 2" d "[f_dot, av, ?bv]"]
    by (auto dest:transitivity simp add: union_abs2 union_abs1)
  ultimately
  show ?thesis by auto
qed

locale M_master_CH = M_master + M_library_DC

sublocale M_ZFC2_ground_CH_trans  M_master_CH "##M"
  using replacement_dcwit_repl_body
  by unfold_locales (simp_all add:sep_instances del:setclass_iff
      add: transrec_replacement_def wfrec_replacement_def dcwit_repl_body_def)

context G_generic3_AC_CH begin

context
  includes G_generic1_lemmas
begin

lemma separation_check_snd_aux:
  assumes "f_dotM" "τM" "χformula" "arity(χ)  7"
  shows "separation(##M, λr. M, [fst(r), , leq, 𝟭, f_dot, τ, snd(r)v]  χ)"
proof -
  let ?f_fm="fst_fm(1,0)"
  let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
  note assms
  moreover
  have "?f_fm  formula" "arity(?f_fm)  7" "?g_fm  formula" "arity(?g_fm)  8"
    using ord_simp_union
    unfolding hcomp_fm_def
    by (simp_all add:arity)
  ultimately
  show ?thesis
    using separation_sat_after_function
    using fst_abs snd_abs sats_snd_fm sats_check_fm check_abs
    unfolding hcomp_fm_def
    by simp
qed

lemma separation_check_fst_snd_aux :
  assumes "f_dotM" "rM" "χformula" "arity(χ)  7"
  shows "separation(##M, λp. M, [r, , leq, 𝟭, f_dot, fst(p)v, snd(p)v]  χ)"
proof -
  let ="λz. [r, , leq, 𝟭, f_dot, fst(z)v, snd(z)v]"
  let ?ρ'="λz. [fst(z)v, , leq, 𝟭, f_dot, r, snd(z)v]"
  let =" (⋅∃(⋅∃(⋅∃(⋅∃(⋅∃(⋅∃0 = 11  1 = 7  2 = 8  3 = 9  4 = 10  5 = 6 
    (λp. incr_bv(p)`6)^6 (χ) ⋅)⋅)⋅)⋅)⋅)⋅)"
  let ?f_fm="hcomp_fm(check_fm(5),fst_fm,1,0)"
  let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
  note assms
  moreover
  have "?f_fm  formula" "arity(?f_fm)  7" "?g_fm  formula" "arity(?g_fm)  8"
    using ord_simp_union
    unfolding hcomp_fm_def
    by (simp_all add:arity)
  moreover from assms
  have fm:"formula" by simp
  moreover from χ  formula arity(χ)  7
  have "arity(χ) = 0  arity(χ) = 1  arity(χ) = 2  arity(χ) = 3
     arity(χ) = 4  arity(χ) = 5  arity(χ) = 6  arity(χ) = 7"
    unfolding lt_def by auto
  with calculation and χ  formula
  have ar:"arity()  7"
    using arity_incr_bv_lemma by safe (simp_all add: arity ord_simp_union)
  moreover from calculation
  have sep:"separation(##M,λz. M,?ρ'(z))"
    using separation_sat_after_function sats_check_fm check_abs
      fst_abs snd_abs
    unfolding hcomp_fm_def
    by simp
  moreover from assms
  have "(z)  list(M)" if "(##M)(z)" for z
    using that by simp
  moreover from calculation and r  M χ  formula
  have "(M,(z)  χ)  (M,?ρ'(z))" if "(##M)(z)" for z
    using that sats_incr_bv_iff[of _ _ M _ "[_,_,_,_,_,_]"]
    by simp
  ultimately
  show ?thesis
    using separation_cong[THEN iffD1,OF _ sep]
    by simp
qed

lemma separation_leq_and_forces_apply_aux:
  assumes "f_dotM" "BM"
  shows "nM. separation(##M, λx. snd(x)  fst(x) 
          (bB. M, [snd(x), , leq, 𝟭, f_dot, ((n))v, bv]  forces(0`1 is 2 )))"
proof -
  have pred_nat_closed: "pred(n)M" if "nM" for n
    using nat_case_closed that
    unfolding pred_def
    by auto
  have "separation(##M, λz. M, [snd(fst(z)), , leq, 𝟭, f_dot, τ, snd(z)v]  χ)"
    if "χformula" "arity(χ)  7" "τM" for χ τ
  proof -
    let ?f_fm="hcomp_fm(snd_fm,fst_fm,1,0)"
    let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
    note assms
    moreover
    have "?f_fm  formula" "arity(?f_fm)  7" "?g_fm  formula" "arity(?g_fm)  8"
      using ord_simp_union
      unfolding hcomp_fm_def
      by (simp_all add:arity)
    ultimately
    show ?thesis
      using separation_sat_after_function sats_check_fm check_abs fst_abs snd_abs that
      unfolding hcomp_fm_def
      by simp
  qed
  with assms
  show ?thesis
    using separation_in lam_replacement_constant lam_replacement_snd lam_replacement_fst
      lam_replacement_product pred_nat_closed
      arity_forces[of " 0`1 is 2"] arity_fun_apply_fm[of 0 1 2] ord_simp_union
    by(clarify,rule_tac separation_conj,simp_all,rule_tac separation_bex,simp_all)
qed

lemma separation_leq_and_forces_apply_aux':
  assumes "f_dotM" "pM" "BM"
  shows "separation
     (##M, λp .  snd(snd(p))  fst(snd(p)) 
    (bB. M, [snd(snd(p)), , leq, 𝟭, f_dot, (fst(p))v, bv]  forces(0`1 is 2 )))"
proof -
  have "separation(##M, λz. M, [snd(snd(fst(z))), , leq, 𝟭, f_dot, (fst(fst(z)))v, snd(z)v]  χ)"
    if "χformula" "arity(χ)  7" for χ
  proof -
    let ?f_fm="hcomp_fm(snd_fm,hcomp_fm(snd_fm,fst_fm),1,0)"
    let ?g="λz . ((fst(fst(z))))v"
    let ?g_fm="hcomp_fm(check_fm(6),hcomp_fm(big_union_fm,hcomp_fm(fst_fm,fst_fm)),2,0)"
    let ?h_fm="hcomp_fm(check_fm(7),snd_fm,3,0)"
    note assms
    moreover
    have f_fm_facts:"?f_fm  formula" "arity(?f_fm)  6"
      using ord_simp_union
      unfolding hcomp_fm_def
      by (simp_all add:arity)
    moreover from assms
    have "?g_fm  formula" "arity(?g_fm)  7" "?h_fm  formula" "arity(?h_fm)  8"
      using ord_simp_union
      unfolding hcomp_fm_def
      by (simp_all add:arity)
    ultimately
    show ?thesis
      using separation_sat_after_function3[OF _ _ _ f_fm_facts] check_abs
        sats_check_fm that fst_abs snd_abs sats_fst_fm sats_snd_fm
      unfolding hcomp_fm_def
      by simp
  qed
  with assms
  show ?thesis
    using
      separation_conj separation_bex
      lam_replacement_constant lam_replacement_hcomp
      lam_replacement_fst lam_replacement_snd
      arity_forces[of " 0`1 is 2"] arity_fun_apply_fm[of 0 1 2] ord_simp_union
      separation_in[OF _ lam_replacement_product]
    by simp
qed

lemma separation_closed_leq_and_forces_eq_check_aux :
  assumes "AM" "rG" "τ  M"
  shows "(##M)({q. hA. q  r  q  0 = 1 [τ, hv]})"
proof -
  have "separation(##M, λz. M, [fst(z), , leq, 𝟭, τ, snd(z)v]  χ)" if
    "χformula" "arity(χ)  6" for χ
  proof -
    let ?f_fm="fst_fm(1,0)"
    let ?g_fm="hcomp_fm(check_fm(6),snd_fm,2,0)"
    note assms
    moreover
    have "?f_fm  formula" "arity(?f_fm)  6" "?g_fm  formula" "arity(?g_fm)  7"
      using ord_simp_union
      unfolding hcomp_fm_def
      by (simp_all add:arity)
    ultimately
    show ?thesis
      using separation_sat_after_function_1 sats_fst_fm that
        fst_abs snd_abs sats_snd_fm sats_check_fm check_abs
      unfolding hcomp_fm_def
      by simp
  qed
  with assms
  show ?thesis
    using separation_conj separation_in G_subset_M[THEN subsetD]
      lam_replacement_constant lam_replacement_fst lam_replacement_product
      arity_forces[of "0 = 1",simplified] ord_simp_union
    by(rule_tac separation_closed[OF separation_bex],simp_all)
qed

lemma separation_closed_forces_apply_aux:
  assumes "BM" "f_dotM" "rM"
  shows "(##M)({n,b  ω × B. r  0`1 is 2 [f_dot, nv, bv]})"
  using nat_in_M assms transitivity[OF _ BM] nat_into_M separation_check_fst_snd_aux
    arity_forces[of " 0`1 is 2"] arity_fun_apply_fm[of 0 1 2] ord_simp_union
  unfolding split_def
  by simp_all

― ‹Kunen IV.6.9 (3)$\Rightarrow$(2), with general domain.›
lemma kunen_IV_6_9_function_space_rel_eq:
  assumes "p τ. p  0:12 [τ, Av, Bv]  p  τ  M 
    q. hA →⇗MB. q  p   q  0 = 1 [τ, hv]" "AM" "BM"
  shows
    "A →⇗MB = A →⇗M[G]B"
proof (intro equalityI; clarsimp simp add:
    assms function_space_rel_char ext.function_space_rel_char)
  fix f
  assume "f  A  B" "f  M[G]"
  moreover from this
  obtain τ where "val(G,τ) = f" "τ  M"
    using GenExtD by force
  moreover from calculation and AM BM
  obtain r where "r  0:12 [τ, Av, Bv]" "rG"
    using truth_lemma[of "0:12" "[τ, Av, Bv]"]
      typed_function_type arity_typed_function_fm val_check[OF one_in_G one_in_P]
    by (auto simp: union_abs2 union_abs1)
  moreover from AM BM rG τ  M
  have "{q. hA →⇗MB. q  r  q  0 = 1 [τ, hv]}  M" (is "?D  M")
    using separation_closed_leq_and_forces_eq_check_aux by auto
  moreover from calculation and assms(2-)
  have "dense_below(?D, r)"
    using strengthening_lemma[of r "0:12" _ "[τ, Av, Bv]", THEN assms(1)[of _ τ]]
      leq_transD generic_dests(1)[of r]
    by (auto simp: union_abs2 union_abs1 typed_function_type arity_typed_function_fm) blast
  moreover from calculation
  obtain q h where "hA →⇗MB" "q  0 = 1 [τ, hv]" "q  r" "q" "qG"
    using generic_inter_dense_below[of ?D r] by blast
  note q  0 = 1 [τ, hv] τM hA →⇗MB AM BM qG
  moreover from this
  have "map(val(G), [τ, hv])  list(M[G])" "hM"
    by (auto dest:transitivity)
  ultimately
  have "h = f"
    using truth_lemma[of "0=1" "[τ, hv]"] val_check[OF one_in_G one_in_P]
    by (auto simp: ord_simp_union)
  with hM
  show "f  M" by simp
qed

subsection‹$(\omega+1)$-Closed notions preserve countable sequences›

― ‹Kunen IV.7.15, only for countable sequences›
lemma succ_omega_closed_imp_no_new_nat_sequences:
  assumes "succ(ω)-closed⇗M⇖(,leq)" "f : ω  B" "fM[G]" "BM"
  shows "fM"
proof -
  (* Nice jEdit folding level to read this: 7 *)
  text‹The next long block proves that the assumptions of Lemma
  @{thm [source] kunen_IV_6_9_function_space_rel_eq} are satisfied.›
  {
    fix p f_dot
    assume "p  0:12 [f_dot, ωv, Bv]" "p" "f_dotM"
    let ?subp="{q. q  p}"
    from p
    have "?subp  M"
      using first_section_closed[of  p "converse(leq)"]
      by (auto dest:transitivity)
    define S where "S  λnnat.
    {q,r  ?subp×?subp. r  q  (bB. r  0`1 is 2 [f_dot, ((n))v, bv])}"
      (is "S  λnnat. ?Y(n)")
    define S' where "S'  λnnat.
    {q,r  ?subp×?subp. r  q  (bB. r  0`1 is 2 [f_dot, (pred(n))v, bv])}"
      ― ‹Towards proving termSM.›
    moreover
    have "S = S'"
      unfolding S_def S'_def using pred_nat_eq lam_cong by auto
    moreover from BM ?subpM f_dotM
    have "{r  ?subp. bB. r  0`1 is 2 [f_dot, ((n))v, bv]}  M" (is "?X(n)  M")
      if "nω" for n
      using that separation_check_snd_aux nat_into_M ord_simp_union
        arity_forces[of " 0`1 is 2"] arity_fun_apply_fm
      by(rule_tac separation_closed[OF separation_bex,simplified], simp_all)
    moreover
    have "?Y(n) = (?subp × ?X(n))  converse(leq)" for n
      by (intro equalityI) auto
    moreover
    note ?subp  M BM p f_dotM
    moreover from calculation
    have "n  ω  ?Y(n)  M" for n
      using nat_into_M by simp
    moreover from calculation
    have "S  M"
      using  separation_leq_and_forces_apply_aux separation_leq_and_forces_apply_aux'
        transitivity[OF p]
      unfolding S_def split_def
      by(rule_tac lam_replacement_Collect'[THEN lam_replacement_imp_lam_closed,simplified], simp_all)
    ultimately
    have "S'  M"
      by simp
    from p f_dotM p  0:12 [f_dot, ωv, Bv] BM
    have exr:"r. r  q  (bB. r  0`1 is 2 [f_dot, pred(n)v, bv])"
      if "q  p" "q" "nω" for q n
      using that forcing_a_value by (auto dest:transitivity)
    have "q?subp. nω. r?subp. q,r  S'`n"
    proof -
      {
        fix q n
        assume "q  ?subp" "nω"
        moreover from this
        have "q  p" "q  " "pred(n) = n"
          using pred_nat_eq by simp_all
        moreover from calculation and exr
        obtain r where MM:"r  q" "bB. r  0`1 is 2 [f_dot, pred(n)v, bv]" "r"
          by blast
        moreover from calculation q  p p  
        have "r  p"
          using leq_transD[of r q p] by auto
        ultimately
        have "r?subp. r  q  (bB. r  0`1 is 2 [f_dot, (pred(n))v, bv])"
          by auto
      }
      then
      show ?thesis
        unfolding S'_def by simp
    qed
    with p ?subp  M S'  M
    obtain g where "g  ω →⇗M?subp" "g`0 = p" "n  nat. g`n,g`succ(n)S'`succ(n)"
      using sequence_DC[simplified] refl_leq[of p] by blast
    moreover from this and ?subp  M
    have "g : ω  " "g  M"
      using fun_weaken_type[of g ω ?subp ] function_space_rel_char by auto
    ultimately
    have "g : ω <→⇗M(,converse(leq))"
      using decr_succ_decr[of g] leq_preord
      unfolding S'_def by (auto simp:absolut intro:leI)
    moreover from succ(ω)-closed⇗M⇖(,leq) and this
    have "qM. q    (αM. α  ω  q  g ` α)"
      using transitivity[simplified, of g] mono_seqspace_rel_closed[of ω _ "converse(leq)"]
      unfolding kappa_closed_rel_def
      by auto
    ultimately
    obtain r where "r" "rM" "nω. r  g`n"
      using nat_into_M by auto
    with g`0 = p
    have "r  p"
      by blast
    let ?h="{n,b  ω × B. r  0`1 is 2 [f_dot, nv, bv]}"
    have "function(?h)"
    proof (rule_tac functionI, rule_tac ccontr, auto simp del: app_Cons)
      fix n b b'
      assume "n  ω" "b  b'" "b  B" "b'  B"
      moreover
      assume "r  0`1 is 2 [f_dot, nv, bv]" "r  0`1 is 2 [f_dot, nv, b'v]"
      moreover
      note r  
      moreover from this
      have "¬ r  r"
        by (auto intro!:refl_leq)
      moreover
      note f_dotM BM
      ultimately
      show False
        using forces_neq_apply_imp_incompatible[of r f_dot "nv" b r b']
          transitivity[of _ B] by (auto dest:transitivity)
    qed
    moreover
    have "range(?h)  B"
      by auto
    moreover
    have "domain(?h) = ω"
    proof -
      {
        fix n
        assume "n  ω"
        moreover from this
        have 1:"((n)) = pred(n)"
          using pred_nat_eq by simp
        moreover from calculation and n  nat. g`n,g`succ(n)S'`succ(n)
        obtain b where "g`(succ(n))  0`1 is 2 [f_dot, nv, bv]" "bB"
          unfolding S'_def by auto
        moreover from BM and calculation
        have "b  M" "n  M"
          by (auto dest:transitivity)
        moreover
        note g : ω   nω. r  g`n r f_dotM
        moreover from calculation
        have "r  0`1 is 2 [f_dot, nv, bv]"
          using fun_apply_type arity_fun_apply_fm
            strengthening_lemma[of "g`succ(n)" "0`1 is 2" r "[f_dot, nv, bv]"]
          by (simp add: union_abs2 union_abs1)
        ultimately
        have "bB. r  0`1 is 2 [f_dot, nv, bv]"
          by auto
      }
      then
      show ?thesis
        by force
    qed
    moreover
    have "relation(?h)"
      unfolding relation_def by simp
    moreover from f_dotM rM BM
    have "?h  M"
      using separation_closed_forces_apply_aux by simp
    moreover
    note B  M
    ultimately
    have "?h: ω →⇗MB"
      using function_imp_Pi[THEN fun_weaken_type[of ?h _ "range(?h)" B]]
        function_space_rel_char by simp
    moreover
    note p  0:12 [f_dot, ωv, Bv] r  p r p f_dotM BM
    moreover from this
    have "r  0:12 [f_dot, ωv, Bv]"
      using strengthening_lemma[of p "0:12" r "[f_dot, ωv, Bv]"]
        typed_function_type arity_typed_function_fm
      by (auto simp: union_abs2 union_abs1)
    moreover
    note ?hM
    moreover from calculation
    have "r  0 = 1 [f_dot, ?hv]"
    proof (intro definition_of_forcing[THEN iffD2] allI impI,
        simp_all add:union_abs2 union_abs1 del:app_Cons)
      fix H
      let ?f="val(H,f_dot)"
      assume "M_generic(H)  r  H"
      moreover from this
      interpret g:G_generic1 _ _ _ _ _ H
        by unfold_locales simp
      note r f_dotM BM
      moreover from calculation
      have "map(val(H), [f_dot, ωv, Bv])  list(M[H])" "rH"
        by simp_all
      moreover from calculation and rH and r  0:12 [f_dot, ωv, Bv]
      have "?f : ω  B"
        using g.truth_lemma[of "0:12" "[f_dot, ωv, Bv]",THEN iffD1] g.one_in_G one_in_P
          typed_function_type arity_typed_function_fm val_check
        by (auto simp: union_abs2 union_abs1)
      moreover
      have "?h`n = ?f`n" if "n  ω" for n
      proof -
        note n  ω domain(?h) = ω
        moreover from this
        have "ndomain(?h)"
          by simp
        moreover from this
        obtain b where "r  0`1 is 2 [f_dot, nv, bv]" "bB"
          by force
        moreover
        note function(?h)
        moreover from calculation
        have "b = ?h`n"
          using function_apply_equality by simp
        moreover
        note B  M
        moreover from calculation
        have "?h`n  M"
          by (auto dest:transitivity)
        moreover
        note f_dot  M r   M_generic(H)  r  H map(val(H), [f_dot, ωv, Bv])  list(M[H])
        moreover from calculation
        have "[?f, n, ?h`n]  list(M[H])"
          using M_subset_MG nat_into_M[of n] g.one_in_G by (auto dest:transitivity)
        ultimately
        show ?thesis
          using definition_of_forcing[of r "0`1 is 2" "[f_dot, nv, bv]",
              THEN iffD1, rule_format, of H]― ‹without this line is slower›
            val_check g.one_in_G one_in_P nat_into_M
          by (auto dest:transitivity simp add:fun_apply_type
              arity_fun_apply_fm union_abs2 union_abs1)
      qed
      with calculation and BM ?h: ω →⇗MB
      have "?h = ?f"
        using function_space_rel_char
        by (rule_tac fun_extension[of ?h ω "λ_.B" ?f]) auto
      ultimately
      show "?f = val(H, ?hv)"
        using val_check g.one_in_G one_in_P generic by simp
    qed
    ultimately
    have "r. hω →⇗MB. r  p  r  0 = 1 [f_dot, hv]"
      by blast
  }
  moreover
  note B  M assms
  moreover from calculation
  have "f : ω →⇗MB"
    using kunen_IV_6_9_function_space_rel_eq function_space_rel_char
      ext.mem_function_space_rel_abs by auto
  ultimately
  show ?thesis
    by (auto dest:transitivity)
qed

declare mono_seqspace_rel_closed[rule del]
  ― ‹Mysteriously breaks the end of the next proof›

lemma succ_omega_closed_imp_no_new_reals:
  assumes "succ(ω)-closed⇗M⇖(,leq)"
  shows "ω →⇗M2 = ω →⇗M[G]2"
proof -
  from assms
  have "ω →⇗M[G]2  ω →⇗M2"
    using succ_omega_closed_imp_no_new_nat_sequences function_space_rel_char
      ext.function_space_rel_char Aleph_rel_succ Aleph_rel_zero
    by auto
  then
  show ?thesis
    using function_space_rel_transfer by (intro equalityI) auto
qed

lemma succ_omega_closed_imp_Aleph_1_preserved:
  assumes "succ(ω)-closed⇗M⇖(,leq)"
  shows "ℵ⇘1⇙⇗M= ℵ⇘1⇙⇗M[G]⇖"
proof -
  have "ℵ⇘1⇙⇗M[G] ℵ⇘1⇙⇗M⇖"
  proof (rule ccontr)
    assume "¬ ℵ⇘1⇙⇗M[G] ℵ⇘1⇙⇗M⇖"
    then
    have "ℵ⇘1⇙⇗M< ℵ⇘1⇙⇗M[G]⇖"
      ― ‹Ridiculously complicated proof›
      using Card_rel_is_Ord ext.Card_rel_is_Ord
        not_le_iff_lt[THEN iffD1] by auto
    then
    have "|ℵ⇘1⇙⇗M⇖|⇗M[G] ω"
      using ext.Card_rel_lt_csucc_rel_iff ext.Aleph_rel_zero
        ext.Aleph_rel_succ ext.Card_rel_nat
      by (auto intro!:ext.lt_csucc_rel_iff[THEN iffD1]
          intro:Card_rel_Aleph_rel[THEN Card_rel_is_Ord, of 1])
    then
    obtain f where "f  inj(ℵ⇘1⇙⇗M,ω)" "f  M[G]"
      using ext.countable_rel_iff_cardinal_rel_le_nat[of "ℵ⇘1⇙⇗M⇖", THEN iffD2]
      unfolding countable_rel_def lepoll_rel_def
      by auto
    then
    obtain g where "g  surj⇗M[G]⇖(ω, ℵ⇘1⇙⇗M)"
      using ext.inj_rel_imp_surj_rel[of f _ ω, OF _ zero_lt_Aleph_rel1[THEN ltD]]
      by auto
    moreover from this
    have "g : ω  ℵ⇘1⇙⇗M⇖" "g  M[G]"
      using ext.surj_rel_char surj_is_fun by simp_all
    moreover
    note succ(ω)-closed⇗M⇖(,leq)
    ultimately
    have "g  surj⇗M⇖(ω, ℵ⇘1⇙⇗M)" "g  M"
      using succ_omega_closed_imp_no_new_nat_sequences
        mem_surj_abs ext.mem_surj_abs by simp_all
    then
    show False
      using surj_rel_implies_cardinal_rel_le[of g ω "ℵ⇘1⇙⇗M⇖"]
        Card_rel_nat[THEN Card_rel_cardinal_rel_eq] Card_rel_is_Ord
        not_le_iff_lt[THEN iffD2, OF _ _ nat_lt_Aleph_rel1]
      by simp
  qed
  then
  show ?thesis
    using Aleph_rel_le_Aleph_rel
    by (rule_tac le_anti_sym) simp
qed

end ― ‹bundle G\_generic1\_lemmas›

end ― ‹localeG_generic3_AC

end