Let X, Tx, W 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.
Assume HwW: w ∈ W.
We will prove ∃Bw : set, Bw ∈ Tx ∧ Bw ⊆ w ∧ closure_of X Tx Bw ⊆ w.
We prove the intermediate claim HWTx: ∀w0 : set, w0 ∈ W → w0 ∈ Tx.
An exact proof term for the current goal is (andEL (∀w0 : set, w0 ∈ W → w0 ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w0 : set, w0 ∈ W → w0 ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim HTsubPow: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HWsubPow: W ⊆ 𝒫 X.
An exact proof term for the current goal is (open_cover_family_sub X Tx W HTx HWcov).
We prove the intermediate claim HWsubX: ∀w0 : set, w0 ∈ W → w0 ⊆ X.
Let w0 be given.
Assume Hw0W: w0 ∈ W.
An exact proof term for the current goal is (PowerE X w0 (HWsubPow w0 Hw0W)).
Set Wno to be the term W ∖ {w}.
Set Clno to be the term {closure_of X Tx w0|w0 ∈ Wno}.
Set A to be the term ⋃ Clno.
Set Bw to be the term X ∖ A.
We prove the intermediate claim HWnoSubW: Wno ⊆ W.
Let z be given.
Assume Hz: z ∈ Wno.
An exact proof term for the current goal is (setminusE1 W {w} z Hz).
We prove the intermediate claim HWnoLF: locally_finite_family X Tx Wno.
An exact proof term for the current goal is (locally_finite_subfamily X Tx W Wno HWlf HWnoSubW).
We prove the intermediate claim HClnoLF: locally_finite_family X Tx Clno.
An exact proof term for the current goal is (locally_finite_family_closures X Tx Wno HWnoLF).
We prove the intermediate claim HClnoClosed: ∀C : set, C ∈ Clno → closed_in X Tx C.
Let C be given.
Assume HC: C ∈ Clno.
Apply (ReplE_impred Wno (λw0 : set ⇒ closure_of X Tx w0) C HC (closed_in X Tx C)) to the current goal.
Let w0 be given.
Assume Hw0: w0 ∈ Wno.
Assume HeqC: C = closure_of X Tx w0.
rewrite the current goal using HeqC (from left to right).
We prove the intermediate claim Hw0W: w0 ∈ W.
An exact proof term for the current goal is (HWnoSubW w0 Hw0).
We prove the intermediate claim Hw0Tx: w0 ∈ Tx.
An exact proof term for the current goal is (HWTx w0 Hw0W).
We prove the intermediate claim Hw0Pow: w0 ∈ 𝒫 X.
An exact proof term for the current goal is (HTsubPow w0 Hw0Tx).
We prove the intermediate claim Hw0subX: w0 ⊆ X.
An exact proof term for the current goal is (PowerE X w0 Hw0Pow).
An exact proof term for the current goal is (closure_is_closed X Tx w0 HTx Hw0subX).
We prove the intermediate claim HAclosed: closed_in X Tx A.
An exact proof term for the current goal is (Union_locally_finite_closed_is_closed X Tx Clno HClnoLF HClnoClosed).
We prove the intermediate claim HBTx: Bw ∈ Tx.
Apply (closed_in_package X Tx A HAclosed) to the current goal.
Assume HAsubX HexU.
Apply HexU to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ A = X ∖ U0.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (A = X ∖ U0) HU0).
We prove the intermediate claim HAeq: A = X ∖ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (A = X ∖ U0) HU0).
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0Tx).
We prove the intermediate claim HBwEq: Bw = U0.
Apply set_ext to the current goal.
Let x be given.
Assume HxBw: x ∈ Bw.
We will prove x ∈ U0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X A x HxBw).
Apply (xm (x ∈ U0)) to the current goal.
Assume HxU0: x ∈ U0.
An exact proof term for the current goal is HxU0.
Assume HxnotU0: x ∉ U0.
We prove the intermediate claim HxA: x ∈ A.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (setminusI X U0 x HxX HxnotU0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (setminusE2 X A x HxBw HxA).
Let x be given.
Assume HxU0: x ∈ U0.
We will prove x ∈ Bw.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HU0subX x HxU0).
We prove the intermediate claim HxnotA: x ∉ A.
Assume HxA: x ∈ A.
We prove the intermediate claim HxnotU0: x ∉ U0.
We prove the intermediate claim HxA2: x ∈ X ∖ U0.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (setminusE2 X U0 x HxA2).
An exact proof term for the current goal is (HxnotU0 HxU0).
An exact proof term for the current goal is (setminusI X A x HxX HxnotA).
rewrite the current goal using HBwEq (from left to right).
An exact proof term for the current goal is HU0Tx.
We prove the intermediate claim HBsubw: Bw ⊆ w.
Let x be given.
Assume HxB: x ∈ Bw.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X A x HxB).
We prove the intermediate claim Hexw: ∃w1 : set, w1 ∈ W ∧ x ∈ w1.
An exact proof term for the current goal is (HWcovers x HxX).
Apply Hexw to the current goal.
Let w1 be given.
Assume Hw1: w1 ∈ W ∧ x ∈ w1.
We prove the intermediate claim Hw1W: w1 ∈ W.
An exact proof term for the current goal is (andEL (w1 ∈ W) (x ∈ w1) Hw1).
We prove the intermediate claim Hxw1: x ∈ w1.
An exact proof term for the current goal is (andER (w1 ∈ W) (x ∈ w1) Hw1).
Apply (xm (w1 = w)) to the current goal.
Assume Heq: w1 = w.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hxw1.
Assume Hneq: w1 ≠ w.
We prove the intermediate claim Hw1Wno: w1 ∈ Wno.
We prove the intermediate claim Hw1not: w1 ∉ {w}.
Assume Hw1in: w1 ∈ {w}.
We prove the intermediate claim Hw1eq: w1 = w.
An exact proof term for the current goal is (SingE w w1 Hw1in).
An exact proof term for the current goal is (Hneq Hw1eq).
An exact proof term for the current goal is (setminusI W {w} w1 Hw1W Hw1not).
We prove the intermediate claim Hclw1: closure_of X Tx w1 ∈ Clno.
An exact proof term for the current goal is (ReplI Wno (λz : set ⇒ closure_of X Tx z) w1 Hw1Wno).
We prove the intermediate claim Hxclw1: x ∈ closure_of X Tx w1.
We prove the intermediate claim Hw1subX: w1 ⊆ X.
An exact proof term for the current goal is (HWsubX w1 Hw1W).
An exact proof term for the current goal is (subset_of_closure X Tx w1 HTx Hw1subX x Hxw1).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (UnionI Clno x (closure_of X Tx w1) Hxclw1 Hclw1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (setminusE2 X A x HxB HxA).
We prove the intermediate claim HBwDisjAll: ∀w1 : set, w1 ∈ W → w1 ≠ w → w1 ∩ Bw = Empty.
Let w1 be given.
Assume Hw1W: w1 ∈ W.
Assume Hw1neq: w1 ≠ w.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ w1 ∩ Bw.
We will prove z ∈ Empty.
We prove the intermediate claim Hzw1: z ∈ w1.
An exact proof term for the current goal is (binintersectE1 w1 Bw z Hz).
We prove the intermediate claim HzBw: z ∈ Bw.
An exact proof term for the current goal is (binintersectE2 w1 Bw z Hz).
We prove the intermediate claim Hw1Wno: w1 ∈ Wno.
We prove the intermediate claim Hw1not: w1 ∉ {w}.
Assume Hw1in: w1 ∈ {w}.
We prove the intermediate claim Hw1eq: w1 = w.
An exact proof term for the current goal is (SingE w w1 Hw1in).
An exact proof term for the current goal is (Hw1neq Hw1eq).
An exact proof term for the current goal is (setminusI W {w} w1 Hw1W Hw1not).
We prove the intermediate claim Hclw1: closure_of X Tx w1 ∈ Clno.
An exact proof term for the current goal is (ReplI Wno (λz0 : set ⇒ closure_of X Tx z0) w1 Hw1Wno).
We prove the intermediate claim Hzw1cl: z ∈ closure_of X Tx w1.
We prove the intermediate claim Hw1subX: w1 ⊆ X.
An exact proof term for the current goal is (HWsubX w1 Hw1W).
An exact proof term for the current goal is (subset_of_closure X Tx w1 HTx Hw1subX z Hzw1).
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (UnionI Clno z (closure_of X Tx w1) Hzw1cl Hclw1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (setminusE2 X A z HzBw HzA).
We prove the intermediate claim HclBsubw: closure_of X Tx Bw ⊆ w.
Let y be given.
Assume Hy: y ∈ closure_of X Tx Bw.
Apply (xm (y ∈ w)) to the current goal.
Assume Hyw: y ∈ w.
An exact proof term for the current goal is Hyw.
Assume Hynw: y ∉ w.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∀U : set, U ∈ Tx → y0 ∈ U → U ∩ Bw ≠ Empty) y Hy).
We prove the intermediate claim Hexw: ∃w1 : set, w1 ∈ W ∧ y ∈ w1.
An exact proof term for the current goal is (HWcovers y HyX).
Apply Hexw to the current goal.
Let w1 be given.
Assume Hw1: w1 ∈ W ∧ y ∈ w1.
We prove the intermediate claim Hw1W: w1 ∈ W.
An exact proof term for the current goal is (andEL (w1 ∈ W) (y ∈ w1) Hw1).
We prove the intermediate claim Hyw1: y ∈ w1.
An exact proof term for the current goal is (andER (w1 ∈ W) (y ∈ w1) Hw1).
We prove the intermediate claim Hw1neq: w1 ≠ w.
Assume Heq: w1 = w.
We prove the intermediate claim Hyw: y ∈ w.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hyw1.
An exact proof term for the current goal is (Hynw Hyw).
We prove the intermediate claim HBwDisj: w1 ∩ Bw = Empty.
An exact proof term for the current goal is (HBwDisjAll w1 Hw1W Hw1neq).
We prove the intermediate claim HyNbhd: ∀U : set, U ∈ Tx → y ∈ U → U ∩ Bw ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∀U : set, U ∈ Tx → y0 ∈ U → U ∩ Bw ≠ Empty) y Hy).
We prove the intermediate claim Hcontra: w1 ∩ Bw ≠ Empty.
An exact proof term for the current goal is (HyNbhd w1 (HWTx w1 Hw1W) Hyw1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontra HBwDisj).
We use Bw to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HBTx.
An exact proof term for the current goal is HBsubw.
An exact proof term for the current goal is HclBsubw.
∎