Let b be given.
Assume HbR: b ∈ R.
We will prove preimage_of R bounded_transform_phi (open_ray_lower R b) ∈ R_standard_topology.
Apply xm (Rlt 1 b) to the current goal.
Assume H1ltb: Rlt 1 b.
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_lower R b) = R.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R bounded_transform_phi (open_ray_lower R b).
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_lower R b) 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 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 Hle: Rle (apply_fun bounded_transform_phi t) 1.
An exact proof term for the current goal is (RleI (apply_fun bounded_transform_phi t) 1 HfR real_1 Hnlt1f).
We prove the intermediate claim Hlt: Rlt (apply_fun bounded_transform_phi t) b.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun bounded_transform_phi t) 1 b Hle H1ltb).
We prove the intermediate claim Hrel: order_rel R (apply_fun bounded_transform_phi t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun bounded_transform_phi t) b Hlt).
We prove the intermediate claim HftRay: apply_fun bounded_transform_phi t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λx : set ⇒ order_rel R x b) (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_lower R b) 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 Hnlt1: ¬ (Rlt 1 b).
Apply xm (Rlt (minus_SNo 1) b) to the current goal.
Assume Hm1ltb: Rlt (minus_SNo 1) b.
An exact proof term for the current goal is (bounded_transform_phi_preimage_open_ray_lower_mid b HbR Hnlt1 Hm1ltb).
Assume Hnltm1: ¬ (Rlt (minus_SNo 1) b).
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_lower R b) = Empty.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R bounded_transform_phi (open_ray_lower R b).
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_lower R b) 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 Hnltm1f: ¬ (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 HfaRay: apply_fun bounded_transform_phi t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_lower R b) t HtPre).
We prove the intermediate claim Hrel: order_rel R (apply_fun bounded_transform_phi t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun bounded_transform_phi t) HfaRay).
We prove the intermediate claim Hlt: Rlt (apply_fun bounded_transform_phi t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun bounded_transform_phi t) b Hrel).
We prove the intermediate claim HbLe: Rle b (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).
An exact proof term for the current goal is (RleI b (minus_SNo 1) HbR Hm1R Hnltm1).
We prove the intermediate claim Hltm1: Rlt (apply_fun bounded_transform_phi t) (minus_SNo 1).
An exact proof term for the current goal is (Rlt_Rle_tra (apply_fun bounded_transform_phi t) b (minus_SNo 1) Hlt HbLe).
An exact proof term for the current goal is (Hnltm1f Hltm1).
Let t be given.
Assume HtE: t ∈ Empty.
We will prove t ∈ preimage_of R bounded_transform_phi (open_ray_lower R b).
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).
∎