Let X, Tx, Y and Ty be given.
Assume H: Hausdorff_space X Tx ∧ Hausdorff_space Y Ty.
We will prove Hausdorff_space (setprod X Y) (product_topology X Tx Y Ty).
We prove the intermediate claim HX: Hausdorff_space X Tx.
An exact proof term for the current goal is (andEL (Hausdorff_space X Tx) (Hausdorff_space Y Ty) H).
We prove the intermediate claim HY: Hausdorff_space Y Ty.
An exact proof term for the current goal is (andER (Hausdorff_space X Tx) (Hausdorff_space Y Ty) H).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (Hausdorff_space_topology X Tx HX).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (Hausdorff_space_topology Y Ty HY).
We prove the intermediate claim HSepX: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Let x1 and x2 be given.
Assume Hx1: x1 ∈ X.
Assume Hx2: x2 ∈ X.
Assume Hneq12: x1 ≠ x2.
An exact proof term for the current goal is (Hausdorff_space_separation X Tx x1 x2 HX Hx1 Hx2 Hneq12).
We prove the intermediate claim HSepY: ∀y1 y2 : set, y1 ∈ Y → y2 ∈ Y → y1 ≠ y2 → ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ y1 ∈ U ∧ y2 ∈ V ∧ U ∩ V = Empty.
Let y1 and y2 be given.
Assume Hy1: y1 ∈ Y.
Assume Hy2: y2 ∈ Y.
Assume Hneq12: y1 ≠ y2.
An exact proof term for the current goal is (Hausdorff_space_separation Y Ty y1 y2 HY Hy1 Hy2 Hneq12).
We prove the intermediate claim HTProd: topology_on (setprod X Y) (product_topology X Tx Y Ty).
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We will prove topology_on (setprod X Y) (product_topology X Tx Y Ty) ∧ (∀p1 p2 : set, p1 ∈ setprod X Y → p2 ∈ setprod X Y → p1 ≠ p2 → ∃U V : set, U ∈ product_topology X Tx Y Ty ∧ V ∈ product_topology X Tx Y Ty ∧ p1 ∈ U ∧ p2 ∈ V ∧ U ∩ V = Empty).
Apply andI to the current goal.
An exact proof term for the current goal is HTProd.
Let p1 and p2 be given.
Assume Hp1: p1 ∈ setprod X Y.
Assume Hp2: p2 ∈ setprod X Y.
Assume Hne: p1 ≠ p2.
We will prove ∃U V : set, U ∈ product_topology X Tx Y Ty ∧ V ∈ product_topology X Tx Y Ty ∧ p1 ∈ U ∧ p2 ∈ V ∧ U ∩ V = Empty.
Apply (Sigma_E X (λ_ : set ⇒ Y) p1 Hp1) to the current goal.
Let x1 be given.
Assume Hx1_pair.
Apply Hx1_pair to the current goal.
Assume Hx1X Hexy1.
Apply Hexy1 to the current goal.
Let y1 be given.
Assume Hy1_pair.
Apply Hy1_pair to the current goal.
Assume Hy1Y Hp1eq.
Apply (Sigma_E X (λ_ : set ⇒ Y) p2 Hp2) to the current goal.
Let x2 be given.
Assume Hx2_pair.
Apply Hx2_pair to the current goal.
Assume Hx2X Hexy2.
Apply Hexy2 to the current goal.
Let y2 be given.
Assume Hy2_pair.
Apply Hy2_pair to the current goal.
Assume Hy2Y Hp2eq.
Apply (xm (x1 = x2)) to the current goal.
Assume Hx12: x1 = x2.
We prove the intermediate claim Hy12: y1 ≠ y2.
Assume HyEq: y1 = y2.
We prove the intermediate claim HpEq: p1 = p2.
rewrite the current goal using Hp1eq (from left to right).
rewrite the current goal using Hp2eq (from left to right).
rewrite the current goal using Hx12 (from left to right).
rewrite the current goal using HyEq (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hne HpEq).
Apply (HSepY y1 y2 Hy1Y Hy2Y Hy12) to the current goal.
Let U be given.
Assume HexV.
Apply HexV to the current goal.
Let V be given.
Assume HUV_conj.
Apply HUV_conj to the current goal.
Assume Hcore HUVempty.
Apply Hcore to the current goal.
Assume Hcore2 Hy2V.
Apply Hcore2 to the current goal.
Assume Hcore3 Hy1U.
Apply Hcore3 to the current goal.
Assume HU HV.
Set R1 to be the term rectangle_set X U.
Set R2 to be the term rectangle_set X V.
We use R1 to witness the existential quantifier.
We use R2 to witness the existential quantifier.
We will prove R1 ∈ product_topology X Tx Y Ty ∧ R2 ∈ product_topology X Tx Y Ty ∧ p1 ∈ R1 ∧ p2 ∈ R2 ∧ R1 ∩ R2 = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HR1sub: R1 ∈ product_subbasis X Tx Y Ty.
We will prove R1 ∈ product_subbasis X Tx Y Ty.
We prove the intermediate claim HR1fam: rectangle_set X U ∈ {rectangle_set X V0|V0 ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set X V0) U HU).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) X (rectangle_set X U) HXTx HR1fam).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis R1 HR1sub).
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HR2sub: R2 ∈ product_subbasis X Tx Y Ty.
We will prove R2 ∈ product_subbasis X Tx Y Ty.
We prove the intermediate claim HR2fam: rectangle_set X V ∈ {rectangle_set X V0|V0 ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set X V0) V HV).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) X (rectangle_set X V) HXTx HR2fam).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis R2 HR2sub).
rewrite the current goal using Hp1eq (from left to right).
An exact proof term for the current goal is (pair_Sigma X (λ_ : set ⇒ U) x1 Hx1X y1 Hy1U).
rewrite the current goal using Hp2eq (from left to right).
rewrite the current goal using Hx12 (from right to left) at position 1.
An exact proof term for the current goal is (pair_Sigma X (λ_ : set ⇒ V) x1 Hx1X y2 Hy2V).
We will prove R1 ∩ R2 = Empty.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ R1 ∩ R2.
We will prove p ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HpR1: p ∈ R1.
An exact proof term for the current goal is (binintersectE1 R1 R2 p Hp).
We prove the intermediate claim HpR2: p ∈ R2.
An exact proof term for the current goal is (binintersectE2 R1 R2 p Hp).
We prove the intermediate claim Hcoords1: ∃x ∈ X, ∃y ∈ U, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (setprod_elem_decompose X U p HpR1).
Apply Hcoords1 to the current goal.
Let x be given.
Assume Hx_pair.
We prove the intermediate claim HxX': x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (∃y0 ∈ U, p ∈ setprod {x} {y0}) Hx_pair).
We prove the intermediate claim Hexy: ∃y0 ∈ U, p ∈ setprod {x} {y0}.
An exact proof term for the current goal is (andER (x ∈ X) (∃y0 ∈ U, p ∈ setprod {x} {y0}) Hx_pair).
Apply Hexy to the current goal.
Let y be given.
Assume Hy_pair.
We prove the intermediate claim HyU': y ∈ U.
An exact proof term for the current goal is (andEL (y ∈ U) (p ∈ setprod {x} {y}) Hy_pair).
We prove the intermediate claim Hpsing1: p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (y ∈ U) (p ∈ setprod {x} {y}) Hy_pair).
We prove the intermediate claim Hcoords2: ∃x0 ∈ X, ∃y0 ∈ V, p ∈ setprod {x0} {y0}.
An exact proof term for the current goal is (setprod_elem_decompose X V p HpR2).
Apply Hcoords2 to the current goal.
Let x0 be given.
Assume Hx0_pair.
We prove the intermediate claim Hexy0: ∃y0 ∈ V, p ∈ setprod {x0} {y0}.
An exact proof term for the current goal is (andER (x0 ∈ X) (∃y0 ∈ V, p ∈ setprod {x0} {y0}) Hx0_pair).
Apply Hexy0 to the current goal.
Let y0 be given.
Assume Hy0_pair.
We prove the intermediate claim Hpsing2: p ∈ setprod {x0} {y0}.
An exact proof term for the current goal is (andER (y0 ∈ V) (p ∈ setprod {x0} {y0}) Hy0_pair).
We prove the intermediate claim HyV': y ∈ V.
An exact proof term for the current goal is (andER (x ∈ X) (y ∈ V) (setprod_coords_in x y X V p Hpsing1 HpR2)).
We prove the intermediate claim HyUV: y ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V y HyU' HyV').
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using HUVempty (from right to left).
An exact proof term for the current goal is HyUV.
An exact proof term for the current goal is (EmptyE y HyE False).
An exact proof term for the current goal is (Subq_Empty (R1 ∩ R2)).
Assume Hx12n: x1 ≠ x2.
Apply (HSepX x1 x2 Hx1X Hx2X Hx12n) to the current goal.
Let U be given.
Assume HexV.
Apply HexV to the current goal.
Let V be given.
Assume HUV_conj.
Apply HUV_conj to the current goal.
Assume Hcore HUVempty.
Apply Hcore to the current goal.
Assume Hcore2 Hx2V.
Apply Hcore2 to the current goal.
Assume Hcore3 Hx1U.
Apply Hcore3 to the current goal.
Assume HU HV.
Set R1 to be the term rectangle_set U Y.
Set R2 to be the term rectangle_set V Y.
We use R1 to witness the existential quantifier.
We use R2 to witness the existential quantifier.
We will prove R1 ∈ product_topology X Tx Y Ty ∧ R2 ∈ product_topology X Tx Y Ty ∧ p1 ∈ R1 ∧ p2 ∈ R2 ∧ R1 ∩ R2 = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HYTy: Y ∈ Ty.
An exact proof term for the current goal is (topology_has_X Y Ty HTy).
We prove the intermediate claim HR1sub: R1 ∈ product_subbasis X Tx Y Ty.
We will prove R1 ∈ product_subbasis X Tx Y Ty.
We prove the intermediate claim HR1fam: rectangle_set U Y ∈ {rectangle_set U V0|V0 ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set U V0) Y HYTy).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) U (rectangle_set U Y) HU HR1fam).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis R1 HR1sub).
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HYTy: Y ∈ Ty.
An exact proof term for the current goal is (topology_has_X Y Ty HTy).
We prove the intermediate claim HR2sub: R2 ∈ product_subbasis X Tx Y Ty.
We will prove R2 ∈ product_subbasis X Tx Y Ty.
We prove the intermediate claim HR2fam: rectangle_set V Y ∈ {rectangle_set V V0|V0 ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set V V0) Y HYTy).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) V (rectangle_set V Y) HV HR2fam).
An exact proof term for the current goal is (generated_topology_contains_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis R2 HR2sub).
rewrite the current goal using Hp1eq (from left to right).
An exact proof term for the current goal is (pair_Sigma U (λ_ : set ⇒ Y) x1 Hx1U y1 Hy1Y).
rewrite the current goal using Hp2eq (from left to right).
An exact proof term for the current goal is (pair_Sigma V (λ_ : set ⇒ Y) x2 Hx2V y2 Hy2Y).
We will prove R1 ∩ R2 = Empty.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ R1 ∩ R2.
We will prove p ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HpR1: p ∈ R1.
An exact proof term for the current goal is (binintersectE1 R1 R2 p Hp).
We prove the intermediate claim HpR2: p ∈ R2.
An exact proof term for the current goal is (binintersectE2 R1 R2 p Hp).
We prove the intermediate claim Hcoords1: ∃x ∈ U, ∃y ∈ Y, p ∈ setprod {x} {y}.
An exact proof term for the current goal is (setprod_elem_decompose U Y p HpR1).
Apply Hcoords1 to the current goal.
Let x be given.
Assume Hx_pair.
We prove the intermediate claim HxU': x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (∃y0 ∈ Y, p ∈ setprod {x} {y0}) Hx_pair).
We prove the intermediate claim Hexy: ∃y0 ∈ Y, p ∈ setprod {x} {y0}.
An exact proof term for the current goal is (andER (x ∈ U) (∃y0 ∈ Y, p ∈ setprod {x} {y0}) Hx_pair).
Apply Hexy to the current goal.
Let y be given.
Assume Hy_pair.
We prove the intermediate claim Hpsing1: p ∈ setprod {x} {y}.
An exact proof term for the current goal is (andER (y ∈ Y) (p ∈ setprod {x} {y}) Hy_pair).
We prove the intermediate claim Hcoords2: ∃x0 ∈ V, ∃y0 ∈ Y, p ∈ setprod {x0} {y0}.
An exact proof term for the current goal is (setprod_elem_decompose V Y p HpR2).
Apply Hcoords2 to the current goal.
Let x0 be given.
Assume Hx0_pair.
We prove the intermediate claim Hexy0: ∃y0 ∈ Y, p ∈ setprod {x0} {y0}.
An exact proof term for the current goal is (andER (x0 ∈ V) (∃y0 ∈ Y, p ∈ setprod {x0} {y0}) Hx0_pair).
Apply Hexy0 to the current goal.
Let y0 be given.
Assume Hy0_pair.
We prove the intermediate claim Hpsing2: p ∈ setprod {x0} {y0}.
An exact proof term for the current goal is (andER (y0 ∈ Y) (p ∈ setprod {x0} {y0}) Hy0_pair).
We prove the intermediate claim HxV': x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (y ∈ Y) (setprod_coords_in x y V Y p Hpsing1 HpR2)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU' HxV').
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVempty (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE False).
An exact proof term for the current goal is (Subq_Empty (R1 ∩ R2)).
∎