Let X, Tx and W be given.
Assume HTx: topology_on X Tx.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
We will prove ∃B : set, (∀b : set, b ∈ B → b ∈ Tx) ∧ locally_finite_family X Tx B ∧ (∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w) ∧ ∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w.
Set coreW to be the term λw : set ⇒ Eps_i (λBw : set ⇒ Bw ∈ Tx ∧ Bw ⊆ w ∧ closure_of X Tx Bw ⊆ w).
We prove the intermediate claim HcoreW: ∀w : set, w ∈ W → coreW w ∈ Tx ∧ coreW w ⊆ w ∧ closure_of X Tx (coreW w) ⊆ w.
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hex: ∃Bw : set, Bw ∈ Tx ∧ Bw ⊆ w ∧ closure_of X Tx Bw ⊆ w.
An exact proof term for the current goal is (locally_finite_open_cover_core_open_set X Tx W w HTx HWcov HWlf HwW).
Apply Hex to the current goal.
Let Bw be given.
Assume HBw: Bw ∈ Tx ∧ Bw ⊆ w ∧ closure_of X Tx Bw ⊆ w.
An exact proof term for the current goal is (Eps_i_ax (λBw0 : set ⇒ Bw0 ∈ Tx ∧ Bw0 ⊆ w ∧ closure_of X Tx Bw0 ⊆ w) Bw HBw).
Set B to be the term {coreW w|w ∈ W}.
We prove the intermediate claim HBmemTx: ∀b : set, b ∈ B → b ∈ Tx.
Let b be given.
Assume Hb: b ∈ B.
Apply (ReplE_impred W (λw0 : set ⇒ coreW w0) b Hb (b ∈ Tx)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume Heq: b = coreW w.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hpair: coreW w ∈ Tx ∧ coreW w ⊆ w.
An exact proof term for the current goal is (andEL (coreW w ∈ Tx ∧ coreW w ⊆ w) (closure_of X Tx (coreW w) ⊆ w) (HcoreW w HwW)).
An exact proof term for the current goal is (andEL (coreW w ∈ Tx) (coreW w ⊆ w) Hpair).
We prove the intermediate claim HcoreWsub: ∀w : set, w ∈ W → coreW w ⊆ w.
Let w be given.
Assume HwW: w ∈ W.
We prove the intermediate claim Hpair: coreW w ∈ Tx ∧ coreW w ⊆ w.
An exact proof term for the current goal is (andEL (coreW w ∈ Tx ∧ coreW w ⊆ w) (closure_of X Tx (coreW w) ⊆ w) (HcoreW w HwW)).
An exact proof term for the current goal is (andER (coreW w ∈ Tx) (coreW w ⊆ w) Hpair).
We prove the intermediate claim HBlf: locally_finite_family X Tx B.
An exact proof term for the current goal is (locally_finite_family_Repl_subsets X Tx W coreW HWlf HcoreWsub).
We prove the intermediate claim HBsubW: ∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ b ⊆ w.
Let b be given.
Assume Hb: b ∈ B.
Apply (ReplE_impred W (λw0 : set ⇒ coreW w0) b Hb (∃w : set, w ∈ W ∧ b ⊆ w)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume Heq: b = coreW w.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HwW.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (HcoreWsub w HwW).
We prove the intermediate claim HBclsubW: ∀b : set, b ∈ B → ∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w.
Let b be given.
Assume Hb: b ∈ B.
Apply (ReplE_impred W (λw0 : set ⇒ coreW w0) b Hb (∃w : set, w ∈ W ∧ closure_of X Tx b ⊆ w)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume Heq: b = coreW w.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HwW.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (andER (coreW w ∈ Tx ∧ coreW w ⊆ w) (closure_of X Tx (coreW w) ⊆ w) (HcoreW w HwW)).
We use B 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 HBmemTx.
An exact proof term for the current goal is HBlf.
An exact proof term for the current goal is HBsubW.
An exact proof term for the current goal is HBclsubW.
∎