Let X, Tx and A be given.
Assume Hsc: second_countable_space X Tx.
Assume Hdisc: discrete_subspace X Tx A.
We will prove countable_set A.
We prove the intermediate claim HAcX: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∀a : set, a ∈ A → ∃U : set, U ∈ Tx ∧ U ∩ A = {a}) Hdisc).
We prove the intermediate claim HdiscU: ∀a : set, a ∈ A → ∃U : set, U ∈ Tx ∧ U ∩ A = {a}.
An exact proof term for the current goal is (andER (A ⊆ X) (∀a : set, a ∈ A → ∃U : set, U ∈ Tx ∧ U ∩ A = {a}) Hdisc).
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) Hsc).
Apply HexB to the current goal.
Let B be given.
Assume 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) HBpair).
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 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) HBpair).
We prove the intermediate claim HTxeq: 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 pick to be the term (λa : set ⇒ Eps_i (λb : set ⇒ b ∈ B ∧ ∃U : set, U ∈ Tx ∧ (U ∩ A = {a} ∧ (a ∈ b ∧ b ⊆ U)))).
We prove the intermediate claim HpickP: ∀a : set, a ∈ A → (λb : set ⇒ b ∈ B ∧ ∃U : set, U ∈ Tx ∧ (U ∩ A = {a} ∧ (a ∈ b ∧ b ⊆ U))) (pick a).
Let a be given.
Assume Ha: a ∈ A.
We will prove (λb : set ⇒ b ∈ B ∧ ∃U : set, U ∈ Tx ∧ (U ∩ A = {a} ∧ (a ∈ b ∧ b ⊆ U))) (pick a).
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ U ∩ A = {a}.
An exact proof term for the current goal is (HdiscU a Ha).
Apply HexU to the current goal.
Let U be given.
Assume HUpair.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (U ∩ A = {a}) HUpair).
We prove the intermediate claim HUA: U ∩ A = {a}.
An exact proof term for the current goal is (andER (U ∈ Tx) (U ∩ A = {a}) HUpair).
We prove the intermediate claim HUinGen: U ∈ generated_topology X B.
rewrite the current goal using HTxeq (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUbasis: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HUinGen).
We prove the intermediate claim HainUA: a ∈ U ∩ A.
rewrite the current goal using HUA (from left to right).
An exact proof term for the current goal is (SingI a).
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (binintersectE1 U A a HainUA).
We prove the intermediate claim Hexb: ∃b ∈ B, a ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUbasis a HaU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair2.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (a ∈ b ∧ b ⊆ U) Hbpair2).
We prove the intermediate claim Habsub: a ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (a ∈ b ∧ b ⊆ U) Hbpair2).
We prove the intermediate claim Hab: a ∈ b.
An exact proof term for the current goal is (andEL (a ∈ b) (b ⊆ U) Habsub).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (a ∈ b) (b ⊆ U) Habsub).
We prove the intermediate claim Hwit0: b ∈ B ∧ ∃U0 : set, U0 ∈ Tx ∧ (U0 ∩ A = {a} ∧ (a ∈ b ∧ b ⊆ U0)).
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
Apply andI to the current goal.
An exact proof term for the current goal is HUA.
Apply andI to the current goal.
An exact proof term for the current goal is Hab.
An exact proof term for the current goal is HbsubU.
An exact proof term for the current goal is (Eps_i_ax (λb0 : set ⇒ b0 ∈ B ∧ ∃U0 : set, U0 ∈ Tx ∧ (U0 ∩ A = {a} ∧ (a ∈ b0 ∧ b0 ⊆ U0))) b Hwit0).
We prove the intermediate claim HinjAB: inj A B pick.
We will prove (∀a ∈ A, pick a ∈ B) ∧ (∀a0 a1 ∈ A, pick a0 = pick a1 → a0 = a1).
Apply andI to the current goal.
Let a be given.
Assume Ha: a ∈ A.
We will prove pick a ∈ B.
We prove the intermediate claim Hp: (λb : set ⇒ b ∈ B ∧ ∃U : set, U ∈ Tx ∧ (U ∩ A = {a} ∧ (a ∈ b ∧ b ⊆ U))) (pick a).
An exact proof term for the current goal is (HpickP a Ha).
An exact proof term for the current goal is (andEL (pick a ∈ B) (∃U : set, U ∈ Tx ∧ (U ∩ A = {a} ∧ (a ∈ pick a ∧ pick a ⊆ U))) Hp).
Let a0 be given.
Assume Ha0: a0 ∈ A.
Let a1 be given.
Assume Ha1: a1 ∈ A.
Assume Heq: pick a0 = pick a1.
We will prove a0 = a1.
We prove the intermediate claim Hp0: (λb : set ⇒ b ∈ B ∧ ∃U : set, U ∈ Tx ∧ (U ∩ A = {a0} ∧ (a0 ∈ b ∧ b ⊆ U))) (pick a0).
An exact proof term for the current goal is (HpickP a0 Ha0).
We prove the intermediate claim Hp1: (λb : set ⇒ b ∈ B ∧ ∃U : set, U ∈ Tx ∧ (U ∩ A = {a1} ∧ (a1 ∈ b ∧ b ⊆ U))) (pick a1).
An exact proof term for the current goal is (HpickP a1 Ha1).
We prove the intermediate claim Hex0: ∃U : set, U ∈ Tx ∧ (U ∩ A = {a0} ∧ (a0 ∈ pick a0 ∧ pick a0 ⊆ U)).
An exact proof term for the current goal is (andER (pick a0 ∈ B) (∃U : set, U ∈ Tx ∧ (U ∩ A = {a0} ∧ (a0 ∈ pick a0 ∧ pick a0 ⊆ U))) Hp0).
We prove the intermediate claim Hex1: ∃U : set, U ∈ Tx ∧ (U ∩ A = {a1} ∧ (a1 ∈ pick a1 ∧ pick a1 ⊆ U)).
An exact proof term for the current goal is (andER (pick a1 ∈ B) (∃U : set, U ∈ Tx ∧ (U ∩ A = {a1} ∧ (a1 ∈ pick a1 ∧ pick a1 ⊆ U))) Hp1).
We prove the intermediate claim Ha1inpick1: a1 ∈ pick a1.
Apply Hex1 to the current goal.
Let U1 be given.
Assume HU1pair.
We prove the intermediate claim HU1rest: U1 ∩ A = {a1} ∧ (a1 ∈ pick a1 ∧ pick a1 ⊆ U1).
An exact proof term for the current goal is (andER (U1 ∈ Tx) (U1 ∩ A = {a1} ∧ (a1 ∈ pick a1 ∧ pick a1 ⊆ U1)) HU1pair).
An exact proof term for the current goal is (andEL (a1 ∈ pick a1) (pick a1 ⊆ U1) (andER (U1 ∩ A = {a1}) (a1 ∈ pick a1 ∧ pick a1 ⊆ U1) HU1rest)).
We prove the intermediate claim Ha1inpick0: a1 ∈ pick a0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Ha1inpick1.
Apply Hex0 to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (U0 ∩ A = {a0} ∧ (a0 ∈ pick a0 ∧ pick a0 ⊆ U0)) HU0pair).
We prove the intermediate claim HU0rest: U0 ∩ A = {a0} ∧ (a0 ∈ pick a0 ∧ pick a0 ⊆ U0).
An exact proof term for the current goal is (andER (U0 ∈ Tx) (U0 ∩ A = {a0} ∧ (a0 ∈ pick a0 ∧ pick a0 ⊆ U0)) HU0pair).
We prove the intermediate claim HU0eq: U0 ∩ A = {a0}.
An exact proof term for the current goal is (andEL (U0 ∩ A = {a0}) (a0 ∈ pick a0 ∧ pick a0 ⊆ U0) HU0rest).
We prove the intermediate claim HsubU0: pick a0 ⊆ U0.
An exact proof term for the current goal is (andER (a0 ∈ pick a0) (pick a0 ⊆ U0) (andER (U0 ∩ A = {a0}) (a0 ∈ pick a0 ∧ pick a0 ⊆ U0) HU0rest)).
We prove the intermediate claim Ha1U0: a1 ∈ U0.
An exact proof term for the current goal is (HsubU0 a1 Ha1inpick0).
We prove the intermediate claim Ha1UA: a1 ∈ U0 ∩ A.
An exact proof term for the current goal is (binintersectI U0 A a1 Ha1U0 Ha1).
We prove the intermediate claim Ha1sing: a1 ∈ {a0}.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is Ha1UA.
Use symmetry.
An exact proof term for the current goal is (singleton_elem a1 a0 Ha1sing).
We will prove atleastp A ω.
Apply atleastp_tra A B ω to the current goal.
We will prove atleastp A B.
We will prove ∃f : set → set, inj A B f.
We use pick to witness the existential quantifier.
An exact proof term for the current goal is HinjAB.
An exact proof term for the current goal is HBcount.
∎