We will prove generated_topology EuclidPlane rectangular_regions = R2_standard_topology.
We prove the intermediate claim HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HtopPlane: topology_on EuclidPlane R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology HtopR HtopR).
We prove the intermediate claim HCsub: ∀Cx ∈ rectangular_regions, Cx ∈ R2_standard_topology.
Let Cx be given.
Assume HCx: Cx ∈ rectangular_regions.
An exact proof term for the current goal is (rectangular_regions_subset_R2_standard_topology Cx HCx).
We prove the intermediate claim Href: ∀U ∈ R2_standard_topology, ∀p ∈ U, ∃Cx ∈ rectangular_regions, p ∈ Cx ∧ Cx ⊆ U.
Let U be given.
Assume HU: U ∈ R2_standard_topology.
Let p be given.
Assume HpU: p ∈ U.
We prove the intermediate claim HeqPlane: EuclidPlane = setprod R R.
Use reflexivity.
Set B to be the term product_subbasis R R_standard_topology R R_standard_topology.
We prove the intermediate claim HUgenRR: U ∈ generated_topology (setprod R R) B.
We prove the intermediate claim Hdef: R2_standard_topology = generated_topology (setprod R R) B.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HeqPlane (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim HUgen: U ∈ generated_topology EuclidPlane B.
rewrite the current goal using HeqPlane (from left to right).
An exact proof term for the current goal is HUgenRR.
We prove the intermediate claim HUsub: U ⊆ EuclidPlane.
An exact proof term for the current goal is (generated_topology_subset EuclidPlane B U HUgen).
We prove the intermediate claim HpE: p ∈ EuclidPlane.
An exact proof term for the current goal is (HUsub p HpU).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 EuclidPlane) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb: ∃b ∈ B, p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop p HpU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair: b ∈ B ∧ (p ∈ b ∧ b ⊆ U).
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (p ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbprop: p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ B) (p ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hpb: p ∈ b.
An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ U) Hbprop).
Apply (famunionE_impred R_standard_topology (λU0 : set ⇒ {rectangle_set U0 V|V ∈ R_standard_topology}) b HbB (∃Cx ∈ rectangular_regions, p ∈ Cx ∧ Cx ⊆ U)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ R_standard_topology.
Assume HbIn: b ∈ {rectangle_set U0 V|V ∈ R_standard_topology}.
Apply (ReplE_impred R_standard_topology (λV0 : set ⇒ rectangle_set U0 V0) b HbIn (∃Cx ∈ rectangular_regions, p ∈ Cx ∧ Cx ⊆ U)) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ R_standard_topology.
Assume Hbeq: b = rectangle_set U0 V0.
We prove the intermediate claim HpbUV: p ∈ rectangle_set U0 V0.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hpb.
We prove the intermediate claim HpUV: p ∈ setprod U0 V0.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is HpbUV.
We prove the intermediate claim Hp0U0: p 0 ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim Hp1V0: p 1 ∈ V0.
An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) p HpUV).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta U0 V0 p HpUV).
We prove the intermediate claim HU0gen: U0 ∈ generated_topology R R_standard_basis.
rewrite the current goal using R_standard_topology_def_eq (from right to left).
An exact proof term for the current goal is HU0.
We prove the intermediate claim HU0prop: ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU1 : set ⇒ ∀x0 ∈ U1, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U1) U0 HU0gen).
We prove the intermediate claim HexI1: ∃I1 ∈ R_standard_basis, (p 0) ∈ I1 ∧ I1 ⊆ U0.
An exact proof term for the current goal is (HU0prop (p 0) Hp0U0).
Apply HexI1 to the current goal.
Let I1 be given.
Assume HI1pair: I1 ∈ R_standard_basis ∧ ((p 0) ∈ I1 ∧ I1 ⊆ U0).
We prove the intermediate claim HI1: I1 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (I1 ∈ R_standard_basis) ((p 0) ∈ I1 ∧ I1 ⊆ U0) HI1pair).
We prove the intermediate claim HI1prop: (p 0) ∈ I1 ∧ I1 ⊆ U0.
An exact proof term for the current goal is (andER (I1 ∈ R_standard_basis) ((p 0) ∈ I1 ∧ I1 ⊆ U0) HI1pair).
We prove the intermediate claim Hp0I1: (p 0) ∈ I1.
An exact proof term for the current goal is (andEL ((p 0) ∈ I1) (I1 ⊆ U0) HI1prop).
We prove the intermediate claim HI1sub: I1 ⊆ U0.
An exact proof term for the current goal is (andER ((p 0) ∈ I1) (I1 ⊆ U0) HI1prop).
We prove the intermediate claim Hexa: ∃a ∈ R, I1 ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) I1 HI1).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair: a ∈ R ∧ I1 ∈ {open_interval a b|b ∈ R}.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (I1 ∈ {open_interval a b|b ∈ R}) Hapair).
We prove the intermediate claim HI1fam: I1 ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (I1 ∈ {open_interval a b|b ∈ R}) Hapair).
We prove the intermediate claim Hexb1: ∃b1 ∈ R, I1 = open_interval a b1.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0) I1 HI1fam).
Apply Hexb1 to the current goal.
Let b1 be given.
Assume Hb1pair: b1 ∈ R ∧ I1 = open_interval a b1.
We prove the intermediate claim Hb1R: b1 ∈ R.
An exact proof term for the current goal is (andEL (b1 ∈ R) (I1 = open_interval a b1) Hb1pair).
We prove the intermediate claim HI1eq: I1 = open_interval a b1.
An exact proof term for the current goal is (andER (b1 ∈ R) (I1 = open_interval a b1) Hb1pair).
We prove the intermediate claim Hp0InInt: (p 0) ∈ open_interval a b1.
rewrite the current goal using HI1eq (from right to left).
An exact proof term for the current goal is Hp0I1.
We prove the intermediate claim Hp0ineq: Rlt a (p 0) ∧ Rlt (p 0) b1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a z ∧ Rlt z b1) (p 0) Hp0InInt).
We prove the intermediate claim Hap0: Rlt a (p 0).
An exact proof term for the current goal is (andEL (Rlt a (p 0)) (Rlt (p 0) b1) Hp0ineq).
We prove the intermediate claim Hp0b1: Rlt (p 0) b1.
An exact proof term for the current goal is (andER (Rlt a (p 0)) (Rlt (p 0) b1) Hp0ineq).
We prove the intermediate claim Hab: Rlt a b1.
An exact proof term for the current goal is (Rlt_tra a (p 0) b1 Hap0 Hp0b1).
We prove the intermediate claim HV0gen: V0 ∈ generated_topology R R_standard_basis.
rewrite the current goal using R_standard_topology_def_eq (from right to left).
An exact proof term for the current goal is HV0.
We prove the intermediate claim HV0prop: ∀y0 ∈ V0, ∃J1 ∈ R_standard_basis, y0 ∈ J1 ∧ J1 ⊆ V0.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU1 : set ⇒ ∀x0 ∈ U1, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U1) V0 HV0gen).
We prove the intermediate claim HexI2: ∃I2 ∈ R_standard_basis, (p 1) ∈ I2 ∧ I2 ⊆ V0.
An exact proof term for the current goal is (HV0prop (p 1) Hp1V0).
Apply HexI2 to the current goal.
Let I2 be given.
Assume HI2pair: I2 ∈ R_standard_basis ∧ ((p 1) ∈ I2 ∧ I2 ⊆ V0).
We prove the intermediate claim HI2: I2 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (I2 ∈ R_standard_basis) ((p 1) ∈ I2 ∧ I2 ⊆ V0) HI2pair).
We prove the intermediate claim HI2prop: (p 1) ∈ I2 ∧ I2 ⊆ V0.
An exact proof term for the current goal is (andER (I2 ∈ R_standard_basis) ((p 1) ∈ I2 ∧ I2 ⊆ V0) HI2pair).
We prove the intermediate claim Hp1I2: (p 1) ∈ I2.
An exact proof term for the current goal is (andEL ((p 1) ∈ I2) (I2 ⊆ V0) HI2prop).
We prove the intermediate claim HI2sub: I2 ⊆ V0.
An exact proof term for the current goal is (andER ((p 1) ∈ I2) (I2 ⊆ V0) HI2prop).
We prove the intermediate claim Hexc: ∃c ∈ R, I2 ∈ {open_interval c d|d ∈ R}.
An exact proof term for the current goal is (famunionE R (λc0 : set ⇒ {open_interval c0 d|d ∈ R}) I2 HI2).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair: c ∈ R ∧ I2 ∈ {open_interval c d|d ∈ R}.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (I2 ∈ {open_interval c d|d ∈ R}) Hcpair).
We prove the intermediate claim HI2fam: I2 ∈ {open_interval c d|d ∈ R}.
An exact proof term for the current goal is (andER (c ∈ R) (I2 ∈ {open_interval c d|d ∈ R}) Hcpair).
We prove the intermediate claim Hexd1: ∃d1 ∈ R, I2 = open_interval c d1.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ open_interval c d0) I2 HI2fam).
Apply Hexd1 to the current goal.
Let d1 be given.
Assume Hd1pair: d1 ∈ R ∧ I2 = open_interval c d1.
We prove the intermediate claim Hd1R: d1 ∈ R.
An exact proof term for the current goal is (andEL (d1 ∈ R) (I2 = open_interval c d1) Hd1pair).
We prove the intermediate claim HI2eq: I2 = open_interval c d1.
An exact proof term for the current goal is (andER (d1 ∈ R) (I2 = open_interval c d1) Hd1pair).
We prove the intermediate claim Hp1InInt: (p 1) ∈ open_interval c d1.
rewrite the current goal using HI2eq (from right to left).
An exact proof term for the current goal is Hp1I2.
We prove the intermediate claim Hp1ineq: Rlt c (p 1) ∧ Rlt (p 1) d1.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt c z ∧ Rlt z d1) (p 1) Hp1InInt).
We prove the intermediate claim Hcp1: Rlt c (p 1).
An exact proof term for the current goal is (andEL (Rlt c (p 1)) (Rlt (p 1) d1) Hp1ineq).
We prove the intermediate claim Hp1d1: Rlt (p 1) d1.
An exact proof term for the current goal is (andER (Rlt c (p 1)) (Rlt (p 1) d1) Hp1ineq).
We prove the intermediate claim Hcd: Rlt c d1.
An exact proof term for the current goal is (Rlt_tra c (p 1) d1 Hcp1 Hp1d1).
Set Rg to be the term {q ∈ EuclidPlane|∃x y : set, q = (x,y) ∧ Rlt a x ∧ Rlt x b1 ∧ Rlt c y ∧ Rlt y d1}.
We prove the intermediate claim HRgRect: Rg ∈ rectangular_regions.
An exact proof term for the current goal is (rectangular_regionI a b1 c d1 HaR Hb1R HcR Hd1R Hab Hcd).
We prove the intermediate claim HpRg: p ∈ Rg.
rewrite the current goal using HpEta (from left to right).
We prove the intermediate claim Hp0R: (p 0) ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt a z ∧ Rlt z b1) (p 0) Hp0InInt).
We prove the intermediate claim Hp1R: (p 1) ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt c z ∧ Rlt z d1) (p 1) Hp1InInt).
We prove the intermediate claim HpE2: (p 0,p 1) ∈ EuclidPlane.
We prove the intermediate claim HeqPlane2: EuclidPlane = setprod R R.
Use reflexivity.
rewrite the current goal using HeqPlane2 (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R (p 0) (p 1) Hp0R Hp1R).
We prove the intermediate claim Hpred: ∃x y : set, (p 0,p 1) = (x,y) ∧ Rlt a x ∧ Rlt x b1 ∧ Rlt c y ∧ Rlt y d1.
We use (p 0) to witness the existential quantifier.
We use (p 1) to witness the existential quantifier.
Apply and5I to the current goal.
Use reflexivity.
An exact proof term for the current goal is Hap0.
An exact proof term for the current goal is Hp0b1.
An exact proof term for the current goal is Hcp1.
An exact proof term for the current goal is Hp1d1.
An exact proof term for the current goal is (SepI EuclidPlane (λq0 : set ⇒ ∃x y : set, q0 = (x,y) ∧ Rlt a x ∧ Rlt x b1 ∧ Rlt c y ∧ Rlt y d1) (p 0,p 1) HpE2 Hpred).
We prove the intermediate claim HRgSubb: Rg ⊆ b.
We prove the intermediate claim HI1subU0: open_interval a b1 ⊆ U0.
rewrite the current goal using HI1eq (from right to left).
An exact proof term for the current goal is HI1sub.
We prove the intermediate claim HI2subV0: open_interval c d1 ⊆ V0.
rewrite the current goal using HI2eq (from right to left).
An exact proof term for the current goal is HI2sub.
We prove the intermediate claim HsetprodSub: setprod (open_interval a b1) (open_interval c d1) ⊆ setprod U0 V0.
An exact proof term for the current goal is (setprod_Subq (open_interval a b1) (open_interval c d1) U0 V0 HI1subU0 HI2subV0).
We prove the intermediate claim HrectSub: rectangle_set (open_interval a b1) (open_interval c d1) ⊆ rectangle_set U0 V0.
rewrite the current goal using rectangle_set_def (from left to right).
rewrite the current goal using rectangle_set_def (from left to right).
An exact proof term for the current goal is HsetprodSub.
Let q be given.
Assume HqRg: q ∈ Rg.
We will prove q ∈ b.
We prove the intermediate claim HqRect: q ∈ rectangle_set (open_interval a b1) (open_interval c d1).
rewrite the current goal using (open_rectangle_set_eq_rectangle_set_intervals a b1 c d1) (from right to left).
An exact proof term for the current goal is HqRg.
We prove the intermediate claim HqInUV: q ∈ rectangle_set U0 V0.
An exact proof term for the current goal is (HrectSub q HqRect).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HqInUV.
We prove the intermediate claim HRgSubU: Rg ⊆ U.
An exact proof term for the current goal is (Subq_tra Rg b U HRgSubb HbsubU).
We use Rg to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HRgRect.
Apply andI to the current goal.
An exact proof term for the current goal is HpRg.
An exact proof term for the current goal is HRgSubU.
We prove the intermediate claim HBgener: basis_on EuclidPlane rectangular_regions ∧ generated_topology EuclidPlane rectangular_regions = R2_standard_topology.
An exact proof term for the current goal is (basis_refines_topology EuclidPlane R2_standard_topology rectangular_regions HtopPlane HCsub Href).
An exact proof term for the current goal is (andER (basis_on EuclidPlane rectangular_regions) (generated_topology EuclidPlane rectangular_regions = R2_standard_topology) HBgener).
∎