We will prove S ⊆ 𝒫 Dom ∧ ⋃ S = Dom.

Apply andI to the current goal.

Let s be given.

Assume Hs: s ∈ S.

We will prove s ∈ 𝒫 Dom.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} s (s ∈ 𝒫 Dom)) to the current goal.

Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.

An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x U : set, x ∈ X ∧ U ∈ Ty ∧ S0 = {f ∈ Dom|apply_fun f x ∈ U}) s Hsp).

Assume HsDom: s ∈ {Dom}.

We prove the intermediate claim Hseq: s = Dom.

An exact proof term for the current goal is (SingE Dom s HsDom).

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

An exact proof term for the current goal is (PowerI Dom Dom (Subq_ref Dom)).

An exact proof term for the current goal is Hs.

Apply set_ext to the current goal.

Let f be given.

Assume Hf: f ∈ ⋃ S.

We will prove f ∈ Dom.

Apply (UnionE_impred S f Hf (f ∈ Dom)) to the current goal.

Let U be given.

Assume HfU: f ∈ U.

Assume HU: U ∈ S.

Apply (binunionE' (pointwise_subbasis X Tx Y Ty) {Dom} U (f ∈ Dom)) to the current goal.

Assume HUp: U ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim HUpow2: U ∈ 𝒫 Dom.

An exact proof term for the current goal is (SepE1 (𝒫 Dom) (λS0 : set ⇒ ∃x U0 : set, x ∈ X ∧ U0 ∈ Ty ∧ S0 = {f0 ∈ Dom|apply_fun f0 x ∈ U0}) U HUp).

An exact proof term for the current goal is (PowerE Dom U HUpow2 f HfU).

Assume HUDom: U ∈ {Dom}.

We prove the intermediate claim HUeq: U = Dom.

An exact proof term for the current goal is (SingE Dom U HUDom).

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

An exact proof term for the current goal is HfU.

An exact proof term for the current goal is HU.

Let f be given.

Assume Hf: f ∈ Dom.

We will prove f ∈ ⋃ S.

We prove the intermediate claim HDomInS: Dom ∈ S.

An exact proof term for the current goal is (binunionI2 (pointwise_subbasis X Tx Y Ty) {Dom} Dom (SingI Dom)).

An exact proof term for the current goal is (UnionI S f Dom Hf HDomInS).