We will prove countable_set rational_open_intervals_basis.
Set QQ to be the term setprod rational_numbers rational_numbers.
Set F to be the term λp : set ⇒ open_interval (p 0) (p 1) of type set → set.
We prove the intermediate claim HQ: countable_set rational_numbers.
An exact proof term for the current goal is rational_numbers_countable.
We prove the intermediate claim HQQ: countable_set QQ.
An exact proof term for the current goal is (setprod_countable rational_numbers rational_numbers HQ HQ).
We prove the intermediate claim Himg: countable_set {F p|p ∈ QQ}.
An exact proof term for the current goal is (countable_image QQ HQQ F).
We prove the intermediate claim Hsub: rational_open_intervals_basis ⊆ {F p|p ∈ QQ}.
Let I be given.
Assume HI: I ∈ rational_open_intervals_basis.
We will prove I ∈ {F p|p ∈ QQ}.
We prove the intermediate claim Hexq1: ∃q1 ∈ rational_numbers, I ∈ {open_interval q1 q2|q2 ∈ rational_numbers}.
An exact proof term for the current goal is (famunionE rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) I HI).
Apply Hexq1 to the current goal.
Let q1 be given.
Assume Hq1pair.
We prove the intermediate claim Hq1Q: q1 ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q1 ∈ rational_numbers) (I ∈ {open_interval q1 q2|q2 ∈ rational_numbers}) Hq1pair).
We prove the intermediate claim HIRepl: I ∈ {open_interval q1 q2|q2 ∈ rational_numbers}.
An exact proof term for the current goal is (andER (q1 ∈ rational_numbers) (I ∈ {open_interval q1 q2|q2 ∈ rational_numbers}) Hq1pair).
We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, I = open_interval q1 q2.
An exact proof term for the current goal is (ReplE rational_numbers (λq2 : set ⇒ open_interval q1 q2) I HIRepl).
Apply Hexq2 to the current goal.
Let q2 be given.
Assume Hq2pair.
We prove the intermediate claim Hq2Q: q2 ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q2 ∈ rational_numbers) (I = open_interval q1 q2) Hq2pair).
We prove the intermediate claim HIeq: I = open_interval q1 q2.
An exact proof term for the current goal is (andER (q2 ∈ rational_numbers) (I = open_interval q1 q2) Hq2pair).
We prove the intermediate claim HpQQ: (q1,q2) ∈ QQ.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma rational_numbers rational_numbers q1 q2 Hq1Q Hq2Q).
We prove the intermediate claim HFpair: F (q1,q2) = open_interval q1 q2.
We prove the intermediate claim HFdef: F (q1,q2) = open_interval ((q1,q2) 0) ((q1,q2) 1).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (tuple_2_0_eq q1 q2) (from left to right).
rewrite the current goal using (tuple_2_1_eq q1 q2) (from left to right).
Use reflexivity.
rewrite the current goal using HIeq (from left to right).
rewrite the current goal using HFpair (from right to left).
An exact proof term for the current goal is (ReplI QQ F (q1,q2) HpQQ).
An exact proof term for the current goal is (Subq_countable rational_open_intervals_basis {F p|p ∈ QQ} Himg Hsub).
∎