Theory Extensionality_Axiom

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

theory Extensionality_Axiom
  imports
    Names
begin

context forcing_data1
begin

lemma extensionality_in_MG : "extensionality(##(M[G]))"
  unfolding extensionality_def
proof(clarsimp)
  fix x y
  assume "xM[G]" "yM[G]" "(wM[G] . w  x  w  y)"
  moreover from this
  have "zx  zM[G]  zy" for z
    using transitivity_MG by auto
  moreover from calculation
  have "zM[G]  zx  zy" for z
    using transitivity_MG by auto
  ultimately
  show "x=y"
    by auto
qed

end ― ‹localeforcing_data1

end