Let X and Tx be given.
Assume Hscc: second_countable_space X Tx.
We will prove first_countable_space 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 ∧ ∀x : set, x ∈ X → countable_basis_at X Tx x.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We will prove countable_basis_at X Tx x.
We will prove topology_on X Tx ∧ x ∈ X ∧ ∃B0 : set, B0 ⊆ Tx ∧ countable_set B0 ∧ (∀b : set, b ∈ B0 → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B0 ∧ b ⊆ U).
Apply and3I to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HxX.
Apply HexB to the current goal.
Let B be given.
Assume HBpair.
Set B0 to be the term {b ∈ B|x ∈ b}.
We use B0 to witness the existential quantifier.
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).
We prove the intermediate claim HBsubPow: B ⊆ 𝒫 X.
An exact proof term for the current goal is (basis_on_sub_Power X B HBasis).
Apply and4I to the current goal.
Let u be given.
Assume Hu0: u ∈ B0.
We will prove u ∈ Tx.
We prove the intermediate claim HuB: u ∈ B.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ x ∈ b0) u Hu0).
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 Husub: u ⊆ X.
An exact proof term for the current goal is (PowerE X u HuPow).
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.
We prove the intermediate claim HB0sub: B0 ⊆ B.
Let u be given.
Assume Hu0: u ∈ B0.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ x ∈ b0) u Hu0).
An exact proof term for the current goal is (Subq_countable B0 B HBcount HB0sub).
Let u be given.
Assume Hu0: u ∈ B0.
An exact proof term for the current goal is (SepE2 B (λb0 : set ⇒ x ∈ b0) u Hu0).
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove ∃b : set, b ∈ B0 ∧ b ⊆ U.
We prove the intermediate claim HUtop: 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 Hexb2: ∃b : set, b ∈ B ∧ x ∈ b ∧ b ⊆ U.
Apply (generated_topology_local_refine X B U x HUtop HxU) to the current goal.
Let b be given.
Assume Hbpair.
We use b to witness the existential quantifier.
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 Hbrest: 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) Hbrest).
We prove the intermediate claim Hbsub: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbrest).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is Hbsub.
Apply Hexb2 to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim Hbpair1: b ∈ B ∧ x ∈ b.
An exact proof term for the current goal is (andEL (b ∈ B ∧ x ∈ b) (b ⊆ U) Hbpair).
We prove the intermediate claim Hbsub: b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B ∧ x ∈ b) (b ⊆ U) Hbpair).
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b) Hbpair1).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b) Hbpair1).
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (SepI B (λb0 : set ⇒ x ∈ b0) b HbB Hxb).
An exact proof term for the current goal is Hbsub.
∎