We will prove (order_topology_basis ω ⊆ 𝒫 ω) ∧ (∀x ∈ ω, ∃b ∈ (order_topology_basis ω), x ∈ b).

Apply andI to the current goal.

We will prove order_topology_basis ω ⊆ 𝒫 ω.

Let I be given.

Assume HI: I ∈ order_topology_basis ω.

We will prove I ∈ 𝒫 ω.

Set A to be the term {I0 ∈ 𝒫 ω|∃a ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}}.

Set B to be the term {I0 ∈ 𝒫 ω|∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}}.

Set C to be the term {I0 ∈ 𝒫 ω|∃a ∈ ω, I0 = {y ∈ ω|order_rel ω a y}}.

Set Bold to be the term (A ∪ B ∪ C).

Apply (binunionE Bold {ω} I HI) to the current goal.

Assume HI': I ∈ Bold.

Apply (binunionE (A ∪ B) C I HI') to the current goal.

Assume HIAB: I ∈ (A ∪ B).

Apply (binunionE A B I HIAB) to the current goal.

Assume HIA: I ∈ A.

An exact proof term for the current goal is (SepE1 (𝒫 ω) (λI0 : set ⇒ ∃a ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}) I HIA).

Assume HIB: I ∈ B.

An exact proof term for the current goal is (SepE1 (𝒫 ω) (λI0 : set ⇒ ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}) I HIB).

Assume HIC: I ∈ C.

An exact proof term for the current goal is (SepE1 (𝒫 ω) (λI0 : set ⇒ ∃a ∈ ω, I0 = {y ∈ ω|order_rel ω a y}) I HIC).

Assume HIomega: I ∈ {ω}.

We prove the intermediate claim HeqI: I = ω.

An exact proof term for the current goal is (SingE ω I HIomega).

rewrite the current goal using HeqI (from left to right).

An exact proof term for the current goal is (Self_In_Power ω).

Let x be given.

Assume Hx: x ∈ ω.

We use {x} to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (singleton_in_order_topology_basis_omega x Hx).

An exact proof term for the current goal is (SingI x).

Let b1 be given.

Assume Hb1: b1 ∈ order_topology_basis ω.

Let b2 be given.

Assume Hb2: b2 ∈ order_topology_basis ω.

Let x be given.

Assume Hx1: x ∈ b1.

Assume Hx2: x ∈ b2.

We will prove ∃b3 ∈ order_topology_basis ω, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.

We prove the intermediate claim Hb1pow: b1 ∈ 𝒫 ω.

Set A to be the term {I0 ∈ 𝒫 ω|∃a ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}}.

Set B to be the term {I0 ∈ 𝒫 ω|∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}}.

Set C to be the term {I0 ∈ 𝒫 ω|∃a ∈ ω, I0 = {y ∈ ω|order_rel ω a y}}.

Set Bold to be the term (A ∪ B ∪ C).

Apply (binunionE Bold {ω} b1 Hb1) to the current goal.

Assume Hb1U: b1 ∈ Bold.

Apply (binunionE (A ∪ B) C b1 Hb1U) to the current goal.

Assume Hb1AB: b1 ∈ (A ∪ B).

Apply (binunionE A B b1 Hb1AB) to the current goal.

Assume Hb1A: b1 ∈ A.

An exact proof term for the current goal is (SepE1 (𝒫 ω) (λI0 : set ⇒ ∃a ∈ ω, ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω a y ∧ order_rel ω y b0}) b1 Hb1A).

Assume Hb1B: b1 ∈ B.

An exact proof term for the current goal is (SepE1 (𝒫 ω) (λI0 : set ⇒ ∃b0 ∈ ω, I0 = {y ∈ ω|order_rel ω y b0}) b1 Hb1B).

Assume Hb1C: b1 ∈ C.

An exact proof term for the current goal is (SepE1 (𝒫 ω) (λI0 : set ⇒ ∃a ∈ ω, I0 = {y ∈ ω|order_rel ω a y}) b1 Hb1C).

Assume Hb1omega: b1 ∈ {ω}.

We prove the intermediate claim Hb1eq: b1 = ω.

An exact proof term for the current goal is (SingE ω b1 Hb1omega).

rewrite the current goal using Hb1eq (from left to right).

An exact proof term for the current goal is (Self_In_Power ω).

We prove the intermediate claim Hb1sub: b1 ⊆ ω.

An exact proof term for the current goal is (PowerE ω b1 Hb1pow).

We prove the intermediate claim Hxomega: x ∈ ω.

An exact proof term for the current goal is (Hb1sub x Hx1).

We use {x} to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (singleton_in_order_topology_basis_omega x Hxomega).

Apply andI to the current goal.

An exact proof term for the current goal is (SingI x).

We will prove {x} ⊆ b1 ∩ b2.

Let y be given.

Assume Hy: y ∈ {x}.

We prove the intermediate claim Heq: y = x.

An exact proof term for the current goal is (SingE x y Hy).

rewrite the current goal using Heq (from left to right).

An exact proof term for the current goal is (binintersectI b1 b2 x Hx1 Hx2).