Let X, x and y be given.
Assume Hwo: well_ordered_set X.
Assume Hso: simply_ordered_set X.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Hxy: order_rel X x y.
Set I to be the term order_interval_right_closed X x y.
Set J to be the term order_interval X x (ordsucc y).
We prove the intermediate claim HIeq: I = J.
Apply set_ext to the current goal.
Let z be given.
Assume HzI: z ∈ I.
We will prove z ∈ J.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x z0 ∧ (z0 = y ∨ order_rel X z0 y)) z HzI).
We prove the intermediate claim Hzconj: order_rel X x z ∧ (z = y ∨ order_rel X z y).
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X x z0 ∧ (z0 = y ∨ order_rel X z0 y)) z HzI).
We prove the intermediate claim Hxz: order_rel X x z.
An exact proof term for the current goal is (andEL (order_rel X x z) (z = y ∨ order_rel X z y) Hzconj).
We prove the intermediate claim Hzcase: z = y ∨ order_rel X z y.
An exact proof term for the current goal is (andER (order_rel X x z) (z = y ∨ order_rel X z y) Hzconj).
We prove the intermediate claim HJdef: J = {z0 ∈ X|order_rel X x z0 ∧ order_rel X z0 (ordsucc y)}.
Use reflexivity.
rewrite the current goal using HJdef (from left to right).
Apply (SepI X (λz0 : set ⇒ order_rel X x z0 ∧ order_rel X z0 (ordsucc y)) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxz.
Apply Hzcase to the current goal.
Assume Hzy: z = y.
rewrite the current goal using Hzy (from left to right).
We prove the intermediate claim Hymem: y ∈ ordsucc y.
An exact proof term for the current goal is (ordsuccI2 y).
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X y (ordsucc y) Hwo Hymem).
Assume Hzy: order_rel X z y.
We prove the intermediate claim Hmem: z ∈ y.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem X z y Hwo Hzy).
We prove the intermediate claim Hzsucc: z ∈ ordsucc y.
An exact proof term for the current goal is (ordsuccI1 y z Hmem).
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X z (ordsucc y) Hwo Hzsucc).
Let z be given.
Assume HzJ: z ∈ J.
We will prove z ∈ I.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x z0 ∧ order_rel X z0 (ordsucc y)) z HzJ).
We prove the intermediate claim Hzconj: order_rel X x z ∧ order_rel X z (ordsucc y).
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X x z0 ∧ order_rel X z0 (ordsucc y)) z HzJ).
We prove the intermediate claim Hxz: order_rel X x z.
An exact proof term for the current goal is (andEL (order_rel X x z) (order_rel X z (ordsucc y)) Hzconj).
We prove the intermediate claim HzSucc: order_rel X z (ordsucc y).
An exact proof term for the current goal is (andER (order_rel X x z) (order_rel X z (ordsucc y)) Hzconj).
We prove the intermediate claim HmemSucc: z ∈ ordsucc y.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem X z (ordsucc y) Hwo HzSucc).
We prove the intermediate claim Hzcase: z ∈ y ∨ z = y.
An exact proof term for the current goal is (ordsuccE y z HmemSucc).
We prove the intermediate claim HIdef: I = {z0 ∈ X|order_rel X x z0 ∧ (z0 = y ∨ order_rel X z0 y)}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
Apply (SepI X (λz0 : set ⇒ order_rel X x z0 ∧ (z0 = y ∨ order_rel X z0 y)) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxz.
Apply Hzcase to the current goal.
Assume Hzy: z ∈ y.
Apply orIR to the current goal.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X z y Hwo Hzy).
Assume Hzy: z = y.
Apply orIL to the current goal.
An exact proof term for the current goal is Hzy.
We prove the intermediate claim HordX: ordinal X.
An exact proof term for the current goal is (well_ordered_set_is_ordinal X Hwo).
We prove the intermediate claim HsuccCase: ordsucc y ∈ X ∨ X = ordsucc y.
An exact proof term for the current goal is (ordinal_ordsucc_In_eq X y HordX HyX).
Apply HsuccCase to the current goal.
Assume HsuccIn: ordsucc y ∈ X.
We prove the intermediate claim HJinB: J ∈ order_topology_basis X.
Set F1 to be the term {I0 ∈ 𝒫 X|∃a ∈ X, ∃b ∈ X, I0 = {t ∈ X|order_rel X a t ∧ order_rel X t b}}.
Set F2 to be the term {I0 ∈ 𝒫 X|∃b ∈ X, I0 = {t ∈ X|order_rel X t b}}.
Set F3 to be the term {I0 ∈ 𝒫 X|∃a ∈ X, I0 = {t ∈ X|order_rel X a t}}.
Set F12 to be the term F1 ∪ F2.
Set F123 to be the term F12 ∪ F3.
We prove the intermediate claim HBdef: order_topology_basis X = F123 ∪ {X}.
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
We prove the intermediate claim HJpow: J ∈ 𝒫 X.
Apply PowerI to the current goal.
Let t be given.
Assume HtJ: t ∈ J.
An exact proof term for the current goal is (SepE1 X (λt0 : set ⇒ order_rel X x t0 ∧ order_rel X t0 (ordsucc y)) t HtJ).
We prove the intermediate claim Hex: ∃a ∈ X, ∃b ∈ X, J = {t ∈ X|order_rel X a t ∧ order_rel X t b}.
We use x to witness the existential quantifier.
We will prove x ∈ X ∧ ∃b ∈ X, J = {t ∈ X|order_rel X x t ∧ order_rel X t b}.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
We use (ordsucc y) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HsuccIn.
Use reflexivity.
We prove the intermediate claim HJfam: J ∈ F1.
An exact proof term for the current goal is (SepI (𝒫 X) (λI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {t ∈ X|order_rel X a t ∧ order_rel X t b}) J HJpow Hex).
We prove the intermediate claim HJinF123: J ∈ F123.
An exact proof term for the current goal is (binunionI1 F12 F3 J (binunionI1 F1 F2 J HJfam)).
An exact proof term for the current goal is (binunionI1 F123 {X} J HJinF123).
We prove the intermediate claim HJopen: J ∈ order_topology X.
We prove the intermediate claim HdefT: order_topology X = generated_topology X (order_topology_basis X).
Use reflexivity.
rewrite the current goal using HdefT (from left to right).
We prove the intermediate claim HJpow: J ∈ 𝒫 X.
Apply PowerI to the current goal.
Let t be given.
Assume HtJ: t ∈ J.
An exact proof term for the current goal is (SepE1 X (λt0 : set ⇒ order_rel X x t0 ∧ order_rel X t0 (ordsucc y)) t HtJ).
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) J HJpow HJinB).
rewrite the current goal using HIeq (from left to right).
An exact proof term for the current goal is HJopen.
Assume HsuccEq: X = ordsucc y.
We prove the intermediate claim HJray: J = open_ray_upper X x.
Apply set_ext to the current goal.
Let z be given.
Assume HzJ: z ∈ J.
We will prove z ∈ open_ray_upper X x.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x z0 ∧ order_rel X z0 (ordsucc y)) z HzJ).
We prove the intermediate claim Hxz: order_rel X x z.
An exact proof term for the current goal is (andEL (order_rel X x z) (order_rel X z (ordsucc y)) (SepE2 X (λz0 : set ⇒ order_rel X x z0 ∧ order_rel X z0 (ordsucc y)) z HzJ)).
An exact proof term for the current goal is (SepI X (λz0 : set ⇒ order_rel X x z0) z HzX Hxz).
Let z be given.
Assume HzU: z ∈ open_ray_upper X x.
We will prove z ∈ J.
We prove the intermediate claim HJdef: J = {z0 ∈ X|order_rel X x z0 ∧ order_rel X z0 (ordsucc y)}.
Use reflexivity.
rewrite the current goal using HJdef (from left to right).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x z0) z HzU).
We prove the intermediate claim Hxz: order_rel X x z.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X x z0) z HzU).
Apply (SepI X (λz0 : set ⇒ order_rel X x z0 ∧ order_rel X z0 (ordsucc y)) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxz.
rewrite the current goal using HsuccEq (from right to left).
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X z X Hwo HzX).
We prove the intermediate claim HrayB: open_ray_upper X x ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_upper_in_order_topology_basis X x HxX).
We prove the intermediate claim HrayPow: open_ray_upper X x ∈ 𝒫 X.
Apply PowerI to the current goal.
Let z be given.
Assume Hz: z ∈ open_ray_upper X x.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x z0) z Hz).
We prove the intermediate claim HrayOpen: open_ray_upper X x ∈ order_topology X.
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) (open_ray_upper X x) HrayPow HrayB).
rewrite the current goal using HIeq (from left to right).
rewrite the current goal using HJray (from left to right).
An exact proof term for the current goal is HrayOpen.
∎