We will prove Romega_infty = {f ∈ R_omega_space|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0}.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ Romega_infty.
We will prove f ∈ {f0 ∈ R_omega_space|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f0 i = 0}.
Apply (UnionE_impred {Romega_tilde n|n ∈ ω} f Hf) to the current goal.
Let Y be given.
Assume HfY: f ∈ Y.
Assume HY: Y ∈ {Romega_tilde n|n ∈ ω}.
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) Y HY (f ∈ {f0 ∈ R_omega_space|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f0 i = 0})) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HYeq: Y = Romega_tilde n.
We prove the intermediate claim Hfn: f ∈ Romega_tilde n.
rewrite the current goal using HYeq (from right to left).
An exact proof term for the current goal is HfY.
We prove the intermediate claim HfX: f ∈ R_omega_space.
An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ ∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0) f Hfn).
We prove the intermediate claim Htail0: ∀i : set, i ∈ ω → n ∈ i → apply_fun f i = 0.
An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ ∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0) f Hfn).
Set F to be the term ordsucc n.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (nat_finite F (nat_ordsucc n HnNat)).
We prove the intermediate claim Hprop: ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0.
Let i be given.
Assume Hi: i ∈ ω ∖ F.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (setminusE1 ω F i Hi).
We prove the intermediate claim HinF: i ∉ F.
An exact proof term for the current goal is (setminusE2 ω F i Hi).
We prove the intermediate claim Hordn: ordinal n.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal n HnO).
We prove the intermediate claim Hordi: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i HiO).
Apply (ordinal_trichotomy_or_impred i n Hordi Hordn (apply_fun f i = 0)) to the current goal.
Assume Hin: i ∈ n.
We will prove apply_fun f i = 0.
Apply FalseE to the current goal.
We prove the intermediate claim HiF: i ∈ F.
An exact proof term for the current goal is (ordsuccI1 n i Hin).
An exact proof term for the current goal is (HinF HiF).
Assume Heq: i = n.
We will prove apply_fun f i = 0.
Apply FalseE to the current goal.
We prove the intermediate claim HiF: i ∈ F.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (ordsuccI2 n).
An exact proof term for the current goal is (HinF HiF).
Assume Hnin: n ∈ i.
An exact proof term for the current goal is (Htail0 i HiO Hnin).
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
We will prove ∃F0 : set, finite F0 ∧ ∀i : set, i ∈ ω ∖ F0 → apply_fun f i = 0.
We use F to witness the existential quantifier.
We will prove finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0.
Apply andI to the current goal.
An exact proof term for the current goal is HFfin.
An exact proof term for the current goal is Hprop.
Let f be given.
Assume Hf: f ∈ {f0 ∈ R_omega_space|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f0 i = 0}.
We will prove f ∈ Romega_infty.
We prove the intermediate claim HfX: f ∈ R_omega_space.
An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ ∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f0 i = 0) f Hf).
We prove the intermediate claim HexF: ∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0.
An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ ∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f0 i = 0) f Hf).
Apply HexF to the current goal.
Let F be given.
Assume HFconj.
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (andEL (finite F) (∀i : set, i ∈ ω ∖ F → apply_fun f i = 0) HFconj).
We prove the intermediate claim HFsupp: ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0.
An exact proof term for the current goal is (andER (finite F) (∀i : set, i ∈ ω ∖ F → apply_fun f i = 0) HFconj).
Set Fomega to be the term ω ∩ F.
We prove the intermediate claim HFomegaSubO: Fomega ⊆ ω.
An exact proof term for the current goal is (binintersect_Subq_1 ω F).
We prove the intermediate claim HFomegaSubF: Fomega ⊆ F.
An exact proof term for the current goal is (binintersect_Subq_2 ω F).
We prove the intermediate claim HFomegaFin: finite Fomega.
An exact proof term for the current goal is (Subq_finite F HFfin Fomega HFomegaSubF).
We prove the intermediate claim Hexn: ∃n ∈ ω, ∀m ∈ Fomega, m ∈ n.
An exact proof term for the current goal is (finite_subset_of_omega_bounded Fomega HFomegaSubO HFomegaFin).
Apply Hexn to the current goal.
Let n be given.
Assume Hnconj.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (∀m ∈ Fomega, m ∈ n) Hnconj).
We prove the intermediate claim Hbound: ∀m ∈ Fomega, m ∈ n.
An exact proof term for the current goal is (andER (n ∈ ω) (∀m ∈ Fomega, m ∈ n) Hnconj).
We prove the intermediate claim Hfn: f ∈ Romega_tilde n.
We will prove f ∈ {f0 ∈ R_omega_space|∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hnin: n ∈ i.
We will prove apply_fun f i = 0.
We prove the intermediate claim HinFomega: i ∉ Fomega.
Assume HiFomega: i ∈ Fomega.
We will prove False.
We prove the intermediate claim HinN: i ∈ n.
An exact proof term for the current goal is (Hbound i HiFomega).
An exact proof term for the current goal is (In_no2cycle i n HinN Hnin).
We prove the intermediate claim HinF: i ∉ F.
Assume HiF: i ∈ F.
We will prove False.
We prove the intermediate claim HiFomega: i ∈ Fomega.
An exact proof term for the current goal is (binintersectI ω F i HiO HiF).
An exact proof term for the current goal is (HinFomega HiFomega).
We prove the intermediate claim HiOF: i ∈ ω ∖ F.
An exact proof term for the current goal is (setminusI ω F i HiO HinF).
An exact proof term for the current goal is (HFsupp i HiOF).
Set Fam to be the term {Romega_tilde k|k ∈ ω}.
We prove the intermediate claim HFn: Romega_tilde n ∈ Fam.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ Romega_tilde k) n HnO).
An exact proof term for the current goal is (UnionI Fam f (Romega_tilde n) Hfn HFn).
∎