Quelle  Not_CH.thy

section‹Model of the negation of the Continuum Hypothesis›

theory Not_CH
  imports
    Cardinal_Preservation
begin

text‹We are taking advantage that the poset of finite functions is absolute,
  thus we work with the unrelativized term‹Fn›. But it would have been more
  to do the following using the relative term‹Fn_rel›. As it turns
 , the present theory was developed prior to having term‹Fn› relativized!

  also note that term‹Fn(ψ,κ×ψ,2)› is separative, i.e. each term‹X ∈ Fn(ψ,κ×ψ,2)›
  two incompatible extensions; therefore we may recover part of our previous theorem
 {thm [source] extensions_of_ctms_ZF}. But that result also included the possibility
  not having $\AC$ in the ground model, which would not be sensible in a context
  the cardinality of the continuum is under discussion. It is also the case that
 {thm [source] extensions_of_ctms_ZF} was historically our first formalized result
 with a different proof) that showed the forcing machinery had all of its elements
  place.›

abbreviation
  Add_subs :: "i ==> i" where
  "Add_subs(κ) ≡ Fn(ψ,κ×ψ,2)"

abbreviation
  Add_le :: "i ==> i" where
  "Add_le(κ) ≡ Fnle(ψ,κ × ψ,2)"

lemma (in M_aleph) Aleph_rel2_closed[intro,simp]: "M(ℵ)"
  using nat_into_Ord by simp

locale M_master = M_cohen + M_library +
  assumes
    UN_lepoll_assumptions:
    "M(A) ==> M(b) ==> M(f) ==> M(A') ==> separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x∈if_range_F_else_F((`)(A), b, f, i)⟩)"

subsection‹Non-absolute concepts between extensions›

sublocale M_master ⊆ M_Pi_replacement
  by unfold_locales

locale M_master_sub = M_master + N:M_aleph N for N +
  assumes
    M_imp_N: "M(x) ==> N(x)" and
    Ord_iff: "Ord(x) ==> M(x) ⟷ N(x)"

sublocale M_master_sub ⊆ M_N_Perm
  using M_imp_N by unfold_locales

context M_master_sub
begin

lemma cardinal_rel_le_cardinal_rel: "M(X) ==> |X| ≤ |X|"
  using M_imp_N N.lepoll_rel_cardinal_rel_le[OF lepoll_rel_transfer Card_rel_is_Ord]
    cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym, THEN eqpoll_rel_imp_lepoll_rel]
  by simp

lemma Aleph_rel_sub_closed: "Ord(α) ==> M(α) ==> N(ℵ_<alpha>)"
  using Ord_iff[THEN iffD1, OF Card_rel_Aleph_rel[THEN Card_rel_is_Ord]]
  by simp

lemma Card_rel_imp_Card_rel: "Card(κ) ==> M(κ) ==> Card(κ)"
  using N.Card_rel_is_Ord[of κ] M_imp_N Ord_cardinal_rel_le[of κ]
    cardinal_rel_le_cardinal_rel[of κ] le_anti_sym
  unfolding Card_rel_def by auto

lemma csucc_rel_le_csucc_rel:
  assumes "Ord(κ)" "M(κ)"
  shows "(κ⁺) ≤ (κ⁺)"
proof -
  note assms
  moreover from this
  have "N(L) ∧ Card(L) ∧ κ < L ==> M(L) ∧ Card(L) ∧ κ < L"
    (is "?P(L) ==> ?Q(L)") for L
    using M_imp_N Ord_iff[THEN iffD2, of L] N.Card_rel_is_Ord lt_Ord
      Card_rel_imp_Card_rel by auto
  moreover from assms
  have "N((κ⁺))" "Card((κ⁺))" "κ < (κ⁺)"
    using N.lt_csucc_rel[of κ] N.Card_rel_csucc_rel[of κ] M_imp_N by simp_all
  ultimately
  show ?thesis
    using M_imp_N Least_antitone[of _ ?P ?Q] unfolding csucc_rel_def by blast
qed

lemma Aleph_rel_le_Aleph_rel: "Ord(α) ==> M(α) ==> ℵ_<alpha> ≤ ℵ_<alpha>"
proof (induct rule:trans_induct3)
  case 0
  then
  show ?case
    using Aleph_rel_zero N.Aleph_rel_zero by simp
next
  case (succ x)
  then
  have "ℵ ≤ ℵ" "Ord(x)" "M(x)" by simp_all
  moreover from this
  have "(ℵ⁺) ≤ (ℵ⁺)"
    using M_imp_N Ord_iff[THEN iffD2, OF N.Card_rel_is_Ord]
    by (intro csucc_rel_le_mono) simp_all
  moreover from calculation
  have "(ℵ⁺) ≤ (ℵ⁺)"
    using M_imp_N N.Card_rel_is_Ord Ord_iff[THEN iffD2, OF N.Card_rel_is_Ord]
    by (intro csucc_rel_le_csucc_rel) auto
  ultimately
  show ?case
    using M_imp_N Aleph_rel_succ N.Aleph_rel_succ csucc_rel_le_csucc_rel
      le_trans by auto
next
  case (limit x)
  then
  show ?case
    using M_imp_N Aleph_rel_limit N.Aleph_rel_limit
    by simp (blast dest: transM intro!:le_implies_UN_le_UN)
qed

end ― ‹🍋‹M_master_sub››

lemmas (in M_ZF2_trans) sep_instances =
  separation_ifrangeF_body separation_ifrangeF_body2 separation_ifrangeF_body3
  separation_ifrangeF_body4 separation_ifrangeF_body5 separation_ifrangeF_body6
  separation_ifrangeF_body7 separation_cardinal_rel_lesspoll_rel
  separation_is_dcwit_body separation_cdltgamma separation_cdeqgamma

lemmas (in M_ZF2_trans) repl_instances = lam_replacement_inj_rel

sublocale M_ZFC2_ground_notCH_trans ⊆ M_master "##M"
  using replacement_trans_apply_image
  by unfold_locales (simp_all add:repl_instances sep_instances del:setclass_iff
      add: transrec_replacement_def wfrec_replacement_def)

sublocale M_ZFC2_trans ⊆ M_Pi_replacement "##M"
  by unfold_locales

subsection‹Cohen forcing is ccc›

context M_ctm2_AC
begin

lemma ccc_Add_subs_Aleph_2: "ccc(Add_subs(ℵ),Add_le(ℵ))"
proof -
  interpret M_add_reals "##M" "ℵ × ψ"
    by unfold_locales blast
  show ?thesis
    using ccc_rel_Fn_nat by fast
qed

end ― ‹🍋‹M_ctm2_AC››

sublocale G_generic3_AC ⊆ M_master_sub "##M" "##(M[G])"
  using M_subset_MG[OF one_in_G] generic Ord_MG_iff
  by unfold_locales auto

lemma (in M_trans) mem_F_bound4:
  fixes F A
  defines "F ≡ (`)"
  shows "x∈F(A,c) ==> c ∈ (range(f) ∪ domain(A))"
  using apply_0 unfolding F_def
  by (cases "M(c)", auto simp:F_def)

lemma (in M_trans) mem_F_bound5:
  fixes F A
  defines "F ≡ λ_ x. A`x "
  shows "x∈F(A,c) ==> c ∈ (range(f) ∪ domain(A))"
  using apply_0 unfolding F_def
  by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)

sublocale M_ctm2_AC ⊆ M_replacement_lepoll "##M" "(`)"
  using UN_lepoll_assumptions lam_replacement_apply lam_replacement_inj_rel
    mem_F_bound4 apply_0 lam_replacement_minimum
  unfolding lepoll_assumptions_defs
proof (unfold_locales,
    rule_tac [3] lam_Least_assumption_general[where U=domain, OF _ mem_F_bound4], simp_all)
  fix A i x
  assume "A ∈ M" "x ∈ M" "x ∈ A ` i"
  then
  show "i ∈ M"
    using apply_0[of i A] transM[of _ "domain(A)", simplified]
    by force
qed

context G_generic3_AC begin

context
  includes G_generic1_lemmas
begin

lemma G_in_MG: "G ∈ M[G]"
  using G_in_Gen_Ext
  by blast

lemma ccc_preserves_Aleph_succ:
  assumes "ccc(ℙ,leq)" "Ord(z)" "z ∈ M"
  shows "Card^[G](ℵ_(z))"
proof (rule ccontr)
  assume "¬ Card^[G](ℵ_(z))"
  moreover
  note ‹z ∈ M› ‹Ord(z)›
  moreover from this
  have "Ord(ℵ_(z))"
    using Card_rel_is_Ord by fastforce
  ultimately
  obtain α f where "α < ℵ_(z)" "f ∈ surj^[G](α, ℵ_(z))"
    using ext.lt_surj_rel_empty_imp_Card_rel M_subset_MG[OF one_in_G]
    by force
  moreover from this and ‹z∈M› ‹Ord(z)›
  have "α ∈ M" "f ∈ M[G]"
    using ext.trans_surj_rel_closed
    by (auto dest:transM ext.transM dest!:ltD)
  moreover
  note ‹ccc(ℙ,leq)› ‹z∈M›
  ultimately
  obtain F where "F:α→Pow(ℵ_(z))" "∀β∈α. f`β ∈ F`β" "∀β∈α. |F`β| ≤ ψ"
    "F ∈ M"
    using ccc_fun_approximation_lemma[of α "ℵ<sub>(z)</sub>" f]
      ext.mem_surj_abs[of f α "ℵ<sub>(z)</sub>"] ‹Ord(z)›
      surj_is_fun[of f α "ℵ<sub>(z)</sub>"] by auto
  then
  have "β ∈ α ==> |F`β| ≤ ℵ" for β
    using Aleph_rel_zero by simp
  have "w ∈ F ` x ==> x ∈ M" for w x
  proof -
    fix w x
    assume "w ∈ F`x"
    then
    have "x ∈ domain(F)"
      using apply_0 by auto
    with ‹F:α→Pow(ℵ_(z))› ‹α ∈ M›
    show "x ∈ M" using domain_of_fun
      by (auto dest:transM)
  qed
  with ‹α ∈ M› ‹F:α→Pow(ℵ_(z))› ‹F∈M›
  interpret M_cardinal_UN_lepoll "##M" "λβ. F`β" α
    using UN_lepoll_assumptions lepoll_assumptions
      lam_replacement_apply lam_replacement_inj_rel lam_replacement_minimum
  proof (unfold_locales, auto dest:transM simp del:if_range_F_else_F_def)
    fix f b
    assume "b∈M" "f∈M"
    with ‹F∈M›
    show "lam_replacement(##M, λx. μ i. x ∈ if_range_F_else_F((`)(F), b, f, i))"
      using UN_lepoll_assumptions mem_F_bound5
      by (rule_tac lam_Least_assumption_general[where U="domain", OF _ mem_F_bound5])
        simp_all
  qed
  from ‹α < \ℵ_(z)› ‹α ∈ M› ‹Ord(z)› ‹z∈M›
  have "α < ℵ"
    using
      cardinal_rel_lt_csucc_rel_iff[of "ℵ" α]
      le_Card_rel_iff[of "ℵ" α]
      Aleph_rel_succ[of z] Card_rel_lt_iff[of α "ℵ_(z)"]
      lt_Ord[of α "ℵ_(z)"]
      Card_rel_csucc_rel[of "ℵ"]
      Card_rel_Aleph_rel[THEN Card_rel_is_Ord]
    by simp
  with ‹α < \ℵ_(z)› ‹∀β∈α. |F`β| ≤ ψ› ‹α ∈ M› assms
  have "|∪β∈α. F`β| ≤ ℵ"
    using InfCard_rel_Aleph_rel[of z] Aleph_rel_zero
      subset_imp_lepoll_rel[THEN lepoll_rel_imp_cardinal_rel_le,
        of "∪β∈α. F`β" "ℵ"] Aleph_rel_succ
      Aleph_rel_increasing[THEN leI, THEN [2] le_trans, of _ 0 z]
      Ord_0_lt_iff[THEN iffD1, of z]
    by (cases "0<z"; rule_tac lepoll_rel_imp_cardinal_rel_UN_le) (auto, force)
  moreover
  note ‹z∈M› ‹Ord(z)›
  moreover from ‹∀β∈α. f`β ∈ F`β› ‹f ∈ surj<sup>[G]</sup>(α, ℵ<sub>(z)</sub>)›
    ‹α ∈ M› ‹f ∈ M[G]› and this
  have "ℵ<sub>(z)</sub> ⊆ (∪β∈α. F`β)"
    using ext.mem_surj_abs by (force simp add:surj_def)
  moreover from ‹F ∈ M› ‹α ∈ M›
  have "(∪x∈α. F ` x) ∈ M"
    using j.B_replacement
    by (intro Union_closed[simplified] RepFun_closed[simplified])
      (auto dest:transM)
  ultimately
  have "ℵ<sub>(z)</sub> ≤ ℵ"
    using subset_imp_le_cardinal_rel[of "ℵ<sub>(z)</sub>" "∪β∈α. F`β"]
      le_trans by auto
  with assms
  show "False"
    using Aleph_rel_increasing not_le_iff_lt[of "ℵ_(z)" "ℵ"]
      Card_rel_Aleph_rel[THEN Card_rel_is_Ord]
    by auto
qed

end ― ‹bundle G\_generic1\_lemmas›

end ― ‹🍋‹G_generic3_AC››

context M_ctm1
begin

abbreviation
  Add :: "i" where
  "Add ≡ Fn(ψ, ℵ × ψ, 2)"

end ― ‹🍋‹M_ctm1››

locale add_generic3 = G_generic3_AC "Fn(ψ, ℵ^#M × ψ, 2)" "Fnle(ψ, ℵ^#M × ψ, 2)" 0

sublocale add_generic3 ⊆ cohen_data ψ "ℵ × ψ" 2 by unfold_locales auto

context add_generic3
begin

notation Leq (infixl ‹⪯› 50)
notation Incompatible (infixl ‹⊥› 50)

lemma Add_subs_preserves_Aleph_succ: "Ord(z) ==> z∈M ==> Card^[G](ℵ_(z))"
  using ccc_preserves_Aleph_succ ccc_Add_subs_Aleph_2
  by auto

lemma Aleph_rel_nats_MG_eq_Aleph_rel_nats_M:
  includes G_generic1_lemmas
  assumes "z ∈ ψ"
  shows "ℵ^[G] = ℵ"
  using assms
proof (induct)
  case 0
  show ?case
    by(rule trans[OF ext.Aleph_rel_zero Aleph_rel_zero[symmetric]])
next
  case (succ z)
  then
  have "ℵ_(z) ≤ ℵ_(z)^[G]"
    using Aleph_rel_le_Aleph_rel nat_into_M by simp
  moreover from ‹z ∈ ψ›
  have "ℵ ∈ M[G]" "ℵ_(z) ∈ M[G]"
    using nat_into_M by simp_all
  moreover from this and ‹ℵ^[G] = ℵ› ‹z ∈ ψ›
  have "ℵ_(z)^[G] ≤ ℵ_(z)"
    using ext.Aleph_rel_succ nat_into_M
      Add_subs_preserves_Aleph_succ[THEN ext.csucc_rel_le, of z]
      Aleph_rel_increasing[of z "succ(z)"]
    by simp
  ultimately
  show ?case using le_anti_sym by blast
qed

abbreviation
  f_G :: "i" (‹f›) where
  "f ≡ ∪G"

abbreviation
  dom_dense :: "i ==> i" where
  "dom_dense(x) ≡ {p ∈ Add . x ∈ domain(p) }"

declare (in M_ctm2_AC) Fn_nat_closed[simplified setclass_iff, simp, intro]
declare (in M_ctm2_AC) Fnle_nat_closed[simp del, rule del,
    simplified setclass_iff, simp, intro]
declare (in M_ctm2_AC) cexp_rel_closed[simplified setclass_iff, simp, intro]
declare (in G_generic3_AC) ext.cexp_rel_closed[simplified setclass_iff, simp, intro]

lemma dom_dense_closed[intro,simp]: "x ∈ ℵ × ψ ==> dom_dense(x) ∈ M"
  using separation_in_domain[of x] nat_into_M
  by (rule_tac separation_closed[simplified], blast dest:transM) simp

lemma domain_f_G: assumes "x ∈ ℵ" "y ∈ ψ"
  shows "⟨x, y⟩ ∈ domain(f)"
proof -
  from assms
  have "Add = Fn(ψ,ℵ×ψ,2)"
    using Fn_nat_abs by auto
  moreover from this
  have "Fnle(ψ,ℵ×ψ,2) = Fnle(ψ,ℵ×ψ,2)"
    unfolding Fnle_rel_def Fnle_def by auto
  moreover from calculation assms
  have "dense(dom_dense(⟨x, y⟩))"
    using dense_dom_dense[of "⟨x,y⟩" "ℵ×ψ" ψ  2] InfCard_rel_nat
    unfolding dense_def by auto
  with assms
  obtain p where "p∈dom_dense(⟨x, y⟩)" "p∈G"
    using M_generic_denseD[of "dom_dense(⟨x, y⟩)"]
    by auto
  then
  show "⟨x, y⟩ ∈ domain(f)" by blast
qed

lemma f_G_funtype:
  includes G_generic1_lemmas
  shows "f : ℵ × ψ → 2"
  using generic domain_f_G Pi_iff Un_filter_is_function generic
    subset_trans[OF filter_subset_notion Fn_nat_subset_Pow]
  by force

lemma inj_dense_closed[intro,simp]:
  "w ∈ ℵ ==> x ∈ ℵ ==> inj_dense(ℵ,2,w,x) ∈ M"
  using transM[OF _ Aleph_rel2_closed] separation_conj separation_bex
    lam_replacement_product
    separation_in lam_replacement_fst lam_replacement_snd lam_replacement_constant
    lam_replacement_hcomp[OF lam_replacement_snd lam_replacement_restrict']
    separation_bex separation_conj
  by simp

lemma Aleph_rel2_new_reals:
  assumes "w ∈ ℵ" "x ∈ ℵ" "w ≠ x"
  shows "(λn∈ψ. f ` ⟨w, n⟩) ≠ (λn∈ψ. f ` ⟨x, n⟩)"
proof -
  have "0∈2" by auto
  with assms
  have "dense(inj_dense(ℵ,2,w,x))"
    unfolding dense_def using dense_inj_dense by auto
  with assms
  obtain p where "p∈inj_dense(ℵ,2,w,x)" "p∈G"
    using M_generic_denseD[of "inj_dense(ℵ,2,w,x)"]
    by blast
  then
  obtain n where "n ∈ ψ" "⟨⟨w, n⟩, 1⟩ ∈ p" "⟨⟨x, n⟩, 0⟩ ∈ p"
    by blast
  moreover from this and ‹p∈G›
  have "⟨⟨w, n⟩, 1⟩ ∈ f" "⟨⟨x, n⟩, 0⟩ ∈ f" by auto
  moreover from calculation
  have "f ` ⟨w, n⟩ = 1" "f ` ⟨x, n⟩ = 0"
    using f_G_funtype apply_equality
    by auto
  ultimately
  have "(λn∈ψ. f ` ⟨w, n⟩) ` n ≠ (λn∈ψ. f ` ⟨x, n⟩) ` n"
    by simp
  then
  show ?thesis by fastforce
qed

definition
  h_G :: "i" (‹h›) where
  "h ≡ λα∈ℵ. λn∈ψ. f`⟨α,n⟩"

lemma h_G_in_MG[simp]:
  includes G_generic1_lemmas
  shows "h ∈ M[G]"
  using ext.curry_closed[unfolded curry_def] G_in_MG
  unfolding h_G_def
  by simp

lemma h_G_inj_Aleph_rel2_reals: "h ∈ inj^[G](ℵ, ψ →^[G] 2)"
  using Aleph_rel_sub_closed f_G_funtype G_in_MG Aleph_rel_sub_closed
    ext.curry_rel_exp[unfolded curry_def] ext.curry_closed[unfolded curry_def]
    ext.mem_function_space_rel_abs
  by (intro ext.mem_inj_abs[THEN iffD2],simp_all)
      (auto simp: inj_def h_G_def dest:Aleph_rel2_new_reals)

lemma Aleph2_extension_le_continuum_rel:
  includes G_generic1_lemmas
  shows "ℵ^[G] ≤ 2^{<up>ℵ[G],M[G]}"
proof -
  have "ℵ^[G] <^[G] ψ →^[G] 2"
    using ext.def_lepoll_rel[of "ℵ" "ψ →^[G] 2"]
      h_G_inj_Aleph_rel2_reals Aleph_rel_nats_MG_eq_Aleph_rel_nats_M
    by auto
  moreover from calculation
  have "ℵ^[G] <^[G] |ψ →^[G] 2|^[G]"
    using ext.lepoll_rel_imp_lepoll_rel_cardinal_rel by simp
  ultimately
  have "|ℵ^[G]|^[G] ≤ 2^{<up>ℵ[G],M[G]}"
    using ext.lepoll_rel_imp_cardinal_rel_le[of "ℵ^[G]" "ψ →^[G] 2",
        OF _ _ ext.function_space_rel_closed]
      ext.Aleph_rel_zero
    unfolding cexp_rel_def by simp
  then
  show "ℵ^[G] ≤ 2^{<up>ℵ[G],M[G]}"
    using ext.Card_rel_Aleph_rel[of 2, THEN ext.Card_rel_cardinal_rel_eq]
    by simp
qed

lemma Aleph_rel_lt_continuum_rel: "ℵ^[G] < 2^{<up>ℵ[G],M[G]}"
  using Aleph2_extension_le_continuum_rel
    ext.Aleph_rel_increasing[of 1 2] le_trans by auto

corollary not_CH: "ℵ^[G] ≠ 2^{<up>ℵ[G],M[G]}"
  using Aleph_rel_lt_continuum_rel by auto

end ― ‹🍋‹add_generic3››

subsection‹Models of fragments of $\ZFC + \neg \CH$›

definition
  ContHyp :: "o" where
  "ContHyp ≡ ℵ = 2^<up>ℵ"

relativize functional "ContHyp" "ContHyp_rel"
notation ContHyp_rel (‹CH›)
relationalize "ContHyp_rel" "is_ContHyp"

context M_ZF_library
begin

is_iff_rel for "ContHyp"
  using is_cexp_iff is_Aleph_iff[of 0] is_Aleph_iff[of 1]
  unfolding is_ContHyp_def ContHyp_rel_def
  by (auto simp del:setclass_iff) (rule rexI[of _ _ M, OF _ nonempty], auto)

end ― ‹🍋‹M_ZF_library››

synthesize "is_ContHyp" from_definition assuming "nonempty"
arity_theorem for "is_ContHyp_fm"

notation is_ContHyp_fm (‹⋅CH⋅›)

theorem ctm_of_not_CH:
  assumes
    "M ≈ ψ" "Transset(M)" "M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}"
    "Φ ⊆ formula" "M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}"
  shows
    "∃N.
      M ⊆ N ∧ N ≈ ψ ∧ Transset(N) ∧ N ⊨ ZC ∪ {⋅¬⋅CH⋅⋅} ∪ { ⋅Replacement(φ)⋅ . φ ∈ Φ} ∧
      (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))"
proof -
  from ‹M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}›
  interpret M_ZFC3 M
    using M_satT_overhead_imp_M_ZF3 unfolding overhead_notCH_def by force
  from ‹M ⊨ ZC ∪ {⋅Replacement(p)⋅ . p ∈ overhead_notCH}› ‹Transset(M)›
  interpret M_ZF_ground_notCH_trans M
    using M_satT_imp_M_ZF_ground_notCH_trans
    unfolding ZC_def by auto
  from ‹M ≈ ψ›
  obtain enum where "enum ∈ bij(ψ,M)"
    using eqpoll_sym unfolding eqpoll_def by blast
  then
  interpret M_ctm3_AC M enum by unfold_locales
  interpret cohen_data ψ "ℵ × ψ" 2 by unfold_locales auto
  have "Add ∈ M" "Add_le(ℵ) ∈ M"
    using nat_into_M Aleph_rel_closed M_nat cartprod_closed Fn_nat_closed Fnle_nat_closed
    by simp_all
  then
  interpret forcing_data1 "Add" "Add_le(ℵ)" 0 M enum
    by unfold_locales simp_all
  obtain G where "M_generic(G)"
    using generic_filter_existence[OF one_in_P]
    by auto
  moreover from this
  interpret add_generic3 M enum G by unfold_locales
  have "¬ (ℵ^[G] = 2^{<up>ℵ[G],M[G]})"
    using not_CH .
  then
  have "M[G], [] ⊨ ⋅¬⋅CH⋅⋅"
    using ext.is_ContHyp_iff
    by (simp add:ContHyp_rel_def)
  then
  have "M[G] ⊨ ZC ∪ {⋅¬⋅CH⋅⋅}"
    using ext.M_satT_ZC by auto
  moreover
  have "Transset(M[G])" using Transset_MG .
  moreover
  have "M ⊆ M[G]" using M_subset_MG[OF one_in_G] generic by simp
  moreover
  note ‹M ⊨ { ⋅Replacement(ground_repl_fm(φ))⋅ . φ ∈ Φ}› ‹Φ ⊆ formula›
  ultimately
  show ?thesis
    using Ord_MG_iff MG_eqpoll_nat satT_ground_repl_fm_imp_satT_ZF_replacement_fm[of Φ]
    by (rule_tac x="M[G]" in exI, blast)
qed

lemma ZF_replacement_overhead_sub_ZFC: "{⋅Replacement(p)⋅ . p ∈ overhead} ⊆ ZFC"
  using overhead_type unfolding ZFC_def ZF_def ZF_schemes_def by auto

lemma ZF_replacement_overhead_notCH_sub_ZFC: "{⋅Replacement(p)⋅ . p ∈ overhead_notCH} ⊆ ZFC"
  using overhead_notCH_type unfolding ZFC_def ZF_def ZF_schemes_def by auto

lemma ZF_replacement_overhead_CH_sub_ZFC: "{⋅Replacement(p)⋅ . p ∈ overhead_CH} ⊆ ZFC"
  using overhead_CH_type unfolding ZFC_def ZF_def ZF_schemes_def by auto

corollary ctm_ZFC_imp_ctm_not_CH:
  assumes
    "M ≈ ψ" "Transset(M)" "M ⊨ ZFC"
  shows
    "∃N.
      M ⊆ N ∧ N ≈ ψ ∧ Transset(N) ∧ N ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅} ∧
      (∀α. Ord(α) ⟶ (α ∈ M ⟷ α ∈ N))"
proof-
  from assms
  have "∃N.
      M ⊆ N ∧
        N ≈ ψ ∧
        Transset(N) ∧
        N ⊨ ZC ∧ N ⊨ {⋅¬⋅CH⋅⋅} ∧ N ⊨ {⋅Replacement(x)⋅ . x ∈ formula} ∧ (∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)"
    using ctm_of_not_CH[of M formula] satT_ZFC_imp_satT_ZC[of M]
      satT_mono[OF _ ground_repl_fm_sub_ZFC, of M]
      satT_mono[OF _ ZF_replacement_overhead_notCH_sub_ZFC, of M]
      satT_mono[OF _ ZF_replacement_fms_sub_ZFC, of M]
    by (simp add: satT_Un_iff)
  then
  obtain N where "N ⊨ ZC" "N ⊨ {⋅¬⋅CH⋅⋅}" "N ⊨ {⋅Replacement(x)⋅ . x ∈ formula}"
    "M ⊆ N" "N ≈ ψ" "Transset(N)" "(∀α. Ord(α) ⟶ α ∈ M ⟷ α ∈ N)"
    by auto
  moreover from this
  have "N ⊨ ZFC"
    using satT_ZC_ZF_replacement_imp_satT_ZFC
    by auto
  moreover from this and ‹N ⊨ {⋅¬⋅CH⋅⋅}›
  have "N ⊨ ZFC ∪ {⋅¬⋅CH⋅⋅}"
    by auto
  ultimately
  show ?thesis by auto
qed

end