Let U and V be given.
Assume HU: U ∈ discrete_topology R.
Assume HV: V ∈ R_standard_topology.
Set X0 to be the term setprod R R.
Set T to be the term R2_dictionary_order_topology.
We prove the intermediate claim HT: topology_on X0 T.
An exact proof term for the current goal is dictionary_order_topology_is_topology.
We prove the intermediate claim HUPow: U ∈ 𝒫 R.
We prove the intermediate claim HdefDisc: discrete_topology R = 𝒫 R.
Use reflexivity.
rewrite the current goal using HdefDisc (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUsub: U ⊆ R.
An exact proof term for the current goal is (PowerE R U HUPow).
Set Fam to be the term {rectangle_set {a} V|a ∈ U}.
We prove the intermediate claim HFamSub: Fam ⊆ T.
Let W be given.
Assume HW: W ∈ Fam.
Apply (ReplE_impred U (λa : set ⇒ rectangle_set {a} V) W HW (W ∈ T)) to the current goal.
Let a be given.
Assume HaU Heq.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (HUsub a HaU).
An exact proof term for the current goal is (singleton_rectangle_in_dictionary a V HaR HV).
We prove the intermediate claim HUnionInT: ⋃ Fam ∈ T.
An exact proof term for the current goal is (topology_union_closed X0 T Fam HT HFamSub).
We prove the intermediate claim HUnionEq: ⋃ Fam = rectangle_set U V.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ ⋃ Fam.
Apply (UnionE_impred Fam p Hp (p ∈ rectangle_set U V)) to the current goal.
Let W be given.
Assume HpW HW.
Apply (ReplE_impred U (λa : set ⇒ rectangle_set {a} V) W HW (p ∈ rectangle_set U V)) to the current goal.
Let a be given.
Assume HaU Heq.
We prove the intermediate claim HpWrect: p ∈ rectangle_set {a} V.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HpW.
We prove the intermediate claim HpWsetprod: p ∈ setprod {a} V.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HpWrect.
We prove the intermediate claim Hp0: p 0 ∈ {a}.
An exact proof term for the current goal is (ap0_Sigma {a} (λ_ : set ⇒ V) p HpWsetprod).
We prove the intermediate claim Hpa: p 0 = a.
An exact proof term for the current goal is (SingE a (p 0) Hp0).
We will prove p ∈ rectangle_set U V.
rewrite the current goal using rectangle_set_def (from left to right).
We prove the intermediate claim Hp1: p 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma {a} (λ_ : set ⇒ V) p HpWsetprod).
We prove the intermediate claim Hp0U: p 0 ∈ U.
rewrite the current goal using Hpa (from left to right).
An exact proof term for the current goal is HaU.
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta {a} V p HpWsetprod).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U V (p 0) (p 1) Hp0U Hp1).
Let p be given.
Assume Hp: p ∈ rectangle_set U V.
We will prove p ∈ ⋃ Fam.
We prove the intermediate claim HpUV: p ∈ setprod U V.
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is Hp.
Set a to be the term p 0.
We prove the intermediate claim Hp0U: p 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ V) p HpUV).
We prove the intermediate claim Hp1V: p 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ V) p HpUV).
We prove the intermediate claim HpEta0: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta U V p HpUV).
Set W to be the term rectangle_set {a} V.
We prove the intermediate claim HWFam: W ∈ Fam.
An exact proof term for the current goal is (ReplI U (λx : set ⇒ rectangle_set {x} V) a Hp0U).
We prove the intermediate claim HpW: p ∈ W.
rewrite the current goal using rectangle_set_def (from left to right).
rewrite the current goal using HpEta0 (from left to right) at position 1.
We prove the intermediate claim Hp0Sing: p 0 ∈ {a}.
We prove the intermediate claim Hadef: a = p 0.
Use reflexivity.
rewrite the current goal using Hadef (from left to right).
An exact proof term for the current goal is (SingI (p 0)).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {a} V (p 0) (p 1) Hp0Sing Hp1V).
An exact proof term for the current goal is (UnionI Fam p W HpW HWFam).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionInT.
∎