Theory Powerset_Axiom

sectionThe Powerset Axiom in $M[G]$

theory Powerset_Axiom
  imports
    Separation_Axiom Pairing_Axiom Union_Axiom
begin

simple_rename "perm_pow" src "[ss,p,l,o,fs,χ]" tgt "[fs,ss,sp,p,l,o,χ]"

context G_generic1
begin

lemma sats_fst_snd_in_M:
  assumes
    "AM" "BM" "φ  formula" "pM" "lM" "oM" "χM" "arity(φ)  6"
  shows "{s,qA×B . M, [q,p,l,o,s,χ]  φ}  M" (is "  M")
proof -
  let ?φ' = "ren(φ)`6`7`perm_pow_fn"
  from AM BM
  have "A×B  M"
    using cartprod_closed by simp
  from arity(φ)  6 φ formula
  have "?φ'  formula" "arity(?φ')7"
    unfolding perm_pow_fn_def
    using perm_pow_thm  arity_ren ren_tc Nil_type
    by auto
  with ?φ'  formula
  have arty: "arity(Exists(Exists(And(pair_fm(0,1,2),?φ'))))5" (is "arity()5")
    using ord_simp_union pred_le
    by (auto simp:arity)
  {
    fix sp
    note A×B  M AM BM
    moreover
    assume "sp  A×B"
    moreover from calculation
    have "fst(sp)  A" "snd(sp)  B"
      using fst_type snd_type by simp_all
    ultimately
    have "sp  M" "fst(sp)  M" "snd(sp)  M"
      using transitivity
      by simp_all
    note inM = AM BM pM lM oM χM
      spM fst(sp)M snd(sp)M
    with arty sp  M ?φ'  formula
    have "(M, [sp,p,l,o,χ]@[p]  )  M,[sp,p,l,o,χ]  " (is "(M,?env0@ __)  _")
      using arity_sats_iff[of  "[p]" M ?env0] by auto
    also from inM sp  A×B
    have "...  sats(M,?φ',[fst(sp),snd(sp),sp,p,l,o,χ])"
      by auto
    also from inM φ  formula arity(φ)  6
    have "...  M, [snd(sp),p,l,o,fst(sp),χ]  φ"
      (is "sats(_,_,?env1)  sats(_,_,?env2)")
      using sats_iff_sats_ren[of φ 6 7 ?env2 M ?env1 perm_pow_fn] perm_pow_thm
      unfolding perm_pow_fn_def by simp
    finally
    have "(M,[sp,p,l,o,χ,p]  )  M, [snd(sp),p,l,o,fst(sp),χ]  φ"
      by simp
  }
  then
  have " = {spA×B . sats(M,,[sp,p,l,o,χ,p])}"
    by auto
  with assms A×BM
  show ?thesis
    using separation_ax separation_iff arty leI ?φ'  formula
    by simp
qed

declare nat_into_M[rule del, simplified setclass_iff, intro]
lemmas ssimps = domain_closed cartprod_closed cons_closed Pow_rel_closed
declare ssimps [simp del, simplified setclass_iff, simp, intro]

― ‹We keep termPow(a)  M[G] to be consistent with Kunen.
lemma Pow_inter_MG:
  assumes "aM[G]"
  shows "Pow(a)  M[G]  M[G]"
proof -
  from assms
  obtain τ where "τ  M" "val(G, τ) = a"
    using GenExtD by auto
  let ?Q="Pow⇗M⇖(domain(τ)×)"
  let ="?Q×{𝟭}"
  let ?b="val(G,)"
  from τM
  have "domain(τ)×  M" "domain(τ)  M"
    by simp_all
  then
  have "?b  M[G]"
    by (auto intro!:GenExtI)
  have "Pow(a)  M[G]  ?b"
  proof
    fix c
    assume "c  Pow(a)  M[G]"
    then
    obtain χ where "cM[G]" "χ  M" "val(G,χ) = c"
      using GenExt_iff by auto
    let ="{σ,p domain(τ)× . p  0  1 [σ,χ] }"
    have "arity(forces( 0  1 )) = 6"
      using arity_forces_at by auto
    with domain(τ)  M χ  M
    have "  M"
      using sats_fst_snd_in_M
      by simp
    with domain(τ)×  M
    have "  ?Q"
      using Pow_rel_char by auto
    have "val(G,) = c"
    proof(intro equalityI subsetI)
      fix x
      assume "x  val(G,)"
      then
      obtain σ p where 1: "σ,p" "pG" "val(G,σ) =  x"
        using elem_of_val_pair
        by blast
      moreover from σ,p   M
      have "σM"
        using name_components_in_M[of _ _ ] by auto
      moreover from 1
      have "p  0  1 [σ,χ]" "p"
        by simp_all
      moreover
      note val(G,χ) = c χ  M
      ultimately
      have "M[G], [x, c]  0  1"
        using generic definition_of_forcing[where φ="0  1"] ord_simp_union
        by auto
      moreover from σM χM
      have "xM[G]"
        using val(G,σ) = x GenExtI by blast
      ultimately
      show "xc"
        using cM[G] by simp
    next
      fix x
      assume "x  c"
      with c  Pow(a)  M[G]
      have "x  a" "cM[G]" "xM[G]"
        using transitivity_MG by auto
      with val(G, τ) = a
      obtain σ where "σdomain(τ)" "val(G,σ) = x"
        using elem_of_val by blast
      moreover
      note xc val(G,χ) = c cM[G] xM[G]
      moreover from calculation
      have "val(G,σ)  val(G,χ)"
        by simp
      moreover from calculation
      have "M[G], [x, c]  0  1"
        by simp
      moreover
      have "σM"
      proof -
        from σdomain(τ)
        obtain p where "σ,p  τ"
          by auto
        with τM
        show ?thesis
          using name_components_in_M by blast
      qed
      moreover
      note χ  M
      ultimately
      obtain p where "pG" "p  0  1 [σ,χ]"
        using generic truth_lemma[of "0  1" "[σ,χ]" ] ord_simp_union
        by auto
      moreover from pG
      have "p"
        using generic by blast
      ultimately
      have "σ,p"
        using σdomain(τ) by simp
      with val(G,σ) =  x pG
      show "xval(G,)"
        using val_of_elem [of _ _ "" G] by auto
    qed
    with   ?Q
    show "c?b"
      using one_in_G generic val_of_elem [of  𝟭  G]
      by auto
  qed
  then
  have "Pow(a)  M[G] = {x?b . xa  xM[G]}"
    by auto
  also from aM[G]
  have " ... = {x?b . ( M[G], [x,a]  0  1 )}  M[G]"
    using Transset_MG by force
  also from ?bM[G]
  have " ... = {x?b . ( M[G], [x,a]  0  1 )}"
    by (intro equalityI) (auto dest:ext.transM)
  also from ?bM[G] aM[G]
  have " ...  M[G]"
    using Collect_sats_in_MG GenExtI ord_simp_union by (simp add:arity)
  finally
  show ?thesis .
qed

end ― ‹localeG_generic1

sublocale G_generic1  ext: M_trivial "##M[G]"
  using generic Union_MG pairing_in_MG
  by unfold_locales (simp; blast)

context G_generic1 begin

theorem power_in_MG : "power_ax(##(M[G]))"
  unfolding power_ax_def
proof (intro rallI, simp only:setclass_iff rex_setclass_is_bex)
  fix a
  textAfter simplification, we have to show that for every
  termaM[G] there exists some termxM[G] satisfying
  termpowerset(##M[G],a,x)
  assume "a  M[G]"
  have "{xPow(a) . x  M[G]} = Pow(a)  M[G]"
    by auto
  also from aM[G]
  have " ...  M[G]"
    using Pow_inter_MG by simp
  finally
  have "{xPow(a) . x  M[G]}  M[G]" .
  moreover from aM[G] this
  have "powerset(##M[G], a, {xPow(a) . x  M[G]})"
    using ext.powerset_abs
    by simp
  ultimately
  show "xM[G] . powerset(##M[G], a, x)"
    by auto
qed

end ― ‹localeG_generic1

end