Let X be given.
Apply set_ext to the current goal.
Let U be given.
Assume HUgen.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ singleton_basis X, x0 ∈ b ∧ b ⊆ U0) U HUgen).
Let U be given.
Assume HUinPow: U ∈ 𝒫 X.
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUinPow).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ singleton_basis X, x ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU.
We use {x} to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ {x0}) x (HUsubX x HxU)).
Apply andI to the current goal.
An exact proof term for the current goal is (SingI x).
Let y be given.
Assume Hy.
We prove the intermediate claim Hyx: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ singleton_basis X, x0 ∈ b ∧ b ⊆ U0) U HUinPow HUprop).
∎