Set Fams to be the term {{u}|u ∈ U}.

We use Fams to witness the existential quantifier.

Apply and4I to the current goal.

An exact proof term for the current goal is (countable_image U HUcount (λu : set ⇒ {u})).

We will prove Fams ⊆ 𝒫 (𝒫 X).

Let G be given.

Assume HG: G ∈ Fams.

We will prove G ∈ 𝒫 (𝒫 X).

Apply (ReplE_impred U (λu : set ⇒ {u}) G HG) to the current goal.

Let u be given.

Assume HuU: u ∈ U.

Assume HeqG: G = {u}.

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

We prove the intermediate claim HsubPow: {u} ⊆ 𝒫 X.

Let z be given.

Assume Hz: z ∈ {u}.

We will prove z ∈ 𝒫 X.

We prove the intermediate claim Hzu: z = u.

An exact proof term for the current goal is (SingE u z Hz).

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

We prove the intermediate claim HuTx: u ∈ Tx.

An exact proof term for the current goal is (andEL (∀u0 : set, u0 ∈ U → u0 ∈ Tx) (covers X U) Hcover u HuU).

An exact proof term for the current goal is (topology_subset_axiom X Tx HTx u HuTx).

An exact proof term for the current goal is (PowerI (𝒫 X) {u} HsubPow).

Let G be given.

Assume HG: G ∈ Fams.

We will prove locally_finite_family X Tx G.

Apply (ReplE_impred U (λu : set ⇒ {u}) G HG) to the current goal.

Let u be given.

Assume HuU: u ∈ U.

Assume HeqG: G = {u}.

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

An exact proof term for the current goal is (locally_finite_family_singleton X Tx u HTx).

We will prove U = ⋃ Fams.

Apply set_ext to the current goal.

Let u be given.

Assume HuU: u ∈ U.

We will prove u ∈ ⋃ Fams.

We prove the intermediate claim HsingFam: {u} ∈ Fams.

An exact proof term for the current goal is (ReplI U (λu0 : set ⇒ {u0}) u HuU).

An exact proof term for the current goal is (UnionI Fams u {u} (SingI u) HsingFam).

Let u be given.

Assume Hu: u ∈ ⋃ Fams.

We will prove u ∈ U.

Apply (UnionE_impred Fams u Hu (u ∈ U)) to the current goal.

Let G be given.

Assume HuG: u ∈ G.

Assume HGF: G ∈ Fams.

Apply (ReplE_impred U (λu0 : set ⇒ {u0}) G HGF) to the current goal.

Let u0 be given.

Assume Hu0U: u0 ∈ U.

Assume HeqG: G = {u0}.

We prove the intermediate claim HuEq: u = u0.

We prove the intermediate claim HuG0: u ∈ {u0}.

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

An exact proof term for the current goal is HuG.

An exact proof term for the current goal is (SingE u0 u HuG0).

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

An exact proof term for the current goal is Hu0U.