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
end