Let x be given.
Assume Hxomega: x ∈ ω.
We prove the intermediate claim Hxnat: nat_p x.
An exact proof term for the current goal is (omega_nat_p x Hxomega).
We prove the intermediate claim Hinv: x = 0 ∨ ∃m : set, nat_p m ∧ x = ordsucc m.
An exact proof term for the current goal is (nat_inv x Hxnat).
Apply Hinv to the current goal.
Assume Hx0: x = 0.
rewrite the current goal using Hx0 (from left to right).
rewrite the current goal using open_ray_lower_omega_1_eq_Sing0 (from right to left).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis ω 1 H1omega).
Assume Hex: ∃m : set, nat_p m ∧ x = ordsucc m.
Apply Hex to the current goal.
Let m be given.
Assume Hmcore: nat_p m ∧ x = ordsucc m.
We prove the intermediate claim Hmnat: nat_p m.
An exact proof term for the current goal is (andEL (nat_p m) (x = ordsucc m) Hmcore).
We prove the intermediate claim Hxeq: x = ordsucc m.
An exact proof term for the current goal is (andER (nat_p m) (x = ordsucc m) Hmcore).
We prove the intermediate claim Hx1omega: ordsucc m ∈ ω.
rewrite the current goal using Hxeq (from right to left).
An exact proof term for the current goal is Hxomega.
rewrite the current goal using Hxeq (from left to right).
Set x1 to be the term ordsucc m.
Set b to be the term ordsucc x1.
We prove the intermediate claim Hmomega: m ∈ ω.
An exact proof term for the current goal is (nat_p_omega m Hmnat).
We prove the intermediate claim Hbomega: b ∈ ω.
An exact proof term for the current goal is (omega_ordsucc x1 Hx1omega).
Set I to be the term {y ∈ ω|order_rel ω m y ∧ order_rel ω y b}.
We prove the intermediate claim HIeq: I = {x1}.
Apply set_ext to the current goal.
Let y be given.
Assume HyI: y ∈ I.
We will prove y ∈ {x1}.
We prove the intermediate claim Hycore: order_rel ω m y ∧ order_rel ω y b.
An exact proof term for the current goal is (SepE2 ω (λy0 : set ⇒ order_rel ω m y0 ∧ order_rel ω y0 b) y HyI).
We prove the intermediate claim Hmy: order_rel ω m y.
An exact proof term for the current goal is (andEL (order_rel ω m y) (order_rel ω y b) Hycore).
We prove the intermediate claim Hyb: order_rel ω y b.
An exact proof term for the current goal is (andER (order_rel ω m y) (order_rel ω y b) Hycore).
We prove the intermediate claim Hm_in_y: m ∈ y.
An exact proof term for the current goal is (order_rel_omega_implies_mem m y Hmy).
We prove the intermediate claim Hy_in_b: y ∈ b.
An exact proof term for the current goal is (order_rel_omega_implies_mem y b Hyb).
Apply (ordsuccE x1 y Hy_in_b) to the current goal.
Assume Hyin: y ∈ x1.
Apply (ordsuccE m y Hyin) to the current goal.
Assume Hyinm: y ∈ m.
Apply FalseE to the current goal.
An exact proof term for the current goal is (In_no2cycle m y Hm_in_y Hyinm).
Assume Heq0: y = m.
Apply FalseE to the current goal.
We prove the intermediate claim Hmm: m ∈ m.
rewrite the current goal using Heq0 (from right to left) at position 2.
An exact proof term for the current goal is Hm_in_y.
An exact proof term for the current goal is ((In_irref m) Hmm).
Assume Heq1: y = x1.
rewrite the current goal using Heq1 (from left to right).
An exact proof term for the current goal is (SingI x1).
Let y be given.
Assume HyS: y ∈ {x1}.
We will prove y ∈ I.
We prove the intermediate claim Heq: y = x1.
An exact proof term for the current goal is (SingE x1 y HyS).
rewrite the current goal using Heq (from left to right).
Apply (SepI ω (λy0 : set ⇒ order_rel ω m y0 ∧ order_rel ω y0 b) x1 Hx1omega) to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hmemb: m ∈ x1.
An exact proof term for the current goal is (ordsuccI2 m).
An exact proof term for the current goal is (mem_implies_order_rel_omega m x1 Hmemb).
We prove the intermediate claim Hx1b: x1 ∈ b.
An exact proof term for the current goal is (ordsuccI2 x1).
An exact proof term for the current goal is (mem_implies_order_rel_omega x1 b Hx1b).
We prove the intermediate claim HIpow: I ∈ 𝒫 ω.
Apply PowerI to the current goal.
Let y be given.
Assume HyI: y ∈ I.
An exact proof term for the current goal is (SepE1 ω (λy0 : set ⇒ order_rel ω m y0 ∧ order_rel ω y0 b) y HyI).
We prove the intermediate claim Hexab: ∃a ∈ ω, ∃b0 ∈ ω, I = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}.
We use m to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hmomega.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbomega.
Use reflexivity.
We prove the intermediate claim HIinFam: I ∈ {I0 ∈ 𝒫 ω|∃a ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}}.
An exact proof term for the current goal is (SepI (𝒫 ω) (λI0 : set ⇒ ∃a ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}) I HIpow Hexab).
rewrite the current goal using HIeq (from right to left).
Set Bold to be the term (({I0 ∈ 𝒫 ω|∃a0 ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a0 y ∧ order_rel ω y b0}} ∪ {I0 ∈ 𝒫 ω|∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}}) ∪ {I0 ∈ 𝒫 ω|∃a0 ∈ ω, I0 = {y ∈ ω|order_rel ω a0 y}}).
An exact proof term for the current goal is (binunionI1 Bold {ω} I (binunionI1 ({I0 ∈ 𝒫 ω|∃a0 ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a0 y ∧ order_rel ω y b0}} ∪ {I0 ∈ 𝒫 ω|∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}}) {I0 ∈ 𝒫 ω|∃a0 ∈ ω, I0 = {y ∈ ω|order_rel ω a0 y}} I (binunionI1 {I0 ∈ 𝒫 ω|∃a0 ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a0 y ∧ order_rel ω y b0}} {I0 ∈ 𝒫 ω|∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}} I HIinFam))).
∎