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 ∃S : set, finite S ∧ S ⊆ W ∧ ∀w : set, w ∈ W → x ∈ closure_of X Tx w → w ∈ S.
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0.
An exact proof term for the current goal is (locally_finite_family_property X Tx W HWlf x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0.
We prove the intermediate claim HNpair: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S0 : set, finite S0 ∧ S0 ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0) 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 HexS0: ∃S0 : set, finite S0 ∧ S0 ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S0 : set, finite S0 ∧ S0 ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0) HNpack).
Apply HexS0 to the current goal.
Let S0 be given.
Assume HS0: finite S0 ∧ S0 ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0.
We use S0 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 (andEL (finite S0) (S0 ⊆ W) (andEL (finite S0 ∧ S0 ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0) HS0)).
An exact proof term for the current goal is (andER (finite S0) (S0 ⊆ W) (andEL (finite S0 ∧ S0 ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0) HS0)).
Let w be given.
Assume HwW: w ∈ W.
Assume Hxcl: x ∈ closure_of X Tx w.
We prove the intermediate claim HclCond: ∀U : set, U ∈ Tx → x ∈ U → U ∩ w ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ w ≠ Empty) x Hxcl).
We prove the intermediate claim HNw: N ∩ w ≠ Empty.
An exact proof term for the current goal is (HclCond N HNTx HxN).
We prove the intermediate claim HwN: w ∩ N ≠ Empty.
rewrite the current goal using (binintersect_com w N) (from left to right).
An exact proof term for the current goal is HNw.
An exact proof term for the current goal is (andER (finite S0 ∧ S0 ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S0) HS0 w HwW HwN).
∎