Theory Pairing_Axiom

section‹The Axiom of Pairing in $M[G]$›
theory Pairing_Axiom imports Names begin

context forcing_data
begin

lemma val_Upair :
  "one ∈ G ⟹ val(G,{⟨τ,one⟩,⟨ρ,one⟩}) = {val(G,τ),val(G,ρ)}"
  by (insert one_in_P, rule trans, subst def_val,auto simp add: Sep_and_Replace)

lemma pairing_in_MG : 
  assumes "M_generic(G)"
  shows "upair_ax(##M[G])"
proof - 
  {
    fix x y
    have "one∈G" using assms one_in_G by simp
    from assms 
    have "G⊆P" unfolding M_generic_def and filter_def by simp
    with ‹one∈G›
    have "one∈P" using subsetD by simp
    then 
    have "one∈M" using transitivity[OF _ P_in_M] by simp
    assume "x ∈ M[G]" "y ∈ M[G]"
    then 
    obtain τ ρ where
      0 : "val(G,τ) = x" "val(G,ρ) = y" "ρ ∈ M"  "τ ∈ M"
      using GenExtD by blast
    with ‹one∈M› 
    have "⟨τ,one⟩ ∈ M" "⟨ρ,one⟩∈M" using pair_in_M_iff by auto
    then 
    have 1: "{⟨τ,one⟩,⟨ρ,one⟩} ∈ M" (is "?σ ∈ _") using upair_in_M_iff by simp
    then 
    have "val(G,?σ) ∈ M[G]" using GenExtI by simp
    with 1 
    have "{val(G,τ),val(G,ρ)} ∈ M[G]" using val_Upair assms one_in_G by simp
    with 0 
    have "{x,y} ∈ M[G]" by simp
  }
  then show ?thesis unfolding upair_ax_def upair_def by auto
qed

end  (* context forcing_data *)
end