Let X, Tx, D and Fam be given.
Assume HTx: topology_on X Tx.
Assume Hdense: dense_in D X Tx.
Assume HcountD: countable_set D.
Assume HFamSub: Fam ⊆ Tx.
Assume Hne: ∀U : set, U ∈ Fam → U ≠ Empty.
Assume Hdisj: pairwise_disjoint Fam.
We will prove countable_set Fam.
We prove the intermediate claim dense_meets_nonempty_open: ∀U : set, U ∈ Tx → U ≠ Empty → ∃d : set, d ∈ D ∧ d ∈ U.
Let U be given.
Assume HUopen: U ∈ Tx.
Assume HUne: U ≠ Empty.
We prove the intermediate claim Hexx: ∃x : set, x ∈ U.
An exact proof term for the current goal is (nonempty_has_element U HUne).
Set x0 to be the term Eps_i (λx : set ⇒ x ∈ U).
We prove the intermediate claim Hx0U: x0 ∈ U.
An exact proof term for the current goal is (Eps_i_ex (λx : set ⇒ x ∈ U) Hexx).
We prove the intermediate claim HUSubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUopen).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (HUSubX x0 Hx0U).
We prove the intermediate claim HclEq: closure_of X Tx D = X.
An exact proof term for the current goal is Hdense.
We prove the intermediate claim Hx0cl: x0 ∈ closure_of X Tx D.
rewrite the current goal using HclEq (from left to right).
An exact proof term for the current goal is Hx0X.
We prove the intermediate claim Hcliff: x0 ∈ closure_of X Tx D ↔ (∀W ∈ Tx, x0 ∈ W → W ∩ D ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx D x0 HTx Hx0X).
We prove the intermediate claim Hneigh: ∀W ∈ Tx, x0 ∈ W → W ∩ D ≠ Empty.
An exact proof term for the current goal is (iffEL (x0 ∈ closure_of X Tx D) (∀W ∈ Tx, x0 ∈ W → W ∩ D ≠ Empty) Hcliff Hx0cl).
We prove the intermediate claim HUDne: U ∩ D ≠ Empty.
An exact proof term for the current goal is (Hneigh U HUopen Hx0U).
We prove the intermediate claim HexUD: ∃d : set, d ∈ U ∩ D.
An exact proof term for the current goal is (nonempty_has_element (U ∩ D) HUDne).
Apply HexUD to the current goal.
Let d be given.
Assume HdUD: d ∈ U ∩ D.
We use d to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binintersectE2 U D d HdUD).
An exact proof term for the current goal is (binintersectE1 U D d HdUD).
Set pick to be the term (λU : set ⇒ Eps_i (λd : set ⇒ d ∈ D ∧ d ∈ U)).
We prove the intermediate claim Hpick_in_D: ∀U : set, U ∈ Fam → pick U ∈ D.
Let U be given.
Assume HUfam: U ∈ Fam.
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (HFamSub U HUfam).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (Hne U HUfam).
We prove the intermediate claim Hexd: ∃d : set, d ∈ D ∧ d ∈ U.
An exact proof term for the current goal is (dense_meets_nonempty_open U HUopen HUne).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair: d ∈ D ∧ d ∈ U.
We prove the intermediate claim HpickProp: pick U ∈ D ∧ pick U ∈ U.
An exact proof term for the current goal is (Eps_i_ax (λd0 : set ⇒ d0 ∈ D ∧ d0 ∈ U) d Hdpair).
An exact proof term for the current goal is (andEL (pick U ∈ D) (pick U ∈ U) HpickProp).
We prove the intermediate claim Hpick_in_U: ∀U : set, U ∈ Fam → pick U ∈ U.
Let U be given.
Assume HUfam: U ∈ Fam.
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (HFamSub U HUfam).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (Hne U HUfam).
We prove the intermediate claim Hexd: ∃d : set, d ∈ D ∧ d ∈ U.
An exact proof term for the current goal is (dense_meets_nonempty_open U HUopen HUne).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair: d ∈ D ∧ d ∈ U.
We prove the intermediate claim HpickProp: pick U ∈ D ∧ pick U ∈ U.
An exact proof term for the current goal is (Eps_i_ax (λd0 : set ⇒ d0 ∈ D ∧ d0 ∈ U) d Hdpair).
An exact proof term for the current goal is (andER (pick U ∈ D) (pick U ∈ U) HpickProp).
We prove the intermediate claim HinjFamD: atleastp Fam D.
We will prove ∃f : set → set, inj Fam D f.
We use pick to witness the existential quantifier.
Apply (injI Fam D pick) to the current goal.
Let U be given.
Assume HUfam: U ∈ Fam.
An exact proof term for the current goal is (Hpick_in_D U HUfam).
Let U1 be given.
Assume HU1: U1 ∈ Fam.
Let U2 be given.
Assume HU2: U2 ∈ Fam.
Assume Heq: pick U1 = pick U2.
We will prove U1 = U2.
Apply (dneg (U1 = U2)) to the current goal.
Assume Hneq: ¬ (U1 = U2).
We will prove False.
We prove the intermediate claim Hinter: U1 ∩ U2 = Empty.
An exact proof term for the current goal is (Hdisj U1 U2 HU1 HU2 Hneq).
We prove the intermediate claim HpickU1: pick U1 ∈ U1.
An exact proof term for the current goal is (Hpick_in_U U1 HU1).
We prove the intermediate claim HpickU2: pick U1 ∈ U2.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Hpick_in_U U2 HU2).
We prove the intermediate claim Hpt: pick U1 ∈ U1 ∩ U2.
An exact proof term for the current goal is (binintersectI U1 U2 (pick U1) HpickU1 HpickU2).
We prove the intermediate claim Hbad: pick U1 ∈ Empty.
rewrite the current goal using Hinter (from right to left).
An exact proof term for the current goal is Hpt.
An exact proof term for the current goal is (EmptyE (pick U1) Hbad False).
An exact proof term for the current goal is (atleastp_tra Fam D ω HinjFamD HcountD).
∎