Let k be given.
Assume HkO: k ∈ ω.
Set X to be the term setprod 2 ω.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (omega_nat_p k HkO).
Apply (nat_inv k HkNat ({(0,k)} ∈ order_topology X)) to the current goal.
Assume Hk0: k = 0.
rewrite the current goal using Hk0 (from left to right).
An exact proof term for the current goal is singleton_setprod_2_omega_00_open.
Assume Hex: ∃m : set, nat_p m ∧ k = ordsucc m.
Apply Hex to the current goal.
Let m be given.
Assume Hmconj: nat_p m ∧ k = ordsucc m.
We prove the intermediate claim HmNat: nat_p m.
An exact proof term for the current goal is (andEL (nat_p m) (k = ordsucc m) Hmconj).
We prove the intermediate claim HkEq: k = ordsucc m.
An exact proof term for the current goal is (andER (nat_p m) (k = ordsucc m) Hmconj).
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m HmNat).
We prove the intermediate claim HsuccKO: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkO).
Set a to be the term (0,m).
Set b to be the term (0,ordsucc k).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 m In_0_2 HmO).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 (ordsucc k) In_0_2 HsuccKO).
Set U to be the term {y ∈ X|order_rel X a y ∧ order_rel X y b}.
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
Apply PowerI X U to the current goal.
Let y be given.
Assume Hy: y ∈ U.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y Hy).
We prove the intermediate claim HUinB: U ∈ order_topology_basis X.
Set A to be the term {I ∈ 𝒫 X|∃a0 ∈ X, ∃b0 ∈ X, I = {y0 ∈ X|order_rel X a0 y0 ∧ order_rel X y0 b0}}.
Set B to be the term {I ∈ 𝒫 X|∃b0 ∈ X, I = {y0 ∈ X|order_rel X y0 b0}}.
Set C to be the term {I ∈ 𝒫 X|∃a0 ∈ X, I = {y0 ∈ X|order_rel X a0 y0}}.
Set Bold to be the term (A ∪ B ∪ C).
We prove the intermediate claim HUA: U ∈ A.
Apply (SepI (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, ∃b0 ∈ X, I = {y0 ∈ X|order_rel X a0 y0 ∧ order_rel X y0 b0}) U HUpow) to the current goal.
We use a to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HaX.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbX.
Use reflexivity.
We prove the intermediate claim HUAB: U ∈ (A ∪ B).
An exact proof term for the current goal is (binunionI1 A B U HUA).
We prove the intermediate claim HUbold: U ∈ Bold.
An exact proof term for the current goal is (binunionI1 (A ∪ B) C U HUAB).
We prove the intermediate claim HUdef: order_topology_basis X = (Bold ∪ {X}).
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (binunionI1 Bold {X} U HUbold).
We prove the intermediate claim HUopen: U ∈ order_topology X.
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) U HUpow HUinB).
We prove the intermediate claim HUeq: U = {(0,k)}.
Apply set_ext to the current goal.
Let y be given.
Assume HyU: y ∈ U.
We will prove y ∈ {(0,k)}.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y HyU).
We prove the intermediate claim Hya: order_rel X a y.
An exact proof term for the current goal is (andEL (order_rel X a y) (order_rel X y b) (SepE2 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y HyU)).
We prove the intermediate claim Hyb: order_rel X y b.
An exact proof term for the current goal is (andER (order_rel X a y) (order_rel X y b) (SepE2 X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) y HyU)).
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is simply_ordered_set_setprod_2_omega.
We prove the intermediate claim HkX: (0,k) ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 k In_0_2 HkO).
We prove the intermediate claim Hamk: order_rel X a (0,k).
We prove the intermediate claim Hrel0: order_rel (setprod 2 ω) (0,m) (0,ordsucc m).
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk m HmO).
We will prove order_rel X a (0,k).
rewrite the current goal using HkEq (from left to right).
An exact proof term for the current goal is Hrel0.
Apply (order_rel_trichotomy_or_impred X y (0,k) Hso HyX HkX (y ∈ {(0,k)})) to the current goal.
Assume Hylk: order_rel X y (0,k).
Apply FalseE to the current goal.
We prove the intermediate claim Hy0k: order_rel (setprod 2 ω) y (0,k).
An exact proof term for the current goal is Hylk.
We prove the intermediate claim Hya0: order_rel (setprod 2 ω) (0,m) y.
An exact proof term for the current goal is Hya.
We prove the intermediate claim HyUp: order_rel (setprod 2 ω) y (0,ordsucc m).
rewrite the current goal using HkEq (from right to left).
An exact proof term for the current goal is Hy0k.
An exact proof term for the current goal is (no_point_between_setprod_2_omega_0k_0succk m y HmO HyX Hya0 HyUp).
Assume Hey: y = (0,k).
rewrite the current goal using Hey (from left to right).
An exact proof term for the current goal is (SingI (0,k)).
Assume Hkly: order_rel X (0,k) y.
Apply FalseE to the current goal.
An exact proof term for the current goal is (no_point_between_setprod_2_omega_0k_0succk k y HkO HyX Hkly Hyb).
Let y be given.
Assume HyS: y ∈ {(0,k)}.
We will prove y ∈ U.
We prove the intermediate claim Hey: y = (0,k).
An exact proof term for the current goal is (SingE (0,k) y HyS).
rewrite the current goal using Hey (from left to right).
We prove the intermediate claim HkX2: (0,k) ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 k In_0_2 HkO).
We prove the intermediate claim Hamk2: order_rel X a (0,k).
We prove the intermediate claim Hrel0: order_rel (setprod 2 ω) (0,m) (0,ordsucc m).
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk m HmO).
We will prove order_rel X a (0,k).
rewrite the current goal using HkEq (from left to right).
An exact proof term for the current goal is Hrel0.
Apply (SepI X (λy0 : set ⇒ order_rel X a y0 ∧ order_rel X y0 b) (0,k) HkX2) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hamk2.
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk k HkO).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUopen.
∎