Let X and Tx be given.
Assume Hlfb: locally_finite_basis X Tx.
We will prove sigma_locally_finite_basis X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∃B : set, basis_generates X B Tx ∧ locally_finite_family X Tx B ∧ (∀b : set, b ∈ B → b ∈ Tx)) Hlfb).
We will prove topology_on X Tx ∧ ∃Fams : set, countable_set Fams ∧ Fams ⊆ 𝒫 (𝒫 X) ∧ (∀F : set, F ∈ Fams → locally_finite_family X Tx F) ∧ basis_generates X (⋃ Fams) Tx ∧ ∀b : set, b ∈ ⋃ Fams → b ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We prove the intermediate claim HexB: ∃B : set, basis_generates X B Tx ∧ locally_finite_family X Tx B ∧ (∀b : set, b ∈ B → b ∈ Tx).
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_generates X B Tx ∧ locally_finite_family X Tx B ∧ (∀b : set, b ∈ B → b ∈ Tx)) Hlfb).
Apply HexB to the current goal.
Let B be given.
Assume HB: basis_generates X B Tx ∧ locally_finite_family X Tx B ∧ (∀b : set, b ∈ B → b ∈ Tx).
We prove the intermediate claim HBpair: basis_generates X B Tx ∧ locally_finite_family X Tx B.
An exact proof term for the current goal is (andEL (basis_generates X B Tx ∧ locally_finite_family X Tx B) (∀b : set, b ∈ B → b ∈ Tx) HB).
We prove the intermediate claim HBgen: basis_generates X B Tx.
An exact proof term for the current goal is (andEL (basis_generates X B Tx) (locally_finite_family X Tx B) HBpair).
We prove the intermediate claim HBlf: locally_finite_family X Tx B.
An exact proof term for the current goal is (andER (basis_generates X B Tx) (locally_finite_family X Tx B) HBpair).
We prove the intermediate claim HBbasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (generated_topology X B = Tx) HBgen).
We prove the intermediate claim HBopen: ∀b : set, b ∈ B → b ∈ Tx.
An exact proof term for the current goal is (andER (basis_generates X B Tx ∧ locally_finite_family X Tx B) (∀b : set, b ∈ B → b ∈ Tx) HB).
Set Fams to be the term Sing B.
We use Fams to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI 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 B)).
We will prove Fams ⊆ 𝒫 (𝒫 X).
Let F be given.
Assume HF: F ∈ Fams.
We will prove F ∈ 𝒫 (𝒫 X).
We prove the intermediate claim HeqF: F = B.
An exact proof term for the current goal is (SingE B F HF).
rewrite the current goal using HeqF (from left to right).
We prove the intermediate claim HBsub: B ⊆ 𝒫 X.
An exact proof term for the current goal is (basis_on_sub_Power X B HBbasis).
An exact proof term for the current goal is (PowerI (𝒫 X) B HBsub).
Let F be given.
Assume HF: F ∈ Fams.
We will prove locally_finite_family X Tx F.
We prove the intermediate claim HeqF: F = B.
An exact proof term for the current goal is (SingE B F HF).
rewrite the current goal using HeqF (from left to right).
An exact proof term for the current goal is HBlf.
We will prove basis_generates X (⋃ Fams) Tx.
We prove the intermediate claim HUnionEq: ⋃ Fams = B.
Apply (set_ext (⋃ Fams) B) to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ Fams.
Apply (UnionE_impred Fams y Hy (y ∈ B)) to the current goal.
Let Y be given.
Assume HyY: y ∈ Y.
Assume HYF: Y ∈ Fams.
We prove the intermediate claim HeqY: Y = B.
An exact proof term for the current goal is (SingE B Y HYF).
rewrite the current goal using HeqY (from right to left).
An exact proof term for the current goal is HyY.
Let y be given.
Assume Hy: y ∈ B.
An exact proof term for the current goal is (UnionI Fams y B Hy (SingI B)).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HBgen.
Let b be given.
Assume Hb: b ∈ ⋃ Fams.
We will prove b ∈ Tx.
We prove the intermediate claim HUnionEq: ⋃ Fams = B.
Apply (set_ext (⋃ Fams) B) to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ Fams.
Apply (UnionE_impred Fams y Hy (y ∈ B)) to the current goal.
Let Y be given.
Assume HyY: y ∈ Y.
Assume HYF: Y ∈ Fams.
We prove the intermediate claim HeqY: Y = B.
An exact proof term for the current goal is (SingE B Y HYF).
rewrite the current goal using HeqY (from right to left).
An exact proof term for the current goal is HyY.
Let y be given.
Assume Hy: y ∈ B.
An exact proof term for the current goal is (UnionI Fams y B Hy (SingI B)).
We prove the intermediate claim HbB: b ∈ B.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is (HBopen b HbB).
∎