Theory Extensionality_Axiom

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

context forcing_data
begin
  
lemma extensionality_in_MG : "extensionality(##(M[G]))"
proof -
  {
    fix x y z
    assume 
      asms: "x∈M[G]" "y∈M[G]" "(∀w∈M[G] . w ∈ x ⟷ w ∈ y)"
    from ‹x∈M[G]› have
      "z∈x ⟷ z∈M[G] ∧ z∈x"
      using transitivity_MG by auto
    also have
      "... ⟷ z∈y"
      using asms transitivity_MG by auto
    finally have
      "z∈x ⟷ z∈y" .
  }
  then have
    "∀x∈M[G] . ∀y∈M[G] . (∀z∈M[G] . z ∈ x ⟷ z ∈ y) ⟶ x = y"
    by blast
  then show ?thesis unfolding extensionality_def by simp
qed
 
end  (* context forcing_data *)
end