Let X, Tx, Fam and S be given.
Assume HLFam: locally_finite_family X Tx Fam.
Assume HClosedFam: ∀A : set, A ∈ Fam → closed_in X Tx A.
Assume HSsub: S ⊆ Fam.
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 Fam HLFam).
We prove the intermediate claim HLS: locally_finite_family X Tx S.
An exact proof term for the current goal is (locally_finite_subfamily X Tx Fam S HLFam HSsub).
We prove the intermediate claim HSsubX: ∀A : set, A ∈ S → A ⊆ X.
Let A be given.
Assume HAS: A ∈ S.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsub A HAS).
We prove the intermediate claim HAclosed: closed_in X Tx A.
An exact proof term for the current goal is (HClosedFam A HAFam).
We prove the intermediate claim HAand: A ⊆ X ∧ ∃U ∈ Tx, A = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (A ⊆ X ∧ ∃U ∈ Tx, A = X ∖ U) HAclosed).
An exact proof term for the current goal is (andEL (A ⊆ X) (∃U ∈ Tx, A = X ∖ U) HAand).
We prove the intermediate claim HUnionSubX: ⋃ S ⊆ X.
Let x be given.
Assume HxU: x ∈ ⋃ S.
Apply (UnionE S x HxU) to the current goal.
Let A be given.
Assume HApack: x ∈ A ∧ A ∈ S.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (andEL (x ∈ A) (A ∈ S) HApack).
We prove the intermediate claim HAS: A ∈ S.
An exact proof term for the current goal is (andER (x ∈ A) (A ∈ S) HApack).
An exact proof term for the current goal is (HSsubX A HAS x HxA).
We prove the intermediate claim HclUsub: closure_of X Tx (⋃ S) ⊆ ⋃ {closure_of X Tx A|A ∈ S}.
An exact proof term for the current goal is (closure_Union_locally_finite_subset_Union_closures X Tx S HSsubX HLS).
We prove the intermediate claim HUnionClSub: ⋃ {closure_of X Tx A|A ∈ S} ⊆ ⋃ S.
Let x be given.
Assume Hx: x ∈ ⋃ {closure_of X Tx A|A ∈ S}.
Apply (UnionE_impred {closure_of X Tx A|A ∈ S} x Hx (x ∈ ⋃ S)) to the current goal.
Let Y be given.
Assume HxY: x ∈ Y.
Assume HY: Y ∈ {closure_of X Tx A|A ∈ S}.
Apply (ReplE_impred S (λA0 : set ⇒ closure_of X Tx A0) Y HY (x ∈ ⋃ S)) to the current goal.
Let A be given.
Assume HAS: A ∈ S.
Assume HYe: Y = closure_of X Tx A.
We prove the intermediate claim HAFam: A ∈ Fam.
An exact proof term for the current goal is (HSsub A HAS).
We prove the intermediate claim HAclosed: closed_in X Tx A.
An exact proof term for the current goal is (HClosedFam A HAFam).
We prove the intermediate claim HclEq: closure_of X Tx A = A.
An exact proof term for the current goal is (closed_closure_eq X Tx A HTx HAclosed).
We prove the intermediate claim HxClA: x ∈ closure_of X Tx A.
rewrite the current goal using HYe (from right to left).
An exact proof term for the current goal is HxY.
We prove the intermediate claim HxA: x ∈ A.
rewrite the current goal using HclEq (from right to left).
An exact proof term for the current goal is HxClA.
An exact proof term for the current goal is (UnionI S x A HxA HAS).
We prove the intermediate claim HclEqU: closure_of X Tx (⋃ S) = ⋃ S.
Apply set_ext to the current goal.
We will prove closure_of X Tx (⋃ S) ⊆ ⋃ S.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx (⋃ S)) (⋃ {closure_of X Tx A|A ∈ S}) (⋃ S) HclUsub HUnionClSub).
We will prove ⋃ S ⊆ closure_of X Tx (⋃ S).
An exact proof term for the current goal is (closure_contains_set X Tx (⋃ S) HTx HUnionSubX).
We will prove closed_in X Tx (⋃ S).
rewrite the current goal using HclEqU (from right to left).
An exact proof term for the current goal is (closure_is_closed X Tx (⋃ S) HTx HUnionSubX).
∎