Let X and Tx be given.
Assume Hscc: second_countable_space 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_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hscc).
We prove the intermediate claim HexB: ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hscc).
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.
Apply HexB to the current goal.
Let B be given.
Assume HB: basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
Set Fams to be the term {{b}|b ∈ B}.
We use Fams to witness the existential quantifier.
We prove the intermediate claim HB12: (basis_on X B ∧ countable_set B) ∧ basis_generates X B Tx.
An exact proof term for the current goal is HB.
We prove the intermediate claim HBasisCount: basis_on X B ∧ countable_set B.
An exact proof term for the current goal is (andEL (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HB12).
We prove the intermediate claim HBgener: basis_generates X B Tx.
An exact proof term for the current goal is (andER (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HB12).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (countable_set B) HBasisCount).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (andER (basis_on X B) (countable_set B) HBasisCount).
We prove the intermediate claim HgenEq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) HBgener).
We prove the intermediate claim HBsubPow: B ⊆ 𝒫 X.
An exact proof term for the current goal is (basis_on_sub_Power X B HBasis).
We prove the intermediate claim HUnionEq: ⋃ Fams = B.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ ⋃ Fams.
We will prove u ∈ B.
Apply (UnionE_impred Fams u Hu (u ∈ B)) to the current goal.
Let G be given.
Assume HuG: u ∈ G.
Assume HGF: G ∈ Fams.
Apply (ReplE_impred B (λb0 : set ⇒ {b0}) G HGF) to the current goal.
Let u0 be given.
Assume Hu0B: u0 ∈ B.
Assume HeqG: G = {u0}.
We prove the intermediate claim HuEq: u = u0.
We prove the intermediate claim HuG0: u ∈ {u0}.
rewrite the current goal using HeqG (from right to left).
An exact proof term for the current goal is HuG.
An exact proof term for the current goal is (SingE u0 u HuG0).
rewrite the current goal using HuEq (from left to right).
An exact proof term for the current goal is Hu0B.
Let u be given.
Assume HuB: u ∈ B.
We will prove u ∈ ⋃ Fams.
We prove the intermediate claim HuFam: {u} ∈ Fams.
An exact proof term for the current goal is (ReplI B (λb0 : set ⇒ {b0}) u HuB).
An exact proof term for the current goal is (UnionI Fams u {u} (SingI u) HuFam).
We will prove 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 and5I to the current goal.
An exact proof term for the current goal is (countable_image B HBcount (λb : set ⇒ {b})).
We will prove Fams ⊆ 𝒫 (𝒫 X).
Let G be given.
Assume HG: G ∈ Fams.
We will prove G ∈ 𝒫 (𝒫 X).
Apply (ReplE_impred B (λb : set ⇒ {b}) G HG) to the current goal.
Let u be given.
Assume HuB: u ∈ B.
Assume HeqG: G = {u}.
rewrite the current goal using HeqG (from left to right).
We prove the intermediate claim HuPow: u ∈ 𝒫 X.
An exact proof term for the current goal is (HBsubPow u HuB).
We prove the intermediate claim HsubPow: {u} ⊆ 𝒫 X.
Let z be given.
Assume Hz: z ∈ {u}.
We will prove z ∈ 𝒫 X.
We prove the intermediate claim Hzu: z = u.
An exact proof term for the current goal is (SingE u z Hz).
rewrite the current goal using Hzu (from left to right).
An exact proof term for the current goal is HuPow.
An exact proof term for the current goal is (PowerI (𝒫 X) {u} HsubPow).
Let G be given.
Assume HG: G ∈ Fams.
We will prove locally_finite_family X Tx G.
Apply (ReplE_impred B (λb : set ⇒ {b}) G HG) to the current goal.
Let u be given.
Assume HuB: u ∈ B.
Assume HeqG: G = {u}.
rewrite the current goal using HeqG (from left to right).
An exact proof term for the current goal is (finite_family_locally_finite_family X Tx {u} HTx (Sing_finite u)).
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is HBgener.
Let u be given.
Assume HuFam: u ∈ ⋃ Fams.
We will prove u ∈ Tx.
We prove the intermediate claim HuB: u ∈ B.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HuFam.
We prove the intermediate claim HuPow: u ∈ 𝒫 X.
An exact proof term for the current goal is (HBsubPow u HuB).
We prove the intermediate claim HuTop: u ∈ generated_topology X B.
An exact proof term for the current goal is (generated_topology_contains_elem X B u HuPow HuB).
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HuTop.
∎