Let X, Tx and Fam be given.
Assume HLF: locally_finite_family X Tx Fam.
We will prove locally_finite_family X Tx {closure_of X Tx A|A ∈ Fam}.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HLF).
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ {closure_of X Tx A|A ∈ Fam} ∧ ∀C : set, C ∈ {closure_of X Tx A|A ∈ Fam} → C ∩ N ≠ Empty → C ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hex: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0) HLF x HxX).
Apply Hex to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S0 : set, finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0.
We prove the intermediate claim HNcore: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃S0 : set, finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → 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) HNcore).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HNcore).
We prove the intermediate claim HexS0: ∃S0 : set, finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S0 : set, finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0) HNpack).
Apply HexS0 to the current goal.
Let S0 be given.
Assume HS0: finite S0 ∧ S0 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0.
We prove the intermediate claim HS0left: finite S0 ∧ S0 ⊆ Fam.
An exact proof term for the current goal is (andEL (finite S0 ∧ S0 ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0) HS0).
We prove the intermediate claim HS0fin: finite S0.
An exact proof term for the current goal is (andEL (finite S0) (S0 ⊆ Fam) HS0left).
We prove the intermediate claim HS0subFam: S0 ⊆ Fam.
An exact proof term for the current goal is (andER (finite S0) (S0 ⊆ Fam) HS0left).
We prove the intermediate claim HS0prop: ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0.
An exact proof term for the current goal is (andER (finite S0 ∧ S0 ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S0) HS0).
Set S to be the term Repl S0 (λA : set ⇒ closure_of X Tx A).
We use N 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 HNTx.
An exact proof term for the current goal is HxN.
We use S 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 (Repl_finite (λA : set ⇒ closure_of X Tx A) S0 HS0fin).
Let C be given.
Assume HC: C ∈ S.
Apply (ReplE_impred S0 (λA : set ⇒ closure_of X Tx A) C HC (C ∈ {closure_of X Tx A|A ∈ Fam})) to the current goal.
Let A be given.
Assume HA0: A ∈ S0.
Assume HeqC: C = closure_of X Tx A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HS0subFam A HA0).
rewrite the current goal using HeqC (from left to right).
An exact proof term for the current goal is (ReplI Fam (λA0 : set ⇒ closure_of X Tx A0) A HAFam).
Let C be given.
Assume HCCl: C ∈ {closure_of X Tx A|A ∈ Fam}.
Assume HCmeet: C ∩ N ≠ Empty.
Apply (ReplE_impred Fam (λA : set ⇒ closure_of X Tx A) C HCCl (C ∈ S)) to the current goal.
Let A be given.
Assume HAFam: A ∈ Fam.
Assume HeqC: C = closure_of X Tx A.
We prove the intermediate claim HAmeetCl: N ∩ closure_of X Tx A ≠ Empty.
rewrite the current goal using (binintersect_com N (closure_of X Tx A)) (from left to right).
rewrite the current goal using HeqC (from right to left).
An exact proof term for the current goal is HCmeet.
We prove the intermediate claim HAmeet: A ∩ N ≠ Empty.
rewrite the current goal using (binintersect_com A N) (from left to right).
An exact proof term for the current goal is (open_intersects_closure_implies_intersects X Tx A N HTx HNTx HAmeetCl).
We prove the intermediate claim HAinS0: A ∈ S0.
An exact proof term for the current goal is (HS0prop A HAFam HAmeet).
rewrite the current goal using HeqC (from left to right).
An exact proof term for the current goal is (ReplI S0 (λA0 : set ⇒ closure_of X Tx A0) A HAinS0).
∎