Theory Union_Axiom

sectionThe Axiom of Unions in $M[G]$
theory Union_Axiom
  imports Names
begin

definition Union_name_body :: "[i,i,i,i]  o" where
  "Union_name_body(P,leq,τ,x)   σdomain(τ) . qP . rP .
      σ,q  τ  fst(x),r  σ  snd(x),r  leq  snd(x),q  leq"

definition Union_name :: "[i,i,i]  i" where
  "Union_name(P,leq,τ)  {u  domain((domain(τ))) × P . Union_name_body(P,leq,τ,u)}"

context forcing_data1
begin

lemma Union_name_closed :
  assumes "τ  M"
  shows "Union_name(,leq,τ)  M"
proof -
  let ?Q="Union_name_body(,leq,τ)"
  note lr_fst2 = lam_replacement_hcomp[OF lam_replacement_fst lam_replacement_fst]
    and lr_fst3 = lam_replacement_hcomp[OF lr_fst2] lam_replacement_hcomp[OF lr_fst2 lr_fst2]
  note τM
  moreover from this
  have "domain((domain(τ)))M" (is "?d  _")
    using domain_closed Union_closed by simp
  moreover from this
  have "?d ×   M"
    using cartprod_closed by simp
  note types = assms ?d×  M ?dM
  ultimately
  show ?thesis
    using domain_closed pair_in_M_iff fst_closed snd_closed separation_closed
      lam_replacement_constant lam_replacement_hcomp
      lam_replacement_fst lam_replacement_snd lam_replacement_product
      separation_bex separation_conj separation_in lr_fst2 lr_fst3
      lam_replacement_hcomp[OF lr_fst3(1) lam_replacement_snd]
    unfolding Union_name_body_def Union_name_def
    by simp
qed

lemma Union_MG_Eq :
  assumes "a  M[G]" and "a = val(G,τ)" and "filter(G)" and "τ  M"
  shows " a = val(G,Union_name(,leq,τ))"
proof (intro equalityI subsetI)
  fix x
  assume "x   a"
  with a=_
  have "x   (val(G,τ))"
    by simp
  then
  obtain i where "i  val(G,τ)" "x  i"
    by blast
  with τ  M
  obtain σ q where "q  G" "σ,q  τ" "val(G,σ) = i" "σ  M"
    using elem_of_val_pair domain_trans[OF trans_M] by blast
  moreover from this x  i
  obtain θ r where "r  G" "θ,r  σ" "val(G,θ) = x" "θ  M"
    using elem_of_val_pair domain_trans[OF trans_M] by blast
  moreover from calculation
  have "θ  domain((domain(τ)))"
    by auto
  moreover from calculation filter(G)
  obtain p where "p  G" "p,r  leq" "p,q  leq" "p  " "r  " "q  "
    using low_bound_filter filterD by blast
  moreover from this
  have "p  M" "qM" "rM"
    by (auto dest:transitivity)
  moreover from calculation
  have "θ,p  Union_name(,leq,τ)"
    unfolding Union_name_def Union_name_body_def
    by auto
  moreover from this p pG
  have "val(G,θ)  val(G,Union_name(,leq,τ))"
    using val_of_elem by simp
  ultimately
  show "x  val(G,Union_name(,leq,τ))"
    by simp
next
  fix x
  assume "x  (val(G,Union_name(,leq,τ)))"
  moreover
  note filter(G) a=val(G,τ)
  moreover from calculation
  obtain θ p where "p  G" "θ,p  Union_name(,leq,τ)" "val(G,θ) = x"
    using elem_of_val_pair by blast
  moreover from calculation
  have "p"
    using filterD by simp
  moreover from calculation
  obtain σ q r where "σ,q  τ" "θ,r  σ" "p,r  leq" "p,q  leq" "r" "q"
    unfolding Union_name_def Union_name_body_def
    by auto
  moreover from calculation
  have "r  G" "q  G"
    using filter_leqD by auto
  moreover from this θ,r  σ σ,qτ q r
  have "val(G,σ)  val(G,τ)" "val(G,θ)  val(G,σ)"
    using val_of_elem by simp+
  ultimately
  show "x   a"
    by blast
qed

lemma union_in_MG :
  assumes "filter(G)"
  shows "Union_ax(##M[G])"
  unfolding Union_ax_def
proof(clarsimp)
  fix a
  assume "a  M[G]"
  moreover
  note filter(G)
  moreover from calculation
  interpret mgtrans : M_trans "##M[G]"
    using transitivity_MG by (unfold_locales; auto)
  from calculation
  obtain τ where "τ  M" "a=val(G,τ)"
    using GenExtD by blast
  moreover from this
  have "val(G,Union_name(,leq,τ))  M[G]"
    using GenExtI Union_name_closed by simp
  ultimately
  show "zM[G] . big_union(##M[G],a,z)"
    using Union_MG_Eq by auto
qed

theorem Union_MG : "M_generic(G)  Union_ax(##M[G])"
  by (auto simp:union_in_MG)

end ― ‹localeforcing_data1

end