Let X and Tx be given.
Assume HTx: topology_on X Tx.
Assume Hscc: second_countable_space X Tx.
We will prove ∃D : set, countable_set D ∧ dense_in D X Tx.
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).
Apply HexB to the current goal.
Let B be given.
Assume HBpair.
We prove the intermediate claim HBmid: (basis_on X B ∧ countable_set B) ∧ basis_generates X B Tx.
An exact proof term for the current goal is HBpair.
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) HBmid).
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) HBmid).
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).
Set B1 to be the term {b ∈ B|b ≠ Empty}.
Set pick to be the term λb ⇒ Eps_i (λx ⇒ x ∈ b) of type set → set.
Set D to be the term {pick b|b ∈ B1}.
We use D to witness the existential quantifier.
Apply andI to the current goal.
We will prove countable_set D.
We prove the intermediate claim HB1sub: B1 ⊆ B.
Let b be given.
Assume Hb1: b ∈ B1.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ b0 ≠ Empty) b Hb1).
We prove the intermediate claim HB1count: countable_set B1.
An exact proof term for the current goal is (Subq_countable B1 B HBcount HB1sub).
An exact proof term for the current goal is (countable_image B1 HB1count pick).
We will prove dense_in D X Tx.
We will prove closure_of X Tx D = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space X Tx D HTx).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ closure_of X Tx D.
We prove the intermediate claim Hcliff: x ∈ closure_of X Tx D ↔ (∀U ∈ Tx, x ∈ U → U ∩ D ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx D x HTx HxX).
We prove the intermediate claim Hneigh: ∀U ∈ Tx, x ∈ U → U ∩ D ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim Href: ∀z ∈ U, ∃b ∈ B, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀z ∈ U0, ∃b ∈ B, z ∈ b ∧ b ⊆ U0) U HUgen).
We prove the intermediate claim Hexb: ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (Href x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim Hbne: b ≠ Empty.
Assume HbE: b = Empty.
We prove the intermediate claim HxEmp: x ∈ Empty.
rewrite the current goal using HbE (from right to left).
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is (EmptyE x HxEmp False).
We prove the intermediate claim Hb1: b ∈ B1.
An exact proof term for the current goal is (SepI B (λb0 : set ⇒ b0 ≠ Empty) b HbB Hbne).
We prove the intermediate claim Hpickb: pick b ∈ b.
An exact proof term for the current goal is (Eps_i_ax (λx0 ⇒ x0 ∈ b) x Hxb).
We prove the intermediate claim HpickU: pick b ∈ U.
An exact proof term for the current goal is (HbsubU (pick b) Hpickb).
We prove the intermediate claim HpickD: pick b ∈ D.
An exact proof term for the current goal is (ReplI B1 pick b Hb1).
We will prove U ∩ D ≠ Empty.
Assume HUD: U ∩ D = Empty.
We prove the intermediate claim Hwd: pick b ∈ U ∩ D.
An exact proof term for the current goal is (binintersectI U D (pick b) HpickU HpickD).
We prove the intermediate claim HwdE: pick b ∈ Empty.
rewrite the current goal using HUD (from right to left).
An exact proof term for the current goal is Hwd.
An exact proof term for the current goal is (EmptyE (pick b) HwdE False).
An exact proof term for the current goal is (iffER (x ∈ closure_of X Tx D) (∀U ∈ Tx, x ∈ U → U ∩ D ≠ Empty) Hcliff Hneigh).
∎