We will prove generated_topology ω (order_topology_basis ω) = 𝒫 ω.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ generated_topology ω (order_topology_basis ω).
We will prove U ∈ 𝒫 ω.
An exact proof term for the current goal is (SepE1 (𝒫 ω) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ order_topology_basis ω, x ∈ b ∧ b ⊆ U0) U HU).
Let U be given.
Assume HU: U ∈ 𝒫 ω.
We will prove U ∈ generated_topology ω (order_topology_basis ω).
We will prove U ∈ {U0 ∈ 𝒫 ω|∀x ∈ U0, ∃b ∈ order_topology_basis ω, x ∈ b ∧ b ⊆ U0}.
Apply (SepI (𝒫 ω) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ order_topology_basis ω, x ∈ b ∧ b ⊆ U0) U HU) to the current goal.
We prove the intermediate claim HUsub: U ⊆ ω.
An exact proof term for the current goal is (PowerE ω U HU).
Let x be given.
Assume Hx: x ∈ U.
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 (HUsub x Hx)).
Apply andI to the current goal.
An exact proof term for the current goal is (SingI x).
Let y be given.
Assume Hy: y ∈ {x}.
We will prove y ∈ U.
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is Hx.
∎