Let b be given.
Assume HbR: b ∈ R.
Assume Hnlt1: ¬ (Rlt 1 b).
Assume Hm1ltb: Rlt (minus_SNo 1) b.
We will prove preimage_of R bounded_transform_phi (open_ray_lower R b) ∈ R_standard_topology.
Apply xm (b = 1) to the current goal.
Assume HbEq: b = 1.
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 will prove t ∈ preimage_of R bounded_transform_phi (open_ray_lower R b).
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 Hlt1: Rlt (apply_fun bounded_transform_phi t) 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t)) (Rlt (apply_fun bounded_transform_phi t) 1) Hbounds).
We prove the intermediate claim HltB: Rlt (apply_fun bounded_transform_phi t) b.
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is Hlt1.
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 HltB).
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 HbNeq: ¬ (b = 1).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HbLt1: Rlt b 1.
Apply (SNoLt_trichotomy_or_impred 1 b SNo_1 HbS (Rlt b 1)) to the current goal.
Assume H1ltbS: 1 < b.
Apply FalseE to the current goal.
We prove the intermediate claim H1ltb: Rlt 1 b.
An exact proof term for the current goal is (RltI 1 b real_1 HbR H1ltbS).
An exact proof term for the current goal is (Hnlt1 H1ltb).
Assume Heq: 1 = b.
Apply FalseE to the current goal.
We prove the intermediate claim Hb1: b = 1.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (HbNeq Hb1).
Assume Hblt1S: b < 1.
An exact proof term for the current goal is (RltI b 1 HbR real_1 Hblt1S).
An exact proof term for the current goal is (bounded_transform_phi_preimage_open_ray_lower_strict_mid b HbR Hm1ltb HbLt1).
∎