Theory Infinity_Axiom

sectionThe Axiom of Infinity in $M[G]$
theory Infinity_Axiom
  imports Union_Axiom Pairing_Axiom
begin

context G_generic1 begin

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

lemma infinity_in_MG : "infinity_ax(##M[G])"
proof -
  have "ω  M[G]"
    using M_subset_MG one_in_G nat_in_M by auto
  moreover from this
  have "succ(y)  ω  M[G]" if "y  ω" for y
    using that transitivity_MG by blast
  ultimately
  show ?thesis
    using transitivity_MG[of 0 ω]
    unfolding infinity_ax_def
    by auto
qed

end ― ‹localeG_generic1

end