Let X, Tx, Y, f, a, b and r be given.
Assume Hconn: connected_space X Tx.
Assume HsoY: simply_ordered_set Y.
Assume Hcont: continuous_map X Tx Y (order_topology Y) f.
Assume Ha: a ∈ X.
Assume Hb: b ∈ X.
Assume Hr: r ∈ Y.
Assume Hbetw: between_in_order Y (apply_fun f a) r (apply_fun f b).
We will prove ∃c : set, c ∈ X ∧ apply_fun f c = r.
Set Im to be the term image_of f X.
Set Tim to be the term subspace_topology Y (order_topology Y) Im.
We prove the intermediate claim HImconn: connected_space Im Tim.
An exact proof term for the current goal is (continuous_image_connected X Tx Y (order_topology Y) f Hconn Hcont).
Apply (Hbetw (∃c : set, c ∈ X ∧ apply_fun f c = r)) to the current goal.
Assume Hcases1: ((order_rel Y (apply_fun f a) r ∧ order_rel Y r (apply_fun f b)) ∨ (order_rel Y (apply_fun f b) r ∧ order_rel Y r (apply_fun f a))) ∨ r = apply_fun f a.
Apply (Hcases1 (∃c : set, c ∈ X ∧ apply_fun f c = r)) to the current goal.
Assume Hstrict: (order_rel Y (apply_fun f a) r ∧ order_rel Y r (apply_fun f b)) ∨ (order_rel Y (apply_fun f b) r ∧ order_rel Y r (apply_fun f a)).
We prove the intermediate claim HrIm: r ∈ Im.
Apply (xm (r ∈ Im)) to the current goal.
Assume HrIm.
An exact proof term for the current goal is HrIm.
Assume HrnotIm: r ∉ Im.
We prove the intermediate claim HXsubX: X ⊆ X.
Let x be given.
Assume Hx: x ∈ X.
An exact proof term for the current goal is Hx.
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y (order_topology Y) f Hcont).
We prove the intermediate claim HImsubY: Im ⊆ Y.
An exact proof term for the current goal is (image_of_sub_codomain f X Y X Hfun HXsubX).
Set Lray to be the term open_ray_lower Y r.
Set Uray to be the term open_ray_upper Y r.
We prove the intermediate claim HLsub: open_rays_subbasis Y ⊆ order_topology Y.
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology Y HsoY).
We prove the intermediate claim HLraySub: Lray ∈ open_rays_subbasis Y.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis Y r Hr).
We prove the intermediate claim HUraySub: Uray ∈ open_rays_subbasis Y.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis Y r Hr).
We prove the intermediate claim HLrayOpen: Lray ∈ order_topology Y.
An exact proof term for the current goal is (HLsub Lray HLraySub).
We prove the intermediate claim HUrayOpen: Uray ∈ order_topology Y.
An exact proof term for the current goal is (HLsub Uray HUraySub).
Set U to be the term Lray ∩ Im.
Set V to be the term Uray ∩ Im.
We prove the intermediate claim HUinTim: U ∈ Tim.
An exact proof term for the current goal is (subspace_topologyI Y (order_topology Y) Im Lray HLrayOpen).
We prove the intermediate claim HVinTim: V ∈ Tim.
An exact proof term for the current goal is (subspace_topologyI Y (order_topology Y) Im Uray HUrayOpen).
We prove the intermediate claim HsepUV: separation_of Im U V.
We prove the intermediate claim HUsubIm: U ⊆ Im.
An exact proof term for the current goal is (binintersect_Subq_2 Lray Im).
We prove the intermediate claim HVsubIm: V ⊆ Im.
An exact proof term for the current goal is (binintersect_Subq_2 Uray Im).
We prove the intermediate claim HUpowIm: U ∈ 𝒫 Im.
An exact proof term for the current goal is (PowerI Im U HUsubIm).
We prove the intermediate claim HVpowIm: V ∈ 𝒫 Im.
An exact proof term for the current goal is (PowerI Im V HVsubIm).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
Apply Empty_eq to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ V.
Apply (binintersectE U V y Hy) to the current goal.
Assume HyU: y ∈ U.
Assume HyV: y ∈ V.
We prove the intermediate claim HyIm: y ∈ Im.
An exact proof term for the current goal is (binintersectE2 Lray Im y HyU).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (HImsubY y HyIm).
We prove the intermediate claim HyL: y ∈ Lray.
An exact proof term for the current goal is (binintersectE1 Lray Im y HyU).
We prove the intermediate claim HyUray: y ∈ Uray.
An exact proof term for the current goal is (binintersectE1 Uray Im y HyV).
We prove the intermediate claim Hyr: order_rel Y y r.
An exact proof term for the current goal is (SepE2 Y (λx0 : set ⇒ order_rel Y x0 r) y HyL).
We prove the intermediate claim Hry: order_rel Y r y.
An exact proof term for the current goal is (SepE2 Y (λx0 : set ⇒ order_rel Y r x0) y HyUray).
We prove the intermediate claim Hyy: order_rel Y y y.
An exact proof term for the current goal is (order_rel_trans Y y r y HsoY HyY Hr HyY Hyr Hry).
Apply FalseE to the current goal.
An exact proof term for the current goal is ((order_rel_irref Y y) Hyy).
We prove the intermediate claim HUne: U ≠ Empty.
Apply (Hstrict (U ≠ Empty)) to the current goal.
Assume Hlr: order_rel Y (apply_fun f a) r ∧ order_rel Y r (apply_fun f b).
We prove the intermediate claim Hfar: order_rel Y (apply_fun f a) r.
An exact proof term for the current goal is (andEL (order_rel Y (apply_fun f a) r) (order_rel Y r (apply_fun f b)) Hlr).
We prove the intermediate claim HfaIm: apply_fun f a ∈ Im.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun f x0) a Ha).
We prove the intermediate claim HfaY: apply_fun f a ∈ Y.
An exact proof term for the current goal is (HImsubY (apply_fun f a) HfaIm).
We prove the intermediate claim HfaL: apply_fun f a ∈ Lray.
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel Y x0 r) (apply_fun f a) HfaY Hfar).
We prove the intermediate claim HfaU: apply_fun f a ∈ U.
An exact proof term for the current goal is (binintersectI Lray Im (apply_fun f a) HfaL HfaIm).
An exact proof term for the current goal is (elem_implies_nonempty U (apply_fun f a) HfaU).
Assume Hrl: order_rel Y (apply_fun f b) r ∧ order_rel Y r (apply_fun f a).
We prove the intermediate claim Hfbr: order_rel Y (apply_fun f b) r.
An exact proof term for the current goal is (andEL (order_rel Y (apply_fun f b) r) (order_rel Y r (apply_fun f a)) Hrl).
We prove the intermediate claim HfbIm: apply_fun f b ∈ Im.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun f x0) b Hb).
We prove the intermediate claim HfbY: apply_fun f b ∈ Y.
An exact proof term for the current goal is (HImsubY (apply_fun f b) HfbIm).
We prove the intermediate claim HfbL: apply_fun f b ∈ Lray.
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel Y x0 r) (apply_fun f b) HfbY Hfbr).
We prove the intermediate claim HfbU: apply_fun f b ∈ U.
An exact proof term for the current goal is (binintersectI Lray Im (apply_fun f b) HfbL HfbIm).
An exact proof term for the current goal is (elem_implies_nonempty U (apply_fun f b) HfbU).
We prove the intermediate claim HVne: V ≠ Empty.
Apply (Hstrict (V ≠ Empty)) to the current goal.
Assume Hlr: order_rel Y (apply_fun f a) r ∧ order_rel Y r (apply_fun f b).
We prove the intermediate claim Hrfb: order_rel Y r (apply_fun f b).
An exact proof term for the current goal is (andER (order_rel Y (apply_fun f a) r) (order_rel Y r (apply_fun f b)) Hlr).
We prove the intermediate claim HfbIm: apply_fun f b ∈ Im.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun f x0) b Hb).
We prove the intermediate claim HfbY: apply_fun f b ∈ Y.
An exact proof term for the current goal is (HImsubY (apply_fun f b) HfbIm).
We prove the intermediate claim HfbUray: apply_fun f b ∈ Uray.
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel Y r x0) (apply_fun f b) HfbY Hrfb).
We prove the intermediate claim HfbV: apply_fun f b ∈ V.
An exact proof term for the current goal is (binintersectI Uray Im (apply_fun f b) HfbUray HfbIm).
An exact proof term for the current goal is (elem_implies_nonempty V (apply_fun f b) HfbV).
Assume Hrl: order_rel Y (apply_fun f b) r ∧ order_rel Y r (apply_fun f a).
We prove the intermediate claim Hrfa: order_rel Y r (apply_fun f a).
An exact proof term for the current goal is (andER (order_rel Y (apply_fun f b) r) (order_rel Y r (apply_fun f a)) Hrl).
We prove the intermediate claim HfaIm: apply_fun f a ∈ Im.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun f x0) a Ha).
We prove the intermediate claim HfaY: apply_fun f a ∈ Y.
An exact proof term for the current goal is (HImsubY (apply_fun f a) HfaIm).
We prove the intermediate claim HfaUray: apply_fun f a ∈ Uray.
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel Y r x0) (apply_fun f a) HfaY Hrfa).
We prove the intermediate claim HfaV: apply_fun f a ∈ V.
An exact proof term for the current goal is (binintersectI Uray Im (apply_fun f a) HfaUray HfaIm).
An exact proof term for the current goal is (elem_implies_nonempty V (apply_fun f a) HfaV).
We prove the intermediate claim Hunion: U ∪ V = Im.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∪ V.
We will prove y ∈ Im.
Apply (binunionE U V y Hy) to the current goal.
Assume HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE2 Lray Im y HyU).
Assume HyV: y ∈ V.
An exact proof term for the current goal is (binintersectE2 Uray Im y HyV).
Let y be given.
Assume HyIm: y ∈ Im.
We will prove y ∈ U ∪ V.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (HImsubY y HyIm).
Apply (order_rel_trichotomy_or_impred Y y r HsoY HyY Hr (y ∈ U ∪ V)) to the current goal.
Assume Hyr: order_rel Y y r.
Apply (binunionI1 U V y) to the current goal.
We prove the intermediate claim HyL: y ∈ Lray.
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel Y x0 r) y HyY Hyr).
An exact proof term for the current goal is (binintersectI Lray Im y HyL HyIm).
Assume Heq: y = r.
Apply FalseE to the current goal.
We prove the intermediate claim HrIm0: r ∈ Im.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyIm.
An exact proof term for the current goal is (HrnotIm HrIm0).
Assume Hry: order_rel Y r y.
Apply (binunionI2 U V y) to the current goal.
We prove the intermediate claim HyUray: y ∈ Uray.
An exact proof term for the current goal is (SepI Y (λx0 : set ⇒ order_rel Y r x0) y HyY Hry).
An exact proof term for the current goal is (binintersectI Uray Im y HyUray HyIm).
We will prove U ∈ 𝒫 Im ∧ V ∈ 𝒫 Im ∧ U ∩ V = Empty ∧ U ≠ Empty ∧ V ≠ Empty ∧ U ∪ V = Im.
Apply and6I to the current goal.
An exact proof term for the current goal is HUpowIm.
An exact proof term for the current goal is HVpowIm.
An exact proof term for the current goal is Hdisj.
An exact proof term for the current goal is HUne.
An exact proof term for the current goal is HVne.
An exact proof term for the current goal is Hunion.
Apply FalseE to the current goal.
We prove the intermediate claim Hnosep: ¬ (∃U0 V0 : set, U0 ∈ Tim ∧ V0 ∈ Tim ∧ separation_of Im U0 V0).
An exact proof term for the current goal is (connected_space_no_separation Im Tim HImconn).
Apply Hnosep to the current goal.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUinTim.
An exact proof term for the current goal is HVinTim.
An exact proof term for the current goal is HsepUV.
Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) r HrIm (∃c : set, c ∈ X ∧ apply_fun f c = r)) to the current goal.
Let c be given.
Assume HcX: c ∈ X.
Assume Hreq: r = apply_fun f c.
We use c to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HcX.
Use symmetry.
An exact proof term for the current goal is Hreq.
Assume HrEqFa: r = apply_fun f a.
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
rewrite the current goal using HrEqFa (from right to left).
Use reflexivity.
Assume HrEqFb: r = apply_fun f b.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
rewrite the current goal using HrEqFb (from right to left).
Use reflexivity.
∎