Let seq be given.
Assume Hseq: function_on seq ω S_Omega.
We will prove ∃b : set, b ∈ S_Omega ∧ ∀n : set, n ∈ ω → apply_fun seq n ∈ b.
Set A to be the term {apply_fun seq n|n ∈ ω}.
We prove the intermediate claim HAcS: A ⊆ S_Omega.
Let y be given.
Assume Hy: y ∈ A.
We will prove y ∈ S_Omega.
Apply (ReplE_impred ω (λn0 : set ⇒ apply_fun seq n0) y Hy) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume Hydef: y = apply_fun seq n.
rewrite the current goal using Hydef (from left to right).
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim HAcount: countable_set A.
We will prove countable_set A.
We prove the intermediate claim HomegaCount: countable_set ω.
We will prove countable_set ω.
We will prove countable ω.
An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).
An exact proof term for the current goal is (countable_image ω HomegaCount (λn0 : set ⇒ apply_fun seq n0)).
We prove the intermediate claim Hexb: ∃b : set, b ∈ S_Omega ∧ ∀a : set, a ∈ A → a ∈ b.
An exact proof term for the current goal is (S_Omega_countable_subsets_bounded A HAcS HAcount).
Apply Hexb to the current goal.
Let b be given.
Assume Hb: b ∈ S_Omega ∧ ∀a : set, a ∈ A → a ∈ b.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (b ∈ S_Omega) (∀a : set, a ∈ A → a ∈ b) Hb).
Let n be given.
Assume HnO: n ∈ ω.
We prove the intermediate claim HAn: apply_fun seq n ∈ A.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ apply_fun seq n0) n HnO).
An exact proof term for the current goal is ((andER (b ∈ S_Omega) (∀a : set, a ∈ A → a ∈ b) Hb) (apply_fun seq n) HAn).
∎