Let X be given.
Assume HXne: X ≠ Empty.
Apply set_ext to the current goal.
Let b be given.
Assume Hb: b ∈ basis_of_subbasis X Empty.
We will prove b ∈ {X}.
We prove the intermediate claim Hbfin: b ∈ finite_intersections_of X Empty.
An exact proof term for the current goal is (SepE1 (finite_intersections_of X Empty) (λb0 : set ⇒ b0 ≠ Empty) b Hb).
We prove the intermediate claim HexF: ∃F ∈ finite_subcollections Empty, b = intersection_of_family X F.
An exact proof term for the current goal is (ReplE (finite_subcollections Empty) (λF0 : set ⇒ intersection_of_family X F0) b Hbfin).
Apply HexF to the current goal.
Let F be given.
Assume HFpair.
Apply HFpair to the current goal.
Assume HF: F ∈ finite_subcollections Empty.
Assume Hbeq: b = intersection_of_family X F.
We prove the intermediate claim HFpow: F ∈ 𝒫 Empty.
An exact proof term for the current goal is (SepE1 (𝒫 Empty) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HFsub: F ⊆ Empty.
An exact proof term for the current goal is (PowerE Empty F HFpow).
We prove the intermediate claim Hall: ∀x : set, x ∉ F.
Let x be given.
Assume Hx: x ∈ F.
We will prove False.
We prove the intermediate claim HxE: x ∈ Empty.
An exact proof term for the current goal is (HFsub x Hx).
An exact proof term for the current goal is (EmptyE x HxE False).
We prove the intermediate claim HFeq: F = Empty.
An exact proof term for the current goal is (Empty_eq F Hall).
We prove the intermediate claim HbX: b = X.
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using HFeq (from left to right).
An exact proof term for the current goal is (intersection_of_family_empty_eq X).
rewrite the current goal using HbX (from left to right).
An exact proof term for the current goal is (SingI X).
Let b be given.
Assume Hb: b ∈ {X}.
We will prove b ∈ basis_of_subbasis X Empty.
We prove the intermediate claim HbX: b = X.
An exact proof term for the current goal is (SingE X b Hb).
rewrite the current goal using HbX (from left to right).
We prove the intermediate claim HF: Empty ∈ finite_subcollections Empty.
An exact proof term for the current goal is (SepI (𝒫 Empty) (λF0 : set ⇒ finite F0) Empty (Empty_In_Power Empty) finite_Empty).
We prove the intermediate claim Hfin: intersection_of_family X Empty ∈ finite_intersections_of X Empty.
An exact proof term for the current goal is (ReplI (finite_subcollections Empty) (λF0 : set ⇒ intersection_of_family X F0) Empty HF).
We prove the intermediate claim HXfin: X ∈ finite_intersections_of X Empty.
We prove the intermediate claim Heq: X = intersection_of_family X Empty.
rewrite the current goal using (intersection_of_family_empty_eq X) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is Hfin.
An exact proof term for the current goal is (SepI (finite_intersections_of X Empty) (λb0 : set ⇒ b0 ≠ Empty) X HXfin HXne).
∎