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

Apply andI to the current goal.

Let s be given.

Assume Hs: s ∈ Spt.

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 ∈ ⋃ Spt.

We will prove f ∈ Dom.

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

Let U be given.

Assume HfU: f ∈ U.

Assume HU: U ∈ Spt.

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 HUpow: 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 HUpow 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 prove the intermediate claim HDomInS: Dom ∈ Spt.

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 Spt f Dom Hf HDomInS).

Let s be given.

Assume Hs: s ∈ Spt.

We will prove s ∈ Tc.

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

Assume Hsp: s ∈ pointwise_subbasis X Tx Y Ty.

We prove the intermediate claim Hex: ∃x U : set, x ∈ X ∧ U ∈ Ty ∧ s = {f ∈ Dom|apply_fun f x ∈ U}.

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

Apply Hex to the current goal.

Let x be given.

Assume Hex1: ∃U : set, x ∈ X ∧ U ∈ Ty ∧ s = {f ∈ Dom|apply_fun f x ∈ U}.

Apply Hex1 to the current goal.

Let U be given.

Assume HxU: x ∈ X ∧ U ∈ Ty ∧ s = {f ∈ Dom|apply_fun f x ∈ U}.

We prove the intermediate claim HxU1: (x ∈ X ∧ U ∈ Ty).

An exact proof term for the current goal is (andEL (x ∈ X ∧ U ∈ Ty) (s = {f ∈ Dom|apply_fun f x ∈ U}) HxU).

We prove the intermediate claim Hseq: s = {f ∈ Dom|apply_fun f x ∈ U}.

An exact proof term for the current goal is (andER (x ∈ X ∧ U ∈ Ty) (s = {f ∈ Dom|apply_fun f x ∈ U}) HxU).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (andEL (x ∈ X) (U ∈ Ty) HxU1).

We prove the intermediate claim HU: U ∈ Ty.

An exact proof term for the current goal is (andER (x ∈ X) (U ∈ Ty) HxU1).

Set K to be the term {x}.

Set S0 to be the term {f ∈ Dom|K ⊆ preimage_of X f U}.

We prove the intermediate claim HKsub: K ⊆ X.

Let t be given.

Assume Ht: t ∈ K.

We prove the intermediate claim Hteq: t = x.

An exact proof term for the current goal is (SingE x t Ht).

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

An exact proof term for the current goal is HxX.

We prove the intermediate claim HTK: topology_on K (subspace_topology X Tx K).

An exact proof term for the current goal is (subspace_topology_is_topology X Tx K HTx HKsub).

We prove the intermediate claim HKcomp: compact_space K (subspace_topology X Tx K).

We prove the intermediate claim HKdef: K = {x}.

Use reflexivity.

An exact proof term for the current goal is (compact_space_singleton K (subspace_topology X Tx K) x HKdef HTK).

We prove the intermediate claim HS0inSub: S0 ∈ compact_open_subbasis X Tx Y Ty.

We prove the intermediate claim HS0sub: S0 ⊆ Dom.

Let f be given.

Assume HfS0: f ∈ S0.

An exact proof term for the current goal is (SepE1 Dom (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f HfS0).

We prove the intermediate claim HS0pow: S0 ∈ 𝒫 Dom.

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

We prove the intermediate claim HS0prop: ∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S0 = {f0 ∈ Dom|K0 ⊆ preimage_of X f0 U0}.

We use K to witness the existential quantifier.

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HKcomp.

An exact proof term for the current goal is HKsub.

An exact proof term for the current goal is HU.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Dom) (λS : set ⇒ ∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S = {f0 ∈ Dom|K0 ⊆ preimage_of X f0 U0}) S0 HS0pow HS0prop).

We prove the intermediate claim HS0eq: {f ∈ Dom|apply_fun f x ∈ U} = S0.

Apply set_ext to the current goal.

Let f be given.

Assume Hf: f ∈ {f0 ∈ Dom|apply_fun f0 x ∈ U}.

We will prove f ∈ S0.

We prove the intermediate claim HfDom: f ∈ Dom.

An exact proof term for the current goal is (SepE1 Dom (λf0 : set ⇒ apply_fun f0 x ∈ U) f Hf).

We prove the intermediate claim HfxU: apply_fun f x ∈ U.

An exact proof term for the current goal is (SepE2 Dom (λf0 : set ⇒ apply_fun f0 x ∈ U) f Hf).

We prove the intermediate claim HKpre: K ⊆ preimage_of X f U.

Let t be given.

Assume HtK: t ∈ K.

We will prove t ∈ preimage_of X f U.

We prove the intermediate claim Hteq: t = x.

An exact proof term for the current goal is (SingE x t HtK).

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

An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ U) x HxX HfxU).

An exact proof term for the current goal is (SepI Dom (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f HfDom HKpre).

Let f be given.

Assume Hf: f ∈ S0.

We will prove f ∈ {f0 ∈ Dom|apply_fun f0 x ∈ U}.

We prove the intermediate claim HfDom: f ∈ Dom.

An exact proof term for the current goal is (SepE1 Dom (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f Hf).

We prove the intermediate claim HKpre: K ⊆ preimage_of X f U.

An exact proof term for the current goal is (SepE2 Dom (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f Hf).

We prove the intermediate claim HxK: x ∈ K.

An exact proof term for the current goal is (SingI x).

We prove the intermediate claim Hxpre: x ∈ preimage_of X f U.

An exact proof term for the current goal is (HKpre x HxK).

We prove the intermediate claim HfxU: apply_fun f x ∈ U.

An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ U) x Hxpre).

An exact proof term for the current goal is (SepI Dom (λf0 : set ⇒ apply_fun f0 x ∈ U) f HfDom HfxU).

We prove the intermediate claim HS0open: S0 ∈ Tc.

We prove the intermediate claim HSsub: subbasis_on Dom (compact_open_subbasis X Tx Y Ty).

An exact proof term for the current goal is (compact_open_subbasis_is_subbasis X Tx Y Ty HTx HTy).

An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis Dom (compact_open_subbasis X Tx Y Ty) S0 HSsub HS0inSub).

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

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

An exact proof term for the current goal is HS0open.

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 (topology_has_X Dom Tc HTc).

An exact proof term for the current goal is Hs.