Let X, Tx and W be given.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
Set ClW to be the term {closure_of X Tx w|w ∈ W}.
We use ClW to witness the existential quantifier.
Apply and4I to the current goal.
Use reflexivity.
We will prove (∀C : set, C ∈ ClW → closed_in X Tx C) ∧ covers X ClW.
Apply andI to the current goal.
Let C be given.
Assume HC: C ∈ ClW.
Apply (ReplE_impred W (λw0 : set ⇒ closure_of X Tx w0) C HC (closed_in X Tx C)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume Heq: C = closure_of X Tx w.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_finite_family_topology X Tx W HWlf).
We prove the intermediate claim HwTx: w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w0 : set, w0 ∈ W → w0 ∈ Tx) (covers X W) HWcov w HwW).
We prove the intermediate claim HsubPow: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HwPow: w ∈ 𝒫 X.
An exact proof term for the current goal is (HsubPow w HwTx).
We prove the intermediate claim HwsubX: w ⊆ X.
An exact proof term for the current goal is (PowerE X w HwPow).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (closure_is_closed X Tx w HTx HwsubX).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ x ∈ w.
An exact proof term for the current goal is (andER (∀w0 : set, w0 ∈ W → w0 ∈ Tx) (covers X W) HWcov x HxX).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ x ∈ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (x ∈ w) Hw).
We prove the intermediate claim Hxw: x ∈ w.
An exact proof term for the current goal is (andER (w ∈ W) (x ∈ w) Hw).
We use (closure_of X Tx w) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI W (λw0 : set ⇒ closure_of X Tx w0) w HwW).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_finite_family_topology X Tx W HWlf).
We prove the intermediate claim HwTx: w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w0 : set, w0 ∈ W → w0 ∈ Tx) (covers X W) HWcov w HwW).
We prove the intermediate claim HsubPow: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HwPow: w ∈ 𝒫 X.
An exact proof term for the current goal is (HsubPow w HwTx).
We prove the intermediate claim HwsubX: w ⊆ X.
An exact proof term for the current goal is (PowerE X w HwPow).
We prove the intermediate claim Hwsubcl: w ⊆ closure_of X Tx w.
An exact proof term for the current goal is (subset_of_closure X Tx w HTx HwsubX).
An exact proof term for the current goal is (Hwsubcl x Hxw).
An exact proof term for the current goal is (locally_finite_family_closures X Tx W HWlf).
Let C be given.
Assume HC: C ∈ ClW.
Apply (ReplE_impred W (λw0 : set ⇒ closure_of X Tx w0) C HC (∃w : set, w ∈ W ∧ C = closure_of X Tx w)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume Heq: C = closure_of X Tx 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.
An exact proof term for the current goal is Heq.
∎