Let X, Tx and F be given.
Assume HTx: topology_on X Tx.
Assume HFsub: F ⊆ 𝒫 X.
Assume Hlf: locally_finite_family X Tx F.
We will prove sigma_locally_finite_family X Tx F.
We will prove topology_on X Tx ∧ ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀G : set, G ∈ Fams → locally_finite_family X Tx G) ∧ F = ⋃ Fams.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Set Fams to be the term Sing F.
We use Fams to witness the existential quantifier.
Apply and4I to the current goal.
We will prove countable_set Fams.
We will prove countable Fams.
An exact proof term for the current goal is (finite_countable Fams (Sing_finite F)).
We will prove Fams ⊆ 𝒫 (𝒫 X).
Let G be given.
Assume HG: G ∈ Fams.
We will prove G ∈ 𝒫 (𝒫 X).
We prove the intermediate claim HeqG: G = F.
An exact proof term for the current goal is (SingE F G HG).
rewrite the current goal using HeqG (from left to right).
An exact proof term for the current goal is (PowerI (𝒫 X) F HFsub).
Let G be given.
Assume HG: G ∈ Fams.
We will prove locally_finite_family X Tx G.
We prove the intermediate claim HeqG: G = F.
An exact proof term for the current goal is (SingE F G HG).
rewrite the current goal using HeqG (from left to right).
An exact proof term for the current goal is Hlf.
We will prove F = ⋃ Fams.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ F.
We will prove f ∈ ⋃ Fams.
An exact proof term for the current goal is (UnionI Fams f F Hf (SingI F)).
Let f be given.
Assume Hf: f ∈ ⋃ Fams.
We will prove f ∈ F.
Apply (UnionE_impred Fams f Hf (f ∈ F)) to the current goal.
Let G be given.
Assume HfG: f ∈ G.
Assume HGF: G ∈ Fams.
We prove the intermediate claim HeqG: G = F.
An exact proof term for the current goal is (SingE F G HGF).
rewrite the current goal using HeqG (from right to left).
An exact proof term for the current goal is HfG.
∎