Let a be given.
Assume HaR: a ∈ R.
Assume Hnltm1: ¬ (Rlt a (minus_SNo 1)).
Assume Halt1: Rlt a 1.
We will prove preimage_of R bounded_transform_phi (open_ray_upper R a) ∈ R_standard_topology.
Apply xm (a = minus_SNo 1) to the current goal.
Assume HaEq: a = minus_SNo 1.
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_upper R a) = R.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R bounded_transform_phi (open_ray_upper R a).
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_upper R a) t HtPre).
Let t be given.
Assume HtR: t ∈ R.
We will prove t ∈ preimage_of R bounded_transform_phi (open_ray_upper R a).
We prove the intermediate claim HfR: apply_fun bounded_transform_phi t ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R t HtR).
We prove the intermediate claim Hbounds: Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t) ∧ Rlt (apply_fun bounded_transform_phi t) 1.
An exact proof term for the current goal is (bounded_transform_phi_strict_bounds t HtR).
We prove the intermediate claim Hm1lt: Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (andEL (Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t)) (Rlt (apply_fun bounded_transform_phi t) 1) Hbounds).
We prove the intermediate claim HltA: Rlt a (apply_fun bounded_transform_phi t).
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is Hm1lt.
We prove the intermediate claim Hrel: order_rel R a (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun bounded_transform_phi t) HltA).
We prove the intermediate claim HftRay: apply_fun bounded_transform_phi t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepI R (λx : set ⇒ order_rel R a x) (apply_fun bounded_transform_phi t) HfR Hrel).
An exact proof term for the current goal is (SepI R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_upper R a) t HtR HftRay).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_has_X R R_standard_topology R_standard_topology_is_topology).
Assume HaNeq: ¬ (a = minus_SNo 1).
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 HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hm1lta: Rlt (minus_SNo 1) a.
Apply (SNoLt_trichotomy_or_impred a (minus_SNo 1) HaS Hm1S (Rlt (minus_SNo 1) a)) to the current goal.
Assume Halt: a < minus_SNo 1.
Apply FalseE to the current goal.
We prove the intermediate claim HaltR: Rlt a (minus_SNo 1).
An exact proof term for the current goal is (RltI a (minus_SNo 1) HaR Hm1R Halt).
An exact proof term for the current goal is (Hnltm1 HaltR).
Assume Heq: a = minus_SNo 1.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HaNeq Heq).
Assume Hgt: minus_SNo 1 < a.
An exact proof term for the current goal is (RltI (minus_SNo 1) a Hm1R HaR Hgt).
An exact proof term for the current goal is (bounded_transform_phi_preimage_open_ray_upper_strict_mid a HaR Hm1lta Halt1).
∎