Let b be given.
Assume HbR: b ∈ R.
We will prove preimage_of (open_interval (minus_SNo 1) 1) bounded_transform_psi (open_ray_lower R b) ∈ subspace_topology R R_standard_topology (open_interval (minus_SNo 1) 1).
Set I to be the term open_interval (minus_SNo 1) 1.
Set U to be the term preimage_of I bounded_transform_psi (open_ray_lower R b).
We prove the intermediate claim HI_sub_R: I ⊆ R.
Let x be given.
Assume HxI: x ∈ I.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) x HxI).
Set mb to be the term minus_SNo b.
We prove the intermediate claim HmbR: mb ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
Set V to be the term preimage_of I bounded_transform_psi (open_ray_upper R mb).
We prove the intermediate claim HVopen: V ∈ subspace_topology R R_standard_topology I.
An exact proof term for the current goal is (bounded_transform_psi_preimage_open_ray_upper mb HmbR).
Set Ti to be the term subspace_topology R R_standard_topology I.
We prove the intermediate claim HnegcontR: continuous_map R R_standard_topology R R_standard_topology neg_fun.
An exact proof term for the current goal is neg_fun_continuous.
We prove the intermediate claim HnegcontI_R: continuous_map I Ti R R_standard_topology neg_fun.
An exact proof term for the current goal is (continuous_on_subspace R R_standard_topology R R_standard_topology neg_fun I R_standard_topology_is_topology HI_sub_R HnegcontR).
We prove the intermediate claim HnegImgI: ∀x : set, x ∈ I → apply_fun neg_fun x ∈ I.
Let x be given.
Assume HxI: x ∈ I.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (HI_sub_R x HxI).
We prove the intermediate claim HnegEq: apply_fun neg_fun x = minus_SNo x.
An exact proof term for the current goal is (neg_fun_apply x HxR).
rewrite the current goal using HnegEq (from left to right).
An exact proof term for the current goal is (neg_closed_open_interval_minus1_1 x HxI).
We prove the intermediate claim HnegcontI_I: continuous_map I Ti I Ti neg_fun.
An exact proof term for the current goal is (continuous_map_range_restrict I Ti R R_standard_topology neg_fun I HnegcontI_R HI_sub_R HnegImgI).
We prove the intermediate claim Heq: U = preimage_of I neg_fun V.
Apply set_ext to the current goal.
Let s be given.
Assume HsU: s ∈ U.
We will prove s ∈ preimage_of I neg_fun V.
We prove the intermediate claim HsI: s ∈ I.
An exact proof term for the current goal is (SepE1 I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_lower R b) s HsU).
We prove the intermediate claim HpsiLower: apply_fun bounded_transform_psi s ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_lower R b) s HsU).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (HI_sub_R s HsI).
We prove the intermediate claim HnegS: apply_fun neg_fun s = minus_SNo s.
An exact proof term for the current goal is (neg_fun_apply s HsR).
We prove the intermediate claim HmsI: minus_SNo s ∈ I.
An exact proof term for the current goal is (neg_closed_open_interval_minus1_1 s HsI).
We prove the intermediate claim HpsR: apply_fun bounded_transform_psi s ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun bounded_transform_psi s) HpsiLower).
We prove the intermediate claim HpreEq0: preimage_of R neg_fun (open_ray_upper R mb) = open_ray_lower R (minus_SNo mb).
An exact proof term for the current goal is (preimage_neg_fun_open_ray_upper mb HmbR).
We prove the intermediate claim HpreEq: preimage_of R neg_fun (open_ray_upper R mb) = open_ray_lower R b.
We prove the intermediate claim HmbDef: mb = minus_SNo b.
Use reflexivity.
We prove the intermediate claim HmmbEq: minus_SNo mb = b.
rewrite the current goal using HmbDef (from left to right).
An exact proof term for the current goal is (minus_SNo_invol b (real_SNo b HbR)).
rewrite the current goal using HpreEq0 (from left to right).
rewrite the current goal using HmmbEq (from left to right).
Use reflexivity.
We prove the intermediate claim HpsPre: apply_fun bounded_transform_psi s ∈ preimage_of R neg_fun (open_ray_upper R mb).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is HpsiLower.
We prove the intermediate claim HnegPs: apply_fun neg_fun (apply_fun bounded_transform_psi s) ∈ open_ray_upper R mb.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun neg_fun x0 ∈ open_ray_upper R mb) (apply_fun bounded_transform_psi s) HpsPre).
We prove the intermediate claim HnegPsEq: apply_fun neg_fun (apply_fun bounded_transform_psi s) = minus_SNo (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (neg_fun_apply (apply_fun bounded_transform_psi s) HpsR).
We prove the intermediate claim HpsiOdd: apply_fun bounded_transform_psi (minus_SNo s) = minus_SNo (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (bounded_transform_psi_odd_open_interval s HsI).
We prove the intermediate claim HpsiUpper: apply_fun bounded_transform_psi (minus_SNo s) ∈ open_ray_upper R mb.
rewrite the current goal using HpsiOdd (from left to right).
rewrite the current goal using HnegPsEq (from right to left).
An exact proof term for the current goal is HnegPs.
We prove the intermediate claim HmSinV2: (minus_SNo s) ∈ V.
An exact proof term for the current goal is (SepI I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_upper R mb) (minus_SNo s) HmsI HpsiUpper).
We prove the intermediate claim HpreNegDef: preimage_of I neg_fun V = {x0 ∈ I|apply_fun neg_fun x0 ∈ V}.
Use reflexivity.
rewrite the current goal using HpreNegDef (from left to right).
Apply (SepI I (λx0 : set ⇒ apply_fun neg_fun x0 ∈ V) s HsI) to the current goal.
rewrite the current goal using HnegS (from left to right).
An exact proof term for the current goal is HmSinV2.
Let s be given.
Assume HsPre: s ∈ preimage_of I neg_fun V.
We will prove s ∈ U.
We prove the intermediate claim HsI: s ∈ I.
An exact proof term for the current goal is (SepE1 I (λx0 : set ⇒ apply_fun neg_fun x0 ∈ V) s HsPre).
We prove the intermediate claim HnegInV: apply_fun neg_fun s ∈ V.
An exact proof term for the current goal is (SepE2 I (λx0 : set ⇒ apply_fun neg_fun x0 ∈ V) s HsPre).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (HI_sub_R s HsI).
We prove the intermediate claim HnegS: apply_fun neg_fun s = minus_SNo s.
An exact proof term for the current goal is (neg_fun_apply s HsR).
We prove the intermediate claim HmsI: minus_SNo s ∈ I.
An exact proof term for the current goal is (neg_closed_open_interval_minus1_1 s HsI).
We prove the intermediate claim HmSinV: (minus_SNo s) ∈ V.
rewrite the current goal using HnegS (from right to left).
An exact proof term for the current goal is HnegInV.
We prove the intermediate claim HpsiUpper: apply_fun bounded_transform_psi (minus_SNo s) ∈ open_ray_upper R mb.
An exact proof term for the current goal is (SepE2 I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_upper R mb) (minus_SNo s) HmSinV).
We prove the intermediate claim HpsiOdd: apply_fun bounded_transform_psi (minus_SNo s) = minus_SNo (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (bounded_transform_psi_odd_open_interval s HsI).
We prove the intermediate claim HnegPs: minus_SNo (apply_fun bounded_transform_psi s) ∈ open_ray_upper R mb.
rewrite the current goal using HpsiOdd (from right to left).
An exact proof term for the current goal is HpsiUpper.
We prove the intermediate claim HpsiMsR: apply_fun bounded_transform_psi (minus_SNo s) ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R mb x0) (apply_fun bounded_transform_psi (minus_SNo s)) HpsiUpper).
We prove the intermediate claim HpsiOdd2: apply_fun bounded_transform_psi s = minus_SNo (apply_fun bounded_transform_psi (minus_SNo s)).
We prove the intermediate claim Hraw: apply_fun bounded_transform_psi (minus_SNo (minus_SNo s)) = minus_SNo (apply_fun bounded_transform_psi (minus_SNo s)).
An exact proof term for the current goal is (bounded_transform_psi_odd_open_interval (minus_SNo s) HmsI).
rewrite the current goal using (minus_SNo_invol s (real_SNo s HsR)) (from right to left) at position 1.
An exact proof term for the current goal is Hraw.
We prove the intermediate claim HminusPsiMsR: minus_SNo (apply_fun bounded_transform_psi (minus_SNo s)) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun bounded_transform_psi (minus_SNo s)) HpsiMsR).
We prove the intermediate claim HpsR: apply_fun bounded_transform_psi s ∈ R.
rewrite the current goal using HpsiOdd2 (from left to right).
An exact proof term for the current goal is HminusPsiMsR.
We prove the intermediate claim HnegPsEq: apply_fun neg_fun (apply_fun bounded_transform_psi s) = minus_SNo (apply_fun bounded_transform_psi s).
An exact proof term for the current goal is (neg_fun_apply (apply_fun bounded_transform_psi s) HpsR).
We prove the intermediate claim HnegPs2: apply_fun neg_fun (apply_fun bounded_transform_psi s) ∈ open_ray_upper R mb.
rewrite the current goal using HnegPsEq (from left to right).
An exact proof term for the current goal is HnegPs.
We prove the intermediate claim HpreEq0: preimage_of R neg_fun (open_ray_upper R mb) = open_ray_lower R (minus_SNo mb).
An exact proof term for the current goal is (preimage_neg_fun_open_ray_upper mb HmbR).
We prove the intermediate claim HpreEq: preimage_of R neg_fun (open_ray_upper R mb) = open_ray_lower R b.
We prove the intermediate claim HmbDef: mb = minus_SNo b.
Use reflexivity.
We prove the intermediate claim HmmbEq: minus_SNo mb = b.
rewrite the current goal using HmbDef (from left to right).
An exact proof term for the current goal is (minus_SNo_invol b (real_SNo b HbR)).
rewrite the current goal using HpreEq0 (from left to right).
rewrite the current goal using HmmbEq (from left to right).
Use reflexivity.
We prove the intermediate claim HpsPre: apply_fun bounded_transform_psi s ∈ preimage_of R neg_fun (open_ray_upper R mb).
Set P to be the term (λx0 : set ⇒ apply_fun neg_fun x0 ∈ open_ray_upper R mb).
An exact proof term for the current goal is (SepI R P (apply_fun bounded_transform_psi s) HpsR HnegPs2).
We prove the intermediate claim HpsiLower: apply_fun bounded_transform_psi s ∈ open_ray_lower R b.
rewrite the current goal using HpreEq (from right to left).
An exact proof term for the current goal is HpsPre.
An exact proof term for the current goal is (SepI I (λx0 : set ⇒ apply_fun bounded_transform_psi x0 ∈ open_ray_lower R b) s HsI HpsiLower).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage I Ti I Ti neg_fun HnegcontI_I V HVopen).
∎