Let X and Tx be given.
Assume HexD: ∃D : set, D ⊆ X ∧ countable D ∧ dense_in D X Tx.
Let Fam be given.
Assume Hopen: ∀U : set, U ∈ Fam → open_in X Tx U.
Assume Hdisj: ∀U V : set, U ∈ Fam → V ∈ Fam → U ≠ V → U ∩ V = Empty.
Apply HexD to the current goal.
Let D be given.
Assume HD: D ⊆ X ∧ countable D ∧ dense_in D X Tx.
We prove the intermediate claim HDpair: D ⊆ X ∧ countable D.
An exact proof term for the current goal is (andEL (D ⊆ X ∧ countable D) (dense_in D X Tx) HD).
We prove the intermediate claim Hdense: dense_in D X Tx.
An exact proof term for the current goal is (andER (D ⊆ X ∧ countable D) (dense_in D X Tx) HD).
We prove the intermediate claim HDsubX: D ⊆ X.
An exact proof term for the current goal is (andEL (D ⊆ X) (countable D) HDpair).
We prove the intermediate claim HDcount: countable D.
An exact proof term for the current goal is (andER (D ⊆ X) (countable D) HDpair).
Set Fam0 to be the term {U ∈ Fam|U ≠ Empty}.
Set choose to be the term λU : set ⇒ Eps_i (λd : set ⇒ d ∈ D ∧ d ∈ U) of type set → set.
We prove the intermediate claim HAtleast: atleastp Fam0 D.
We will prove ∃f : set → set, inj Fam0 D f.
We use choose to witness the existential quantifier.
Apply (injI Fam0 D choose) to the current goal.
Let U be given.
Assume HU0: U ∈ Fam0.
We will prove choose U ∈ D.
We prove the intermediate claim HUFam: U ∈ Fam.
An exact proof term for the current goal is (SepE1 Fam (λU0 : set ⇒ U0 ≠ Empty) U HU0).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (SepE2 Fam (λU0 : set ⇒ U0 ≠ Empty) U HU0).
We prove the intermediate claim HopenU: open_in X Tx U.
An exact proof term for the current goal is (Hopen U HUFam).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (U ∈ Tx) HopenU).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (U ∈ Tx) HopenU).
We prove the intermediate claim HUmeet: U ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx U HTx Hdense HUinTx HUne).
We prove the intermediate claim Hexd: ∃d : set, d ∈ U ∩ D.
An exact proof term for the current goal is (nonempty_has_element (U ∩ D) HUmeet).
We prove the intermediate claim Hexd2: ∃d : set, d ∈ D ∧ d ∈ U.
Apply Hexd 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).
We prove the intermediate claim Hchooseprop: choose U ∈ D ∧ choose U ∈ U.
An exact proof term for the current goal is (Eps_i_ex (λd : set ⇒ d ∈ D ∧ d ∈ U) Hexd2).
An exact proof term for the current goal is (andEL (choose U ∈ D) (choose U ∈ U) Hchooseprop).
Let U be given.
Assume HU0: U ∈ Fam0.
Let V be given.
Assume HV0: V ∈ Fam0.
Assume Heq: choose U = choose V.
We will prove U = V.
Apply dneg to the current goal.
Assume HUVneq: ¬ (U = V).
We will prove False.
We prove the intermediate claim HUFam: U ∈ Fam.
An exact proof term for the current goal is (SepE1 Fam (λU0 : set ⇒ U0 ≠ Empty) U HU0).
We prove the intermediate claim HVFam: V ∈ Fam.
An exact proof term for the current goal is (SepE1 Fam (λU0 : set ⇒ U0 ≠ Empty) V HV0).
We prove the intermediate claim HdisjUV: U ∩ V = Empty.
An exact proof term for the current goal is (Hdisj U V HUFam HVFam HUVneq).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (SepE2 Fam (λU0 : set ⇒ U0 ≠ Empty) U HU0).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (SepE2 Fam (λU0 : set ⇒ U0 ≠ Empty) V HV0).
We prove the intermediate claim HopenU: open_in X Tx U.
An exact proof term for the current goal is (Hopen U HUFam).
We prove the intermediate claim HopenV: open_in X Tx V.
An exact proof term for the current goal is (Hopen V HVFam).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (U ∈ Tx) HopenU).
We prove the intermediate claim HUVin: choose U ∈ U ∧ choose V ∈ V.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (U ∈ Tx) HopenU).
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (V ∈ Tx) HopenV).
We prove the intermediate claim HUmeet: U ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx U HTx Hdense HUinTx HUne).
We prove the intermediate claim HVmeet: V ∩ D ≠ Empty.
An exact proof term for the current goal is (dense_in_meets_nonempty_open D X Tx V HTx Hdense HVinTx HVne).
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) HUmeet).
We prove the intermediate claim HexdU: ∃d : set, d ∈ D ∧ d ∈ U.
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).
We prove the intermediate claim HexVD: ∃d : set, d ∈ V ∩ D.
An exact proof term for the current goal is (nonempty_has_element (V ∩ D) HVmeet).
We prove the intermediate claim HexdV: ∃d : set, d ∈ D ∧ d ∈ V.
Apply HexVD to the current goal.
Let d be given.
Assume HdVD: d ∈ V ∩ 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 V D d HdVD).
An exact proof term for the current goal is (binintersectE1 V D d HdVD).
We prove the intermediate claim HchooseU: choose U ∈ D ∧ choose U ∈ U.
An exact proof term for the current goal is (Eps_i_ex (λd : set ⇒ d ∈ D ∧ d ∈ U) HexdU).
We prove the intermediate claim HchooseV: choose V ∈ D ∧ choose V ∈ V.
An exact proof term for the current goal is (Eps_i_ex (λd : set ⇒ d ∈ D ∧ d ∈ V) HexdV).
Apply andI to the current goal.
An exact proof term for the current goal is (andER (choose U ∈ D) (choose U ∈ U) HchooseU).
An exact proof term for the current goal is (andER (choose V ∈ D) (choose V ∈ V) HchooseV).
We prove the intermediate claim HcU: choose U ∈ U.
An exact proof term for the current goal is (andEL (choose U ∈ U) (choose V ∈ V) HUVin).
We prove the intermediate claim HcV: choose V ∈ V.
An exact proof term for the current goal is (andER (choose U ∈ U) (choose V ∈ V) HUVin).
We prove the intermediate claim HcV2: choose U ∈ V.
We prove the intermediate claim Hsubst: ∀S T : set, S = T → T ∈ V → S ∈ V.
Let S and T be given.
Assume HeqST: S = T.
Assume HT: T ∈ V.
We will prove S ∈ V.
rewrite the current goal using HeqST (from left to right) at position 1.
An exact proof term for the current goal is HT.
An exact proof term for the current goal is (Hsubst (choose U) (choose V) Heq HcV).
We prove the intermediate claim HcUV: choose U ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (choose U) HcU HcV2).
We prove the intermediate claim Hcontra: choose U ∈ Empty.
rewrite the current goal using HdisjUV (from right to left).
An exact proof term for the current goal is HcUV.
An exact proof term for the current goal is (EmptyE (choose U) Hcontra).
We prove the intermediate claim HcountFam0: countable Fam0.
An exact proof term for the current goal is (atleastp_tra Fam0 D ω HAtleast HDcount).
We prove the intermediate claim HcountSing: countable {Empty}.
An exact proof term for the current goal is (finite_countable (Sing Empty) (Sing_finite Empty)).
We prove the intermediate claim HcountUnion: countable (Fam0 ∪ {Empty}).
An exact proof term for the current goal is (binunion_countable Fam0 {Empty} HcountFam0 HcountSing).
We prove the intermediate claim HFsub: Fam ⊆ Fam0 ∪ {Empty}.
Let U be given.
Assume HU: U ∈ Fam.
We will prove U ∈ Fam0 ∪ {Empty}.
Apply (xm (U = Empty)) to the current goal.
Assume HUe: U = Empty.
Apply binunionI2 to the current goal.
rewrite the current goal using HUe (from left to right).
An exact proof term for the current goal is (SingI Empty).
Assume HUne: ¬ (U = Empty).
Apply binunionI1 to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is HU.
Assume HE: U = Empty.
An exact proof term for the current goal is (HUne HE).
An exact proof term for the current goal is (Subq_countable Fam (Fam0 ∪ {Empty}) HcountUnion HFsub).
∎