theory Infinity_Axiom
imports Pairing_Axiom Union_Axiom
begin
locale G_generic = forcing_data +
fixes G :: "i"
assumes generic : "M_generic(G)"
begin
lemma zero_in_MG :
"0 ∈ M[G]"
proof -
from zero_in_M and elem_of_val have
"0 = val(G,0)"
by auto
also from GenExtI and zero_in_M have
"... ∈ M[G]"
by simp
finally show ?thesis .
qed
end
sublocale G_generic ⊆ M_trivial"##M[G]"
using generic Union_MG pairing_in_MG zero_in_MG Transset_intf Transset_MG
unfolding M_trivial_def by simp
locale G_generic_extra = G_generic + M_extra_assms
begin
lemma infinty_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 Transset_MG Transset_intf by simp
with ‹I∈M› have "y ∈ M" if "y ∈ I" for y
using Transset_intf[OF trans_M _ ‹I∈M›] that by simp
with ‹I∈M[G]› have "succ(y) ∈ I ∩ M[G]" if "y ∈ I" for y
using that Eq1 Transset_MG Transset_intf by blast
with Eq1 ‹I∈M[G]› ‹0∈M[G]› show ?thesis
unfolding infinity_ax_def by auto
qed
end
end