Theory Infinity_Axiom

section‹The Axiom of Infinity in $M[G]$›
theory Infinity_Axiom
  imports Pairing_Axiom Union_Axiom Separation_Axiom
begin

context G_generic begin

interpretation mg_triv: M_trivial"##M[G]"
  using transitivity_MG zero_in_MG generic Union_MG pairing_in_MG
  by unfold_locales auto

lemma infinity_in_MG : "infinity_ax(##M[G])"
proof -
  from infinity_ax obtain I where
    Eq1: "I∈M" "0 ∈ I" "∀y∈M. y ∈ I ⟶ succ(y) ∈ I"
    unfolding infinity_ax_def  by auto
  then
  have "check(I) ∈ M"
    using check_in_M by simp
  then
  have "I∈ M[G]"
    using valcheck generic one_in_G one_in_P GenExtI[of "check(I)" G] by simp
  with ‹0∈I›
  have "0∈M[G]" using transitivity_MG by simp
  with ‹I∈M›
  have "y ∈ M" if "y ∈ I" for y
    using  transitivity[OF _ ‹I∈M›] that by simp
  with ‹I∈M[G]›
  have "succ(y) ∈ I ∩ M[G]" if "y ∈ I" for y
    using that Eq1 transitivity_MG by blast
  with Eq1 ‹I∈M[G]› ‹0∈M[G]›
  show ?thesis
    unfolding infinity_ax_def by auto
qed

end (* G_generic' *)
end