Let X, Tx and Fam be given.
Assume HLF: locally_finite_family X Tx Fam.
Set ClFam to be the term {closure_of X Tx A|A ∈ Fam}.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ ClFam ∧ ∀C : set, C ∈ ClFam → C ∩ N ≠ Empty → C ∈ S.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HLF).
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 Hprop: ∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HLF).
We prove the intermediate claim HexN: ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (Hprop x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → 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 ⊆ Fam ∧ ∀A : set, A ∈ Fam → 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 ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HNpack).
Apply HexS to the current goal.
Let S be given.
Assume HS: finite S ∧ S ⊆ Fam ∧ ∀A : set, A ∈ Fam → 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 ⊆ Fam) (andEL (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS)).
We prove the intermediate claim HSsubFam: S ⊆ Fam.
An exact proof term for the current goal is (andER (finite S) (S ⊆ Fam) (andEL (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS)).
We prove the intermediate claim HSprop: ∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (andER (finite S ∧ S ⊆ Fam) (∀A : set, A ∈ Fam → A ∩ N ≠ Empty → A ∈ S) HS).
Set SCl to be the term {closure_of X Tx A|A ∈ S}.
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 SCl 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 (finite_Repl S HSfin (λA : set ⇒ closure_of X Tx A)).
Let C be given.
Assume HC: C ∈ SCl.
We will prove C ∈ ClFam.
Apply (ReplE_impred S (λA : set ⇒ closure_of X Tx A) C HC) to the current goal.
Let A be given.
Assume HA: A ∈ S.
Assume HCeq: C = closure_of X Tx A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsubFam A HA).
rewrite the current goal using HCeq (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 HC: C ∈ ClFam.
Assume HCN: C ∩ N ≠ Empty.
We will prove C ∈ SCl.
Apply (ReplE_impred Fam (λA : set ⇒ closure_of X Tx A) C HC) to the current goal.
Let A be given.
Assume HAFam: A ∈ Fam.
Assume HCeq: C = closure_of X Tx A.
We prove the intermediate claim Hexy: ∃y : set, y ∈ C ∩ N.
An exact proof term for the current goal is (nonempty_has_element (C ∩ N) HCN).
Apply Hexy to the current goal.
Let y be given.
Assume HyCap: y ∈ C ∩ N.
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (binintersectE1 C N y HyCap).
We prove the intermediate claim HyN: y ∈ N.
An exact proof term for the current goal is (binintersectE2 C N y HyCap).
We prove the intermediate claim HyClA: y ∈ closure_of X Tx A.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is HyC.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∀U : set, U ∈ Tx → y0 ∈ U → U ∩ A ≠ Empty) y HyClA).
We prove the intermediate claim Hiff: y ∈ closure_of X Tx A ↔ (∀U ∈ Tx, y ∈ U → U ∩ A ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx A y HTx HyX).
We prove the intermediate claim HyProp: ∀U ∈ Tx, y ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (iffEL (y ∈ closure_of X Tx A) (∀U ∈ Tx, y ∈ U → U ∩ A ≠ Empty) Hiff HyClA).
We prove the intermediate claim HANe: 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 (HyProp N HNTx HyN).
We prove the intermediate claim HAinS: A ∈ S.
An exact proof term for the current goal is (HSprop A HAFam HANe).
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (ReplI S (λA0 : set ⇒ closure_of X Tx A0) A HAinS).
∎