Let X, Tx, A and F be given.
Assume Hnorm: normal_space X Tx.
Assume HAcl: closed_in X Tx A.
Assume HFfin: finite F.
Assume HFTx: ∀w : set, w ∈ F → w ∈ Tx.
Assume HAUF: A ⊆ ⋃ F.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (normal_space_topology_on X Tx Hnorm).
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ A = X ∖ U.
An exact proof term for the current goal is (closed_in_exists_open_complement X Tx A HAcl).
Apply HexU to the current goal.
Let U be given.
Assume HU: U ∈ Tx ∧ A = X ∖ U.
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (A = X ∖ U) HU).
We prove the intermediate claim HAeq: A = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (A = X ∖ U) HU).
Set W to be the term F ∪ {U}.
We prove the intermediate claim HWfin: finite W.
An exact proof term for the current goal is (binunion_finite F HFfin {U} (Sing_finite U)).
We prove the intermediate claim HWcov: open_cover X Tx W.
We will prove (∀w : set, w ∈ W → w ∈ Tx) ∧ covers X W.
Apply andI to the current goal.
Let w be given.
Assume Hw: w ∈ W.
Apply (binunionE F {U} w Hw) to the current goal.
Assume HwF: w ∈ F.
An exact proof term for the current goal is (HFTx w HwF).
Assume HwU: w ∈ {U}.
We prove the intermediate claim Heq: w = U.
An exact proof term for the current goal is (SingE U w HwU).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HUTx.
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim HxUF: x ∈ ⋃ F.
An exact proof term for the current goal is (HAUF x HxA).
Apply (UnionE F x HxUF) to the current goal.
Let w be given.
Assume Hw: x ∈ w ∧ w ∈ F.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 F {U} w (andER (x ∈ w) (w ∈ F) Hw)).
An exact proof term for the current goal is (andEL (x ∈ w) (w ∈ F) Hw).
Assume HxnotA: ¬ (x ∈ A).
We prove the intermediate claim HxU: x ∈ U.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is HxU.
Assume HxnotU: ¬ (x ∈ U).
We prove the intermediate claim HxA2: x ∈ A.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (setminusI X U x HxX HxnotU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotA HxA2).
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 F {U} U (SingI U)).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ finite V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (normal_space_finite_open_cover_shrinking X Tx W Hnorm HWcov HWfin).
Apply HexV to the current goal.
Let V be given.
Assume HV: open_cover X Tx V ∧ finite V ∧ (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) ∧ ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HVopen: open_cover X Tx V.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hcov.
We prove the intermediate claim HVfin: finite V.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hfin.
We prove the intermediate claim HVclmapW: ∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
Apply (and4E (open_cover X Tx V) (finite V) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ v ⊆ w) (∀v : set, v ∈ V → ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w) HV) to the current goal.
Assume Hcov Hfin Hsub Hcl.
An exact proof term for the current goal is Hcl.
We prove the intermediate claim HVTx: ∀v : set, v ∈ V → v ∈ Tx.
An exact proof term for the current goal is (andEL (∀v : set, v ∈ V → v ∈ Tx) (covers X V) HVopen).
We use {v ∈ V|v ∩ A ≠ Empty} to witness the existential quantifier.
Set V0 to be the term {v ∈ V|v ∩ A ≠ Empty}.
We prove the intermediate claim HV0subV: V0 ⊆ V.
Let v be given.
Assume Hv0: v ∈ V0.
An exact proof term for the current goal is (SepE1 V (λv0 : set ⇒ v0 ∩ A ≠ Empty) v Hv0).
We prove the intermediate claim HV0fin: finite V0.
An exact proof term for the current goal is (Subq_finite V HVfin V0 HV0subV).
We prove the intermediate claim HV0Tx: ∀v : set, v ∈ V0 → v ∈ Tx.
Let v be given.
Assume Hv0: v ∈ V0.
An exact proof term for the current goal is (HVTx v (HV0subV v Hv0)).
We prove the intermediate claim HAUnionV0: A ⊆ ⋃ V0.
Let x be given.
Assume HxA: x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U0 ∈ Tx, A = X ∖ U0) (closed_in_package X Tx A HAcl) x HxA).
We prove the intermediate claim Hexv: ∃v : set, v ∈ V ∧ x ∈ v.
An exact proof term for the current goal is (andER (∀v : set, v ∈ V → v ∈ Tx) (covers X V) HVopen x HxX).
Apply Hexv to the current goal.
Let v be given.
Assume Hv: v ∈ V ∧ x ∈ v.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (andEL (v ∈ V) (x ∈ v) Hv).
We prove the intermediate claim Hxv: x ∈ v.
An exact proof term for the current goal is (andER (v ∈ V) (x ∈ v) Hv).
We prove the intermediate claim Hv0: v ∈ V0.
Apply (SepI V (λv0 : set ⇒ v0 ∩ A ≠ Empty) v HvV) to the current goal.
We prove the intermediate claim HxvA: x ∈ v ∩ A.
An exact proof term for the current goal is (binintersectI v A x Hxv HxA).
An exact proof term for the current goal is (elem_implies_nonempty (v ∩ A) x HxvA).
An exact proof term for the current goal is (UnionI V0 x v Hxv Hv0).
Apply and4I to the current goal.
An exact proof term for the current goal is HV0fin.
An exact proof term for the current goal is HV0Tx.
An exact proof term for the current goal is HAUnionV0.
Let v be given.
Assume Hv0: v ∈ V0.
We prove the intermediate claim HvV: v ∈ V.
An exact proof term for the current goal is (HV0subV v Hv0).
We prove the intermediate claim HvNonempty: v ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 V (λv0 : set ⇒ v0 ∩ A ≠ Empty) v Hv0).
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (HVclmapW v HvV).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ closure_of X Tx v ⊆ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (closure_of X Tx v ⊆ w) Hw).
We prove the intermediate claim Hclsub: closure_of X Tx v ⊆ w.
An exact proof term for the current goal is (andER (w ∈ W) (closure_of X Tx v ⊆ w) Hw).
Apply (binunionE F {U} w HwW (∃w0 : set, w0 ∈ F ∧ closure_of X Tx v ⊆ w0)) to the current goal.
Assume HwF: w ∈ F.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HwF.
An exact proof term for the current goal is Hclsub.
Assume HwU: w ∈ {U}.
We prove the intermediate claim Heq: w = U.
An exact proof term for the current goal is (SingE U w HwU).
We prove the intermediate claim HvsubU: v ⊆ U.
Let x be given.
Assume Hxv: x ∈ v.
We prove the intermediate claim HvsubX: v ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx v HTx (HVTx v HvV)).
We prove the intermediate claim Hxcl: x ∈ closure_of X Tx v.
An exact proof term for the current goal is (subset_of_closure X Tx v HTx HvsubX x Hxv).
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (Hclsub x Hxcl).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HvAempty: v ∩ A = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume Hx: x ∈ v ∩ A.
We will prove x ∈ Empty.
We prove the intermediate claim Hxv: x ∈ v.
An exact proof term for the current goal is (binintersectE1 v A x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE2 v A x Hx).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (HvsubU x Hxv).
We prove the intermediate claim HxnotU: x ∉ U.
We prove the intermediate claim HxA2: x ∈ X ∖ U.
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 U x HxA2).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotU HxU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HvNonempty HvAempty).
∎