Let X and Tx be given.
Assume HTx: topology_on X Tx.
Assume Hscc: second_countable_space X Tx.
Let U be given.
Assume HU: open_cover X Tx U.
We will prove ∃V : set, countable_subcollection V U ∧ covers X V.
We prove the intermediate claim HUopen: ∀u : set, u ∈ U → u ∈ Tx.
An exact proof term for the current goal is (andEL (∀u : set, u ∈ U → u ∈ Tx) (covers X U) HU).
We prove the intermediate claim HUcov: covers X U.
An exact proof term for the current goal is (andER (∀u : set, u ∈ U → u ∈ Tx) (covers X U) HU).
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 B0 to be the term {b ∈ B|∃u : set, u ∈ U ∧ b ⊆ u}.
Set choose to be the term λb ⇒ Eps_i (λu ⇒ u ∈ U ∧ b ⊆ u) of type set → set.
Set V to be the term {choose b|b ∈ B0}.
We use V to witness the existential quantifier.
Apply andI to the current goal.
We will prove countable_subcollection V U.
We will prove V ⊆ U ∧ countable_set V.
Apply andI to the current goal.
Let v be given.
Assume Hv: v ∈ V.
We will prove v ∈ U.
Apply (ReplE_impred B0 choose v Hv) to the current goal.
Let b be given.
Assume Hb0: b ∈ B0.
Assume HvEq: v = choose b.
We prove the intermediate claim Hb0prop: ∃u : set, u ∈ U ∧ b ⊆ u.
An exact proof term for the current goal is (SepE2 B (λb0 : set ⇒ ∃u : set, u ∈ U ∧ b0 ⊆ u) b Hb0).
Apply Hb0prop to the current goal.
Let u be given.
Assume Hupair: u ∈ U ∧ b ⊆ u.
We prove the intermediate claim Hchooseprop: choose b ∈ U ∧ b ⊆ choose b.
An exact proof term for the current goal is (Eps_i_ax (λu0 ⇒ u0 ∈ U ∧ b ⊆ u0) u Hupair).
We prove the intermediate claim HchooseU: choose b ∈ U.
An exact proof term for the current goal is (andEL (choose b ∈ U) (b ⊆ choose b) Hchooseprop).
rewrite the current goal using HvEq (from left to right).
An exact proof term for the current goal is HchooseU.
We prove the intermediate claim HB0sub: B0 ⊆ B.
Let b be given.
Assume Hb0: b ∈ B0.
An exact proof term for the current goal is (SepE1 B (λb0 : set ⇒ ∃u : set, u ∈ U ∧ b0 ⊆ u) b Hb0).
We prove the intermediate claim HB0count: countable_set B0.
An exact proof term for the current goal is (Subq_countable B0 B HBcount HB0sub).
An exact proof term for the current goal is (countable_image B0 HB0count choose).
We will prove covers X V.
Let x be given.
Assume HxX: x ∈ X.
Apply (HUcov x HxX) to the current goal.
Let u be given.
Assume Hupair.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (x ∈ u) Hupair).
We prove the intermediate claim Hxu: x ∈ u.
An exact proof term for the current goal is (andER (u ∈ U) (x ∈ u) Hupair).
We prove the intermediate claim HuTx: u ∈ Tx.
An exact proof term for the current goal is (HUopen u HuU).
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 HuTx.
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 Hb0: b ∈ B0.
Apply (SepI B (λb0 : set ⇒ ∃u0 : set, u0 ∈ U ∧ b0 ⊆ u0) b HbB) to the current goal.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
An exact proof term for the current goal is Hbsubu.
We prove the intermediate claim Hchooseprop: choose b ∈ U ∧ b ⊆ choose b.
An exact proof term for the current goal is (Eps_i_ax (λu0 ⇒ u0 ∈ U ∧ b ⊆ u0) u (andI (u ∈ U) (b ⊆ u) HuU Hbsubu)).
We prove the intermediate claim Hbsubchoose: b ⊆ choose b.
An exact proof term for the current goal is (andER (choose b ∈ U) (b ⊆ choose b) Hchooseprop).
We prove the intermediate claim Hxchoose: x ∈ choose b.
An exact proof term for the current goal is (Hbsubchoose x Hxb).
We use choose b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (ReplI B0 choose b Hb0).
An exact proof term for the current goal is Hxchoose.
∎