Let X, Tx, W and x be given.
Assume HWcov: open_cover X Tx W.
Assume HWlf: locally_finite_family X Tx W.
Assume HxX: x ∈ X.
We will prove ∃N S : set, N ∈ Tx ∧ x ∈ N ∧ finite S ∧ S ⊆ W ∧ N ⊆ ⋃ S.
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 HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcov).
We prove the intermediate claim Hex: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (locally_finite_family_property X Tx W HWlf x HxX).
Apply Hex to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HNpair: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S) HNpack).
We prove the intermediate claim HNTx: N ∈ Tx.
An exact proof term for the current goal is (andEL (N ∈ Tx) (x ∈ N) HNpair).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNpair).
We prove the intermediate claim HexS: ∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S) HNpack).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HS1: finite S ∧ S ⊆ W.
An exact proof term for the current goal is (andEL (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ W) HS1).
We prove the intermediate claim HSsubW: S ⊆ W.
An exact proof term for the current goal is (andER (finite S) (S ⊆ W) HS1).
We prove the intermediate claim HSprop: ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S) HS).
We prove the intermediate claim HNsubU: N ⊆ ⋃ S.
Let y be given.
Assume HyN: y ∈ N.
We prove the intermediate claim HNsubX: N ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx N HTx HNTx).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HNsubX y HyN).
We prove the intermediate claim Hexw: ∃w : set, w ∈ W ∧ y ∈ w.
An exact proof term for the current goal is (HWcovers y HyX).
Apply Hexw to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ y ∈ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (y ∈ w) Hw).
We prove the intermediate claim Hyw: y ∈ w.
An exact proof term for the current goal is (andER (w ∈ W) (y ∈ w) Hw).
We prove the intermediate claim HywN: y ∈ w ∩ N.
An exact proof term for the current goal is (binintersectI w N y Hyw HyN).
We prove the intermediate claim Hwint: w ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (w ∩ N) y HywN).
We prove the intermediate claim HwS: w ∈ S.
An exact proof term for the current goal is (HSprop w HwW Hwint).
An exact proof term for the current goal is (UnionI S y w Hyw HwS).
We use N to witness the existential quantifier.
We use S to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HNTx.
An exact proof term for the current goal is HxN.
An exact proof term for the current goal is HSfin.
An exact proof term for the current goal is HSsubW.
An exact proof term for the current goal is HNsubU.
∎