We will prove unbounded_sequences_Romega ≠ Empty.
Assume Heq: unbounded_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 fid to be the term {(i,i)|i ∈ ω}.
We prove the intermediate claim Hfid: fid ∈ R_omega_space.
We will prove fid ∈ product_space ω Xi.
We will prove fid ∈ {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}.
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 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.
Use symmetry.
An exact proof term for the current goal is Hset0.
We prove the intermediate claim HomegaU: ∀i : set, i ∈ ω → i ∈ U.
Let i be given.
Assume Hi: i ∈ ω.
We will prove i ∈ U.
We prove the intermediate claim HiR: i ∈ R.
We prove the intermediate claim HiSNoS: i ∈ SNoS_ ω.
An exact proof term for the current goal is (omega_SNoS_omega i Hi).
An exact proof term for the current goal is (SNoS_omega_real i HiSNoS).
An exact proof term for the current goal is (UnionI {space_family_set Xi i0|i0 ∈ ω} i R HiR HRfam).
We prove the intermediate claim Hsub: fid ⊆ setprod ω U.
Let p be given.
Assume Hp: p ∈ fid.
We will prove p ∈ setprod ω U.
Apply (ReplE_impred ω (λi : set ⇒ (i,i)) p Hp (p ∈ setprod ω U)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume Hpeq: p = (i,i).
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 ω U i i Hi (HomegaU i Hi)).
We prove the intermediate claim Hpow: fid ∈ 𝒫 (setprod ω U).
An exact proof term for the current goal is (PowerI (setprod ω U) fid Hsub).
We prove the intermediate claim Hfun: function_on fid ω U.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun fid i ∈ U.
We prove the intermediate claim Happ: apply_fun fid i = i.
An exact proof term for the current goal is (identity_function_apply ω i Hi).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (HomegaU i Hi).
We prove the intermediate claim Htot: total_function_on fid ω U.
We prove the intermediate claim Htot': ∀i : set, i ∈ ω → ∃y : set, y ∈ U ∧ (i,y) ∈ fid.
Let i be given.
Assume Hi: i ∈ ω.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (HomegaU i Hi).
An exact proof term for the current goal is (ReplI ω (λi0 : set ⇒ (i0,i0)) i Hi).
An exact proof term for the current goal is (andI (function_on fid ω U) (∀x : set, x ∈ ω → ∃y : set, y ∈ U ∧ (x,y) ∈ fid) Hfun Htot').
We prove the intermediate claim Hgraph: functional_graph fid.
An exact proof term for the current goal is (functional_graph_graph ω (λi0 : set ⇒ i0)).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ ω → apply_fun fid i ∈ space_family_set Xi i.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun fid i ∈ space_family_set Xi i.
We prove the intermediate claim Happ: apply_fun fid i = i.
An exact proof term for the current goal is (identity_function_apply ω i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hset: space_family_set Xi i = R.
We prove the intermediate claim HXi: 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 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 HXi (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).
We prove the intermediate claim HiSNoS: i ∈ SNoS_ ω.
An exact proof term for the current goal is (omega_SNoS_omega i Hi).
An exact proof term for the current goal is (SNoS_omega_real i HiSNoS).
We prove the intermediate claim Hprop: total_function_on fid ω U ∧ functional_graph fid ∧ ∀i : set, i ∈ ω → apply_fun fid 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 ω U)) (λf : set ⇒ total_function_on f ω U ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i) fid Hpow Hprop).
We prove the intermediate claim Huseq: unbounded_sequence_Romega fid.
Let M be given.
Assume HM: M ∈ R.
We prove the intermediate claim HMS: SNo M.
An exact proof term for the current goal is (real_SNo M HM).
We prove the intermediate claim Hor: M < 0 ∨ 0 ≤ M.
An exact proof term for the current goal is (SNoLtLe_or M 0 HMS SNo_0).
We prove the intermediate claim Hcase1: M < 0 → ∃n : set, n ∈ ω ∧ ¬ (apply_fun fid n ∈ open_interval (minus_SNo M) M).
Assume HMlt0: M < 0.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We will prove ¬ (apply_fun fid 0 ∈ open_interval (minus_SNo M) M).
Assume Hin: apply_fun fid 0 ∈ open_interval (minus_SNo M) M.
We prove the intermediate claim Happ: apply_fun fid 0 = 0.
An exact proof term for the current goal is (identity_function_apply ω 0 (nat_p_omega 0 nat_0)).
We prove the intermediate claim Hprop: Rlt (minus_SNo M) (apply_fun fid 0) ∧ Rlt (apply_fun fid 0) M.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo M) x0 ∧ Rlt x0 M) (apply_fun fid 0) Hin).
We prove the intermediate claim HRlt0M: Rlt 0 M.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is (andER (Rlt (minus_SNo M) (apply_fun fid 0)) (Rlt (apply_fun fid 0) M) Hprop).
We prove the intermediate claim HRltM0: Rlt M 0.
An exact proof term for the current goal is (RltI M 0 HM real_0 HMlt0).
We prove the intermediate claim Hnot: ¬ (Rlt 0 M).
An exact proof term for the current goal is (not_Rlt_sym M 0 HRltM0).
An exact proof term for the current goal is (Hnot HRlt0M).
We prove the intermediate claim Hcase2: 0 ≤ M → ∃n : set, n ∈ ω ∧ ¬ (apply_fun fid n ∈ open_interval (minus_SNo M) M).
Assume HMnonneg: 0 ≤ M.
We prove the intermediate claim Hexn0: ∃n ∈ ω, n ≤ M ∧ M < ordsucc n.
An exact proof term for the current goal is (nonneg_real_nat_interval M HM HMnonneg).
Apply Hexn0 to the current goal.
Let n0 be given.
Assume Hn0conj.
We prove the intermediate claim Hn0: n0 ∈ ω.
An exact proof term for the current goal is (andEL (n0 ∈ ω) (n0 ≤ M ∧ M < ordsucc n0) Hn0conj).
We prove the intermediate claim Hn0prop: n0 ≤ M ∧ M < ordsucc n0.
An exact proof term for the current goal is (andER (n0 ∈ ω) (n0 ≤ M ∧ M < ordsucc n0) Hn0conj).
We prove the intermediate claim HMltS: M < ordsucc n0.
An exact proof term for the current goal is (andER (n0 ≤ M) (M < ordsucc n0) Hn0prop).
Set n to be the term ordsucc n0.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (omega_ordsucc n0 Hn0).
We will prove ¬ (apply_fun fid n ∈ open_interval (minus_SNo M) M).
Assume Hin: apply_fun fid n ∈ open_interval (minus_SNo M) M.
We prove the intermediate claim Happ: apply_fun fid n = n.
An exact proof term for the current goal is (identity_function_apply ω n (omega_ordsucc n0 Hn0)).
We prove the intermediate claim HnR: n ∈ R.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n0 Hn0).
We prove the intermediate claim HnSNoS: n ∈ SNoS_ ω.
An exact proof term for the current goal is (omega_SNoS_omega n HnO).
An exact proof term for the current goal is (SNoS_omega_real n HnSNoS).
We prove the intermediate claim HRltMn: Rlt M n.
An exact proof term for the current goal is (RltI M n HM HnR HMltS).
We prove the intermediate claim HnotnM: ¬ (Rlt n M).
An exact proof term for the current goal is (not_Rlt_sym M n HRltMn).
We prove the intermediate claim Hprop: Rlt (minus_SNo M) (apply_fun fid n) ∧ Rlt (apply_fun fid n) M.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (minus_SNo M) x0 ∧ Rlt x0 M) (apply_fun fid n) Hin).
We prove the intermediate claim HRltnM: Rlt n M.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is (andER (Rlt (minus_SNo M) (apply_fun fid n)) (Rlt (apply_fun fid n) M) Hprop).
An exact proof term for the current goal is (HnotnM HRltnM).
An exact proof term for the current goal is (Hor (∃n : set, n ∈ ω ∧ ¬ (apply_fun fid n ∈ open_interval (minus_SNo M) M)) Hcase1 Hcase2).
We prove the intermediate claim HfidU: fid ∈ unbounded_sequences_Romega.
An exact proof term for the current goal is (SepI R_omega_space (λf : set ⇒ unbounded_sequence_Romega f) fid Hfid Huseq).
We prove the intermediate claim HeqE: Empty = unbounded_sequences_Romega.
Use symmetry.
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hsubst: ∀S T : set, S = T → fid ∈ T → fid ∈ S.
Let S and T be given.
Assume HeqST: S = T.
Assume HfidT: fid ∈ T.
We will prove fid ∈ S.
rewrite the current goal using HeqST (from left to right).
An exact proof term for the current goal is HfidT.
We prove the intermediate claim HfidE: fid ∈ Empty.
An exact proof term for the current goal is (Hsubst Empty unbounded_sequences_Romega HeqE HfidU).
An exact proof term for the current goal is (EmptyE fid HfidE).
∎