Let X, Tx, W and f be given.
Assume HWlf: locally_finite_family X Tx W.
Assume Hsub: ∀w : set, w ∈ W → f w ⊆ w.
We will prove locally_finite_family X Tx {f w|w ∈ W}.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ {f w|w ∈ W} ∧ ∀A : set, A ∈ {f w|w ∈ W} → A ∩ N ≠ Empty → A ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is (locally_finite_family_topology X Tx W HWlf).
Let x be given.
Assume HxX: x ∈ X.
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 use N to witness the existential quantifier.
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 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 andI to the current goal.
An exact proof term for the current goal is HNpair.
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.
Set S to be the term {f w|w ∈ S0}.
We use S to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HS0fin: finite S0.
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 (Repl_finite (λw0 : set ⇒ f w0) S0 HS0fin).
Let y be given.
Assume Hy: y ∈ S.
Apply (ReplE_impred S0 (λw0 : set ⇒ f w0) y Hy (y ∈ {f w|w ∈ W})) to the current goal.
Let w be given.
Assume HwS0: w ∈ S0.
Assume Heq: y = f w.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HS0subW: S0 ⊆ W.
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)).
An exact proof term for the current goal is (ReplI W (λw0 : set ⇒ f w0) w (HS0subW w HwS0)).
Let A be given.
Assume HA: A ∈ {f w|w ∈ W}.
Assume HAint: A ∩ N ≠ Empty.
Apply (ReplE_impred W (λw0 : set ⇒ f w0) A HA (A ∈ S)) to the current goal.
Let w be given.
Assume HwW: w ∈ W.
Assume HeqA: A = f w.
We prove the intermediate claim HAsubw: A ⊆ w.
rewrite the current goal using HeqA (from left to right).
An exact proof term for the current goal is (Hsub w HwW).
We prove the intermediate claim HwN: w ∩ N ≠ Empty.
We prove the intermediate claim Hexz: ∃z : set, z ∈ A ∩ N.
An exact proof term for the current goal is (nonempty_has_element (A ∩ N) HAint).
Apply Hexz to the current goal.
Let z be given.
Assume Hz: z ∈ A ∩ N.
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (binintersectE1 A N z Hz).
We prove the intermediate claim HzN: z ∈ N.
An exact proof term for the current goal is (binintersectE2 A N z Hz).
We prove the intermediate claim Hzw: z ∈ w.
An exact proof term for the current goal is (HAsubw z HzA).
An exact proof term for the current goal is (elem_implies_nonempty (w ∩ N) z (binintersectI w N z Hzw HzN)).
We prove the intermediate claim HwS0: w ∈ S0.
An exact proof term for the current goal is (andER (finite S0 ∧ S0 ⊆ W) (∀A0 : set, A0 ∈ W → A0 ∩ N ≠ Empty → A0 ∈ S0) HS0 w HwW HwN).
rewrite the current goal using HeqA (from left to right).
An exact proof term for the current goal is (ReplI S0 (λw0 : set ⇒ f w0) w HwS0).
∎