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 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 HWx: ∃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 HWx 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 HSpack: finite S ∧ S ⊆ W ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate claim HSfin: finite S.
An exact proof term for the current goal is (andEL (finite S) (S ⊆ W) (andEL (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S) HSpack)).
We prove the intermediate claim HSsubW: S ⊆ W.
An exact proof term for the current goal is (andER (finite S) (S ⊆ W) (andEL (finite S ∧ S ⊆ W) (∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S) HSpack)).
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) HSpack).
We prove the intermediate claim HNTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_sub_Power X Tx HTx).
We prove the intermediate claim HNPow: N ∈ 𝒫 X.
An exact proof term for the current goal is (HNTsub N HNTx).
We prove the intermediate claim HNsubX: N ⊆ X.
An exact proof term for the current goal is (PowerE X N HNPow).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andI (N ∈ Tx) (x ∈ N) HNTx HxN).
We use S to witness the existential quantifier.
We will prove (finite S ∧ S ⊆ W ∧ N ⊆ ⋃ S) ∧ ∀A : set, A ∈ W → A ∩ N ≠ Empty → A ∈ S.
Apply andI to the current goal.
We will prove (finite S ∧ S ⊆ W) ∧ N ⊆ ⋃ S.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HSfin.
An exact proof term for the current goal is HSsubW.
Let y be given.
Assume HyN: y ∈ N.
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: ∃A : set, A ∈ W ∧ y ∈ A.
An exact proof term for the current goal is (HWcovers y HyX).
Apply Hexw to the current goal.
Let A be given.
Assume HApack: A ∈ W ∧ y ∈ A.
We prove the intermediate claim HAW: A ∈ W.
An exact proof term for the current goal is (andEL (A ∈ W) (y ∈ A) HApack).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (andER (A ∈ W) (y ∈ A) HApack).
We prove the intermediate claim HyAN: y ∈ A ∩ N.
An exact proof term for the current goal is (binintersectI A N y HyA HyN).
We prove the intermediate claim HAnN: A ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (A ∩ N) y HyAN).
We prove the intermediate claim HAinS: A ∈ S.
An exact proof term for the current goal is (HSprop A HAW HAnN).
An exact proof term for the current goal is (UnionI S y A HyA HAinS).
An exact proof term for the current goal is HSprop.
∎