Let X be given.
We will prove ((singleton_basis X ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b ∈ singleton_basis X, x ∈ b)) ∧ (∀b1 ∈ singleton_basis X, ∀b2 ∈ singleton_basis X, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ singleton_basis X, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)).
Apply and3I to the current goal.
We will prove singleton_basis X ⊆ 𝒫 X.
Let s be given.
Assume Hs.
Apply (ReplE_impred X (λx0 : set ⇒ {x0}) s Hs) to the current goal.
Let x be given.
Assume HxX Hseq.
rewrite the current goal using Hseq (from left to right).
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ {x}.
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 HxX.
We will prove ∀x ∈ X, ∃b ∈ singleton_basis X, x ∈ b.
Let x be given.
Assume HxX.
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 HxX).
An exact proof term for the current goal is (SingI x).
We will prove ∀b1 ∈ singleton_basis X, ∀b2 ∈ singleton_basis X, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ singleton_basis X, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
Let b1 be given.
Assume Hb1.
Let b2 be given.
Assume Hb2.
Let x be given.
Assume Hx1 Hx2.
Apply (ReplE_impred X (λx0 : set ⇒ {x0}) b1 Hb1) to the current goal.
Let x1 be given.
Assume Hx1X Hb1eq.
Apply (ReplE_impred X (λx0 : set ⇒ {x0}) b2 Hb2) to the current goal.
Let x2 be given.
Assume Hx2X Hb2eq.
We prove the intermediate claim Hx1in: x ∈ {x1}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim Hx2in: x ∈ {x2}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim Hx_eq_x1: x = x1.
An exact proof term for the current goal is (SingE x1 x Hx1in).
We prove the intermediate claim Hx_eq_x2: x = x2.
An exact proof term for the current goal is (SingE x2 x Hx2in).
We prove the intermediate claim HxX: x ∈ X.
rewrite the current goal using Hx_eq_x1 (from left to right).
An exact proof term for the current goal is Hx1X.
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 HxX).
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.
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 (binintersectI b1 b2 x Hx1 Hx2).
∎