Theory Pairing_Axiom

section‹The Axiom of Pairing in $M[G]$›

theory Pairing_Axiom
  imports
    Names
begin

context G_generic1
begin

lemma val_Upair :
  "𝟭 ∈ G ⟹ val(G,{⟨τ,𝟭⟩,⟨ρ,𝟭⟩}) = {val(G,τ),val(G,ρ)}"
  by (rule trans, subst def_val,auto)

lemma pairing_in_MG : "upair_ax(##M[G])"
proof -
  {
    fix x y
    assume "x ∈ M[G]" "y ∈ M[G]"
    moreover from this
    obtain τ ρ where "val(G,τ) = x" "val(G,ρ) = y" "ρ ∈ M"  "τ ∈ M"
      using GenExtD by blast
    moreover from this
    have "⟨τ,𝟭⟩ ∈ M" "⟨ρ,𝟭⟩∈M"
      using pair_in_M_iff by auto
    moreover from this
    have "{⟨τ,𝟭⟩,⟨ρ,𝟭⟩} ∈ M" (is "?σ ∈ _")
      using upair_in_M_iff by simp
    moreover from this
    have "val(G,?σ) ∈ M[G]"
      using GenExtI by simp
    moreover from calculation
    have "{val(G,τ),val(G,ρ)} ∈ M[G]"
      using val_Upair one_in_G by simp
    ultimately
    have "{x,y} ∈ M[G]"
      by simp
  }
  then
  show ?thesis
    unfolding upair_ax_def upair_def by auto
qed

end ― ‹\<^locale>‹G_generic1››

end