Let a be given.
Assume HaR: a ∈ R.
We will prove preimage_of R bounded_transform_phi (open_ray_upper R a) ∈ R_standard_topology.
Apply xm (Rlt a (minus_SNo 1)) to the current goal.
Assume Haltm1: Rlt 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 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 HfCI: apply_fun bounded_transform_phi t ∈ closed_interval (minus_SNo 1) 1.
An exact proof term for the current goal is (bounded_transform_phi_range_in_closed_interval_minus1_1 t HtR).
We prove the intermediate claim Hbounds: ¬ (Rlt (apply_fun bounded_transform_phi t) (minus_SNo 1)) ∧ ¬ (Rlt 1 (apply_fun bounded_transform_phi t)).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 (minus_SNo 1)) ∧ ¬ (Rlt 1 x0)) (apply_fun bounded_transform_phi t) HfCI).
We prove the intermediate claim Hnlt: ¬ (Rlt (apply_fun bounded_transform_phi t) (minus_SNo 1)).
An exact proof term for the current goal is (andEL (¬ (Rlt (apply_fun bounded_transform_phi t) (minus_SNo 1))) (¬ (Rlt 1 (apply_fun bounded_transform_phi t))) Hbounds).
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 Hm1le: Rle (minus_SNo 1) (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (RleI (minus_SNo 1) (apply_fun bounded_transform_phi t) Hm1R HfR Hnlt).
We prove the intermediate claim Haltf: Rlt a (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (Rlt_Rle_tra a (minus_SNo 1) (apply_fun bounded_transform_phi t) Haltm1 Hm1le).
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) Haltf).
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 Hnltm1: ¬ (Rlt a (minus_SNo 1)).
Apply xm (Rlt a 1) to the current goal.
Assume Halt1: Rlt a 1.
An exact proof term for the current goal is (bounded_transform_phi_preimage_open_ray_upper_mid a HaR Hnltm1 Halt1).
Assume Hnlt1: ¬ (Rlt a 1).
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_upper R a) = Empty.
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).
We will prove t ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HtR: t ∈ R.
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).
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 HfCI: apply_fun bounded_transform_phi t ∈ closed_interval (minus_SNo 1) 1.
An exact proof term for the current goal is (bounded_transform_phi_range_in_closed_interval_minus1_1 t HtR).
We prove the intermediate claim Hbounds: ¬ (Rlt (apply_fun bounded_transform_phi t) (minus_SNo 1)) ∧ ¬ (Rlt 1 (apply_fun bounded_transform_phi t)).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 (minus_SNo 1)) ∧ ¬ (Rlt 1 x0)) (apply_fun bounded_transform_phi t) HfCI).
We prove the intermediate claim Hnlt1f: ¬ (Rlt 1 (apply_fun bounded_transform_phi t)).
An exact proof term for the current goal is (andER (¬ (Rlt (apply_fun bounded_transform_phi t) (minus_SNo 1))) (¬ (Rlt 1 (apply_fun bounded_transform_phi t))) Hbounds).
We prove the intermediate claim HfaRay: apply_fun bounded_transform_phi t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_upper R a) t HtPre).
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 (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun bounded_transform_phi t) HfaRay).
We prove the intermediate claim Haltf: Rlt a (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun bounded_transform_phi t) Hrel).
We prove the intermediate claim Hle1A: Rle 1 a.
An exact proof term for the current goal is (RleI 1 a real_1 HaR Hnlt1).
We prove the intermediate claim H1ltf: Rlt 1 (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (Rle_Rlt_tra 1 a (apply_fun bounded_transform_phi t) Hle1A Haltf).
An exact proof term for the current goal is (Hnlt1f H1ltf).
Let t be given.
Assume HtE: t ∈ Empty.
We will prove t ∈ preimage_of R bounded_transform_phi (open_ray_upper R a).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE t HtE).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_has_empty R R_standard_topology R_standard_topology_is_topology).
∎