Theory Infinity_Axiom
section‹The 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
end