We will prove bounded_sequences_Romega ≠ Empty.
Assume Heq: bounded_sequences_Romega = Empty.
We will prove False.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set U to be the term space_family_union ω Xi.
Set f0 to be the term const_fun ω 0.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HR0: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HX0: apply_fun Xi 0 = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology 0 H0omega).
We prove the intermediate claim Hset0: space_family_set Xi 0 = R.
We prove the intermediate claim Hdef: space_family_set Xi 0 = (apply_fun Xi 0) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HX0 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
We prove the intermediate claim HRfam: R ∈ {space_family_set Xi i|i ∈ ω}.
Apply ReplEq ω (λi : set ⇒ space_family_set Xi i) R to the current goal.
Assume _ H2.
Apply H2 to the current goal.
We will prove ∃i ∈ ω, R = space_family_set Xi i.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H0omega.
We will prove R = space_family_set Xi 0.
Use symmetry.
An exact proof term for the current goal is Hset0.
We prove the intermediate claim H0U: 0 ∈ U.
An exact proof term for the current goal is (UnionI {space_family_set Xi i|i ∈ ω} 0 R HR0 HRfam).
We prove the intermediate claim Hf0: f0 ∈ R_omega_space.
We will prove f0 ∈ product_space ω Xi.
We will prove f0 ∈ {f ∈ 𝒫 (setprod ω (space_family_union ω Xi))|total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i}.
Set U0 to be the term space_family_union ω Xi.
We prove the intermediate claim Hsub: f0 ⊆ setprod ω U0.
Let p be given.
Assume Hp: p ∈ f0.
We will prove p ∈ setprod ω U0.
Apply (ReplE_impred ω (λa : set ⇒ (a,0)) p Hp (p ∈ setprod ω U0)) to the current goal.
Let a be given.
Assume HaO: a ∈ ω.
Assume Hpeq: p = (a,0).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω U0 a 0 HaO H0U).
We prove the intermediate claim Hpow: f0 ∈ 𝒫 (setprod ω U0).
An exact proof term for the current goal is (PowerI (setprod ω U0) f0 Hsub).
We prove the intermediate claim Htot: total_function_on f0 ω U0.
An exact proof term for the current goal is (const_fun_total_function_on ω U0 0 H0U).
We prove the intermediate claim Hgraph: functional_graph f0.
An exact proof term for the current goal is (functional_graph_const_fun ω 0).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun f0 i ∈ space_family_set Xi i.
We prove the intermediate claim Happ: apply_fun f0 i = 0.
An exact proof term for the current goal is (const_fun_apply ω 0 i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HX: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).
We prove the intermediate claim Hset: space_family_set Xi i = R.
We prove the intermediate claim Hdef: space_family_set Xi i = (apply_fun Xi i) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HX (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
rewrite the current goal using Hset (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hprop: total_function_on f0 ω U0 ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is Hgraph.
An exact proof term for the current goal is Hcoords.
An exact proof term for the current goal is (SepI (𝒫 (setprod ω U0)) (λf : set ⇒ total_function_on f ω U0 ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i) f0 Hpow Hprop).
We prove the intermediate claim Hbseq: bounded_sequence_Romega f0.
We prove the intermediate claim Hbnd1: ∀n : set, n ∈ ω → apply_fun f0 n ∈ open_interval (minus_SNo 1) 1.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun f0 n ∈ open_interval (minus_SNo 1) 1.
We prove the intermediate claim Happ: apply_fun f0 n = 0.
An exact proof term for the current goal is (const_fun_apply ω 0 n HnO).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1lt0: Rlt (minus_SNo 1) 0.
An exact proof term for the current goal is (RltI (minus_SNo 1) 0 Hm1R real_0 minus_1_lt_0).
We prove the intermediate claim H0lt1: Rlt 0 1.
An exact proof term for the current goal is Rlt_0_1.
We prove the intermediate claim Hconj: Rlt (minus_SNo 1) 0 ∧ Rlt 0 1.
Apply andI to the current goal.
An exact proof term for the current goal is Hm1lt0.
An exact proof term for the current goal is H0lt1.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) 0 real_0 Hconj).
An exact proof term for the current goal is (λP Hp ⇒ Hp 1 (andI (1 ∈ R) (∀n : set, n ∈ ω → apply_fun f0 n ∈ open_interval (minus_SNo 1) 1) real_1 Hbnd1)).
We prove the intermediate claim Hf0B: f0 ∈ bounded_sequences_Romega.
An exact proof term for the current goal is (SepI R_omega_space (λf : set ⇒ bounded_sequence_Romega f) f0 Hf0 Hbseq).
We prove the intermediate claim Hf0E: f0 ∈ Empty.
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is Hf0B.
An exact proof term for the current goal is (EmptyE f0 Hf0E).
∎