Let X, Tx and W be given.
Assume Hreg: regular_space X Tx.
Assume Hsig: sigma_locally_finite_basis X Tx.
Assume HWTx: W ∈ Tx.
We will prove ∃Ufam : set, countable_set Ufam ∧ Ufam ⊆ Tx ∧ ⋃ Ufam = W ∧ ∀U : set, U ∈ Ufam → closure_of X Tx U ⊆ W.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx) Hsig).
We prove the intermediate claim Hdata: ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
An exact proof term for the current goal is (sigma_locally_finite_basis_data X Tx Hsig).
Apply Hdata to the current goal.
Let Fams be given.
Assume HFams: countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
We prove the intermediate claim HcountFams: countable_set Fams.
Apply (and5E (countable_set Fams) (Fams ⊆ 𝒫 (𝒫 X)) (∀F : set, F ∈ Fams → locally_finite_family X Tx F) (basis_generates X (⋃ Fams) Tx) (∀b : set, b ∈ ⋃ Fams → b ∈ Tx) HFams (countable_set Fams)) to the current goal.
Assume Hcount Hsub Hlf Hgen Hbopen.
An exact proof term for the current goal is Hcount.
We prove the intermediate claim Hlocfin: ∀F : set, F ∈ Fams → locally_finite_family X Tx F.
Apply (and5E (countable_set Fams) (Fams ⊆ 𝒫 (𝒫 X)) (∀F : set, F ∈ Fams → locally_finite_family X Tx F) (basis_generates X (⋃ Fams) Tx) (∀b : set, b ∈ ⋃ Fams → b ∈ Tx) HFams (∀F : set, F ∈ Fams → locally_finite_family X Tx F)) to the current goal.
Assume Hcount Hsub Hlf Hgen Hbopen.
An exact proof term for the current goal is Hlf.
We prove the intermediate claim HBgen: basis_generates X (⋃ Fams) Tx.
Apply (and5E (countable_set Fams) (Fams ⊆ 𝒫 (𝒫 X)) (∀F : set, F ∈ Fams → locally_finite_family X Tx F) (basis_generates X (⋃ Fams) Tx) (∀b : set, b ∈ ⋃ Fams → b ∈ Tx) HFams (basis_generates X (⋃ Fams) Tx)) to the current goal.
Assume Hcount Hsub Hlf Hgen Hbopen.
An exact proof term for the current goal is Hgen.
We prove the intermediate claim HBref: basis_refines X (⋃ Fams) Tx.
An exact proof term for the current goal is (basis_generates_imp_basis_refines X Tx (⋃ Fams) HBgen).
We prove the intermediate claim Href: ∀U ∈ Tx, ∀x ∈ U, ∃b ∈ ⋃ Fams, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U ∈ Tx, ∀x ∈ U, ∃b ∈ ⋃ Fams, x ∈ b ∧ b ⊆ U) HBref).
We prove the intermediate claim HBopen: ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
Apply (and5E (countable_set Fams) (Fams ⊆ 𝒫 (𝒫 X)) (∀F : set, F ∈ Fams → locally_finite_family X Tx F) (basis_generates X (⋃ Fams) Tx) (∀b : set, b ∈ ⋃ Fams → b ∈ Tx) HFams (∀b : set, b ∈ ⋃ Fams → b ∈ Tx)) to the current goal.
Assume Hcount Hsub Hlf Hgen Hbopen.
An exact proof term for the current goal is Hbopen.
Set OpenCover to be the term {⋃ {b ∈ F|closure_of X Tx b ⊆ W}|F ∈ Fams}.
We prove the intermediate claim HcoverCount: countable_set OpenCover.
An exact proof term for the current goal is (countable_image Fams HcountFams (λF : set ⇒ ⋃ {b ∈ F|closure_of X Tx b ⊆ W})).
We prove the intermediate claim HcoverSubTx: OpenCover ⊆ Tx.
Let U0 be given.
Assume HU0: U0 ∈ OpenCover.
We will prove U0 ∈ Tx.
Apply (ReplE_impred Fams (λF0 : set ⇒ ⋃ {b ∈ F0|closure_of X Tx b ⊆ W}) U0 HU0 (U0 ∈ Tx)) to the current goal.
Let F be given.
Assume HF: F ∈ Fams.
Assume HU0eq: U0 = ⋃ {b ∈ F|closure_of X Tx b ⊆ W}.
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim HFgoodSubTx: {b ∈ F|closure_of X Tx b ⊆ W} ⊆ Tx.
Let b be given.
Assume HbFg: b ∈ {b ∈ F|closure_of X Tx b ⊆ W}.
We will prove b ∈ Tx.
We prove the intermediate claim HbF: b ∈ F.
An exact proof term for the current goal is (SepE1 F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b HbFg).
We prove the intermediate claim HbU: b ∈ ⋃ Fams.
An exact proof term for the current goal is (UnionI Fams b F HbF HF).
An exact proof term for the current goal is (HBopen b HbU).
We prove the intermediate claim HFgoodPow: {b ∈ F|closure_of X Tx b ⊆ W} ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx {b ∈ F|closure_of X Tx b ⊆ W} HFgoodSubTx).
An exact proof term for the current goal is (lemma_union_of_topology_family_open X Tx {b ∈ F|closure_of X Tx b ⊆ W} HTx HFgoodPow).
We prove the intermediate claim HcoverUnionSub: ⋃ OpenCover ⊆ W.
Let x be given.
Assume Hx: x ∈ ⋃ OpenCover.
We will prove x ∈ W.
Apply (UnionE_impred OpenCover x Hx (x ∈ W)) to the current goal.
Let U0 be given.
Assume HxU0: x ∈ U0.
Assume HU0: U0 ∈ OpenCover.
Apply (ReplE_impred Fams (λF0 : set ⇒ ⋃ {b ∈ F0|closure_of X Tx b ⊆ W}) U0 HU0 (x ∈ W)) to the current goal.
Let F be given.
Assume HF: F ∈ Fams.
Assume HU0eq: U0 = ⋃ {b ∈ F|closure_of X Tx b ⊆ W}.
We prove the intermediate claim HxU: x ∈ ⋃ {b ∈ F|closure_of X Tx b ⊆ W}.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HxU0.
Apply (UnionE_impred {b ∈ F|closure_of X Tx b ⊆ W} x HxU (x ∈ W)) to the current goal.
Let b be given.
Assume Hxb: x ∈ b.
Assume HbFg: b ∈ {b ∈ F|closure_of X Tx b ⊆ W}.
We prove the intermediate claim HclbSubW: closure_of X Tx b ⊆ W.
An exact proof term for the current goal is (SepE2 F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b HbFg).
We prove the intermediate claim HbF: b ∈ F.
An exact proof term for the current goal is (SepE1 F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b HbFg).
We prove the intermediate claim HbU: b ∈ ⋃ Fams.
An exact proof term for the current goal is (UnionI Fams b F HbF HF).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbU).
We prove the intermediate claim HbSubX: b ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx b HTx HbTx).
We prove the intermediate claim HbSubCl: b ⊆ closure_of X Tx b.
An exact proof term for the current goal is (subset_of_closure X Tx b HTx HbSubX).
An exact proof term for the current goal is (HclbSubW x (HbSubCl x Hxb)).
We prove the intermediate claim HcoverUnionSup: W ⊆ ⋃ OpenCover.
Let x be given.
Assume HxW: x ∈ W.
We will prove x ∈ ⋃ OpenCover.
We prove the intermediate claim HWsubX: W ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx W HTx HWTx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HWsubX x HxW).
We prove the intermediate claim HWopen: open_in X Tx W.
An exact proof term for the current goal is (open_inI X Tx W HTx HWTx).
Apply (regular_space_shrink_neighborhood X Tx x W Hreg HxX HWTx HxW) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Tx ∧ x ∈ V0 ∧ closure_of X Tx V0 ⊆ W.
We prove the intermediate claim HV0a: (V0 ∈ Tx ∧ x ∈ V0) ∧ closure_of X Tx V0 ⊆ W.
An exact proof term for the current goal is HV0.
We prove the intermediate claim HV0b: V0 ∈ Tx ∧ x ∈ V0.
An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ W) HV0a).
We prove the intermediate claim HclV0subW: closure_of X Tx V0 ⊆ W.
An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ x ∈ V0) (closure_of X Tx V0 ⊆ W) HV0a).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (x ∈ V0) HV0b).
We prove the intermediate claim HxV0: x ∈ V0.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (x ∈ V0) HV0b).
We prove the intermediate claim Hexb: ∃b ∈ ⋃ Fams, x ∈ b ∧ b ⊆ V0.
An exact proof term for the current goal is (Href V0 HV0Tx x HxV0).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack: b ∈ ⋃ Fams ∧ (x ∈ b ∧ b ⊆ V0).
We prove the intermediate claim HbU: b ∈ ⋃ Fams.
An exact proof term for the current goal is (andEL (b ∈ ⋃ Fams) (x ∈ b ∧ b ⊆ V0) Hbpack).
We prove the intermediate claim Hxband: x ∈ b ∧ b ⊆ V0.
An exact proof term for the current goal is (andER (b ∈ ⋃ Fams) (x ∈ b ∧ b ⊆ V0) Hbpack).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ V0) Hxband).
We prove the intermediate claim HbsubV0: b ⊆ V0.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ V0) Hxband).
We prove the intermediate claim HexF: ∃F ∈ Fams, b ∈ F.
Apply (UnionE Fams b HbU) to the current goal.
Let F be given.
Assume HFpack: b ∈ F ∧ F ∈ Fams.
We use F to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andER (b ∈ F) (F ∈ Fams) HFpack).
An exact proof term for the current goal is (andEL (b ∈ F) (F ∈ Fams) HFpack).
Apply HexF to the current goal.
Let F be given.
Assume HFpack.
We prove the intermediate claim HF: F ∈ Fams.
An exact proof term for the current goal is (andEL (F ∈ Fams) (b ∈ F) HFpack).
We prove the intermediate claim HbF: b ∈ F.
An exact proof term for the current goal is (andER (F ∈ Fams) (b ∈ F) HFpack).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbU).
We prove the intermediate claim HbSubX: b ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx b HTx HbTx).
We prove the intermediate claim HV0SubX: V0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V0 HTx HV0Tx).
We prove the intermediate claim HclbSubclV0: closure_of X Tx b ⊆ closure_of X Tx V0.
An exact proof term for the current goal is (closure_monotone X Tx b V0 HTx HbsubV0 HV0SubX).
We prove the intermediate claim HclbSubW: closure_of X Tx b ⊆ W.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx b) (closure_of X Tx V0) W HclbSubclV0 HclV0subW).
We prove the intermediate claim HbFg: b ∈ {b ∈ F|closure_of X Tx b ⊆ W}.
Apply (SepI F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b HbF) to the current goal.
An exact proof term for the current goal is HclbSubW.
Set U0 to be the term ⋃ {b ∈ F|closure_of X Tx b ⊆ W}.
We prove the intermediate claim HU0in: U0 ∈ OpenCover.
An exact proof term for the current goal is (ReplI Fams (λF0 : set ⇒ ⋃ {b ∈ F0|closure_of X Tx b ⊆ W}) F HF).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (UnionI {b ∈ F|closure_of X Tx b ⊆ W} x b Hxb HbFg).
An exact proof term for the current goal is (UnionI OpenCover x U0 HxU0 HU0in).
We prove the intermediate claim HunionEq: ⋃ OpenCover = W.
Apply set_ext to the current goal.
An exact proof term for the current goal is HcoverUnionSub.
An exact proof term for the current goal is HcoverUnionSup.
We prove the intermediate claim HclosureSubW: ∀U : set, U ∈ OpenCover → closure_of X Tx U ⊆ W.
Let U0 be given.
Assume HU0: U0 ∈ OpenCover.
Apply (ReplE_impred Fams (λF0 : set ⇒ ⋃ {b ∈ F0|closure_of X Tx b ⊆ W}) U0 HU0 (closure_of X Tx U0 ⊆ W)) to the current goal.
Let F be given.
Assume HF: F ∈ Fams.
Assume HU0eq: U0 = ⋃ {b ∈ F|closure_of X Tx b ⊆ W}.
rewrite the current goal using HU0eq (from left to right).
Set Fgood to be the term {b ∈ F|closure_of X Tx b ⊆ W}.
We prove the intermediate claim HFgoodSubF: Fgood ⊆ F.
Let b be given.
Assume Hb: b ∈ Fgood.
An exact proof term for the current goal is (SepE1 F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b Hb).
We prove the intermediate claim HLF: locally_finite_family X Tx F.
An exact proof term for the current goal is (Hlocfin F HF).
We prove the intermediate claim HLFgood: locally_finite_family X Tx Fgood.
An exact proof term for the current goal is (lemma39_1a_subcollection_locally_finite X Tx F Fgood HLF HFgoodSubF).
We prove the intermediate claim HFgoodSubX: ∀b : set, b ∈ Fgood → b ⊆ X.
Let b be given.
Assume HbFg: b ∈ Fgood.
We prove the intermediate claim HbF: b ∈ F.
An exact proof term for the current goal is (SepE1 F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b HbFg).
We prove the intermediate claim HbU: b ∈ ⋃ Fams.
An exact proof term for the current goal is (UnionI Fams b F HbF HF).
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBopen b HbU).
An exact proof term for the current goal is (topology_elem_subset X Tx b HTx HbTx).
We prove the intermediate claim HclEq: closure_of X Tx (⋃ Fgood) = ⋃ {closure_of X Tx b|b ∈ Fgood}.
An exact proof term for the current goal is (lemma39_1c_closure_Union_eq_Union_closures X Tx Fgood HTx HFgoodSubX HLFgood).
rewrite the current goal using HclEq (from left to right).
Let x be given.
Assume Hx: x ∈ ⋃ {closure_of X Tx b|b ∈ Fgood}.
We will prove x ∈ W.
Apply (UnionE_impred {closure_of X Tx b|b ∈ Fgood} x Hx (x ∈ W)) to the current goal.
Let Y be given.
Assume HxY: x ∈ Y.
Assume HY: Y ∈ {closure_of X Tx b|b ∈ Fgood}.
Apply (ReplE_impred Fgood (λb0 : set ⇒ closure_of X Tx b0) Y HY (x ∈ W)) to the current goal.
Let b be given.
Assume HbFg: b ∈ Fgood.
Assume HYe: Y = closure_of X Tx b.
We prove the intermediate claim HclbSubW: closure_of X Tx b ⊆ W.
An exact proof term for the current goal is (SepE2 F (λb0 : set ⇒ closure_of X Tx b0 ⊆ W) b HbFg).
We prove the intermediate claim HxClb: x ∈ closure_of X Tx b.
rewrite the current goal using HYe (from right to left).
An exact proof term for the current goal is HxY.
An exact proof term for the current goal is (HclbSubW x HxClb).
We use OpenCover to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HcoverCount.
An exact proof term for the current goal is HcoverSubTx.
An exact proof term for the current goal is HunionEq.
An exact proof term for the current goal is HclosureSubW.
∎