Let X, Tx, Y and Ty be given.
Assume HregX: regular_space X Tx.
Assume HregY: regular_space Y Ty.
Set Z to be the term setprod X Y.
Set Tz to be the term product_topology X Tx Y Ty.
We will prove regular_space Z Tz.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx HregX).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (regular_space_topology_on Y Ty HregY).
We prove the intermediate claim HTz: topology_on Z Tz.
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim Hhx: Hausdorff_space X Tx.
An exact proof term for the current goal is (regular_space_implies_Hausdorff X Tx HregX).
We prove the intermediate claim Hhy: Hausdorff_space Y Ty.
An exact proof term for the current goal is (regular_space_implies_Hausdorff Y Ty HregY).
We prove the intermediate claim Hhz: Hausdorff_space Z Tz.
An exact proof term for the current goal is (ex17_11_product_Hausdorff X Tx Y Ty Hhx Hhy).
We prove the intermediate claim HT1z: one_point_sets_closed Z Tz.
We will prove topology_on Z Tz ∧ ∀p : set, p ∈ Z → closed_in Z Tz {p}.
Apply andI to the current goal.
An exact proof term for the current goal is (Hausdorff_space_topology Z Tz Hhz).
Let p be given.
Assume HpZ: p ∈ Z.
An exact proof term for the current goal is (Hausdorff_singletons_closed Z Tz p Hhz HpZ).
We prove the intermediate claim Hclosure_prop: ∀p U : set, p ∈ Z → U ∈ Tz → p ∈ U → ∃V : set, V ∈ Tz ∧ p ∈ V ∧ closure_of Z Tz V ⊆ U.
Let p and U be given.
Assume HpZ: p ∈ Z.
Assume HU: U ∈ Tz.
Assume HpU: p ∈ U.
We prove the intermediate claim Hexb: ∃b ∈ product_subbasis X Tx Y Ty, p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine Z (product_subbasis X Tx Y Ty) U p HU HpU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (andEL (b ∈ product_subbasis X Tx Y Ty) (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) (andER (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ U) Hbpair)).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ U) (andER (b ∈ product_subbasis X Tx Y Ty) (p ∈ b ∧ b ⊆ U) Hbpair)).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbB).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0pair).
We prove the intermediate claim HbFam: b ∈ {rectangle_set U0 V|V ∈ Ty}.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0pair).
We prove the intermediate claim HexV0: ∃V0 ∈ Ty, b = rectangle_set U0 V0.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbFam).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pair.
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0pair).
We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.
An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0pair).
We prove the intermediate claim HpxX: (p 0) ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λx : set ⇒ Y) p HpZ).
We prove the intermediate claim HpyY: (p 1) ∈ Y.
An exact proof term for the current goal is (ap1_Sigma X (λx : set ⇒ Y) p HpZ).
We prove the intermediate claim Hrectmem: p ∈ setprod U0 V0.
We prove the intermediate claim Hpbrect: 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.
rewrite the current goal using (rectangle_set_def U0 V0) (from left to right) at position 1.
An exact proof term for the current goal is Hpbrect.
We prove the intermediate claim HpxU0: (p 0) ∈ U0.
An exact proof term for the current goal is (ap0_Sigma U0 (λx : set ⇒ V0) p Hrectmem).
We prove the intermediate claim HpyV0: (p 1) ∈ V0.
An exact proof term for the current goal is (ap1_Sigma U0 (λx : set ⇒ V0) p Hrectmem).
We prove the intermediate claim HexUx: ∃Ux : set, Ux ∈ Tx ∧ (p 0) ∈ Ux ∧ closure_of X Tx Ux ⊆ U0.
An exact proof term for the current goal is (regular_space_shrink_neighborhood X Tx (p 0) U0 HregX HpxX HU0Tx HpxU0).
Set Ux to be the term Eps_i (λUx0 : set ⇒ Ux0 ∈ Tx ∧ (p 0) ∈ Ux0 ∧ closure_of X Tx Ux0 ⊆ U0).
We prove the intermediate claim HUxprop: Ux ∈ Tx ∧ (p 0) ∈ Ux ∧ closure_of X Tx Ux ⊆ U0.
An exact proof term for the current goal is (Eps_i_ex (λUx0 : set ⇒ Ux0 ∈ Tx ∧ (p 0) ∈ Ux0 ∧ closure_of X Tx Ux0 ⊆ U0) HexUx).
We prove the intermediate claim HUx12: Ux ∈ Tx ∧ (p 0) ∈ Ux.
An exact proof term for the current goal is (andEL (Ux ∈ Tx ∧ (p 0) ∈ Ux) (closure_of X Tx Ux ⊆ U0) HUxprop).
We prove the intermediate claim HUxTx: Ux ∈ Tx.
An exact proof term for the current goal is (andEL (Ux ∈ Tx) ((p 0) ∈ Ux) HUx12).
We prove the intermediate claim HpUx: (p 0) ∈ Ux.
An exact proof term for the current goal is (andER (Ux ∈ Tx) ((p 0) ∈ Ux) HUx12).
We prove the intermediate claim HclUxSubU0: closure_of X Tx Ux ⊆ U0.
An exact proof term for the current goal is (andER (Ux ∈ Tx ∧ (p 0) ∈ Ux) (closure_of X Tx Ux ⊆ U0) HUxprop).
We prove the intermediate claim HexVy: ∃Vy : set, Vy ∈ Ty ∧ (p 1) ∈ Vy ∧ closure_of Y Ty Vy ⊆ V0.
An exact proof term for the current goal is (regular_space_shrink_neighborhood Y Ty (p 1) V0 HregY HpyY HV0Ty HpyV0).
Set Vy to be the term Eps_i (λVy0 : set ⇒ Vy0 ∈ Ty ∧ (p 1) ∈ Vy0 ∧ closure_of Y Ty Vy0 ⊆ V0).
We prove the intermediate claim HVyprop: Vy ∈ Ty ∧ (p 1) ∈ Vy ∧ closure_of Y Ty Vy ⊆ V0.
An exact proof term for the current goal is (Eps_i_ex (λVy0 : set ⇒ Vy0 ∈ Ty ∧ (p 1) ∈ Vy0 ∧ closure_of Y Ty Vy0 ⊆ V0) HexVy).
We prove the intermediate claim HVy12: Vy ∈ Ty ∧ (p 1) ∈ Vy.
An exact proof term for the current goal is (andEL (Vy ∈ Ty ∧ (p 1) ∈ Vy) (closure_of Y Ty Vy ⊆ V0) HVyprop).
We prove the intermediate claim HVyTy: Vy ∈ Ty.
An exact proof term for the current goal is (andEL (Vy ∈ Ty) ((p 1) ∈ Vy) HVy12).
We prove the intermediate claim HpVy: (p 1) ∈ Vy.
An exact proof term for the current goal is (andER (Vy ∈ Ty) ((p 1) ∈ Vy) HVy12).
We prove the intermediate claim HclVySubV0: closure_of Y Ty Vy ⊆ V0.
An exact proof term for the current goal is (andER (Vy ∈ Ty ∧ (p 1) ∈ Vy) (closure_of Y Ty Vy ⊆ V0) HVyprop).
Set V to be the term rectangle_set Ux Vy.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HVsub: V ∈ product_subbasis X Tx Y Ty.
We will prove V ∈ product_subbasis X Tx Y Ty.
We prove the intermediate claim HVfam: V ∈ {rectangle_set Ux V0|V0 ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set Ux V0) Vy HVyTy).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) Ux V HUxTx HVfam).
We prove the intermediate claim HTzDef: Tz = generated_topology (setprod X Y) (product_subbasis X Tx Y Ty).
Use reflexivity.
rewrite the current goal using HTzDef (from left to right).
We prove the intermediate claim HVpow: V ∈ 𝒫 (setprod X Y).
Apply (PowerI (setprod X Y) V) to the current goal.
Let q be given.
Assume Hq: q ∈ V.
We will prove q ∈ setprod X Y.
We prove the intermediate claim HqRect: q ∈ rectangle_set Ux Vy.
We prove the intermediate claim HVdef: V = rectangle_set Ux Vy.
Use reflexivity.
rewrite the current goal using HVdef (from left to right).
An exact proof term for the current goal is Hq.
We prove the intermediate claim HqProd: q ∈ setprod Ux Vy.
rewrite the current goal using (rectangle_set_def Ux Vy) (from right to left) at position 1.
An exact proof term for the current goal is HqRect.
We prove the intermediate claim HTxSub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HTySub: Ty ⊆ 𝒫 Y.
An exact proof term for the current goal is (topology_subset_axiom Y Ty HTy).
We prove the intermediate claim HUxPow: Ux ∈ 𝒫 X.
An exact proof term for the current goal is (HTxSub Ux HUxTx).
We prove the intermediate claim HVyPow: Vy ∈ 𝒫 Y.
An exact proof term for the current goal is (HTySub Vy HVyTy).
We prove the intermediate claim HUxSubX: Ux ⊆ X.
An exact proof term for the current goal is (PowerE X Ux HUxPow).
We prove the intermediate claim HVySubY: Vy ⊆ Y.
An exact proof term for the current goal is (PowerE Y Vy HVyPow).
We prove the intermediate claim HrectSub: setprod Ux Vy ⊆ setprod X Y.
An exact proof term for the current goal is (setprod_Subq Ux Vy X Y HUxSubX HVySubY).
An exact proof term for the current goal is (HrectSub q HqProd).
An exact proof term for the current goal is (generated_topology_contains_elem (setprod X Y) (product_subbasis X Tx Y Ty) V HVpow HVsub).
We prove the intermediate claim HVdef: V = rectangle_set Ux Vy.
Use reflexivity.
rewrite the current goal using HVdef (from left to right).
rewrite the current goal using (rectangle_set_def Ux Vy) (from left to right).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta X Y p HpZ).
rewrite the current goal using HpEta (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Ux Vy (p 0) (p 1) HpUx HpVy).
We prove the intermediate claim HclVeq: closure_of Z Tz V = setprod (closure_of X Tx Ux) (closure_of Y Ty Vy).
We prove the intermediate claim HVdef: V = rectangle_set Ux Vy.
Use reflexivity.
rewrite the current goal using HVdef (from left to right) at position 1.
rewrite the current goal using (rectangle_set_def Ux Vy) (from left to right) at position 1.
An exact proof term for the current goal is (ex17_9_closure_of_product_subset X Y Tx Ty Ux Vy HTx HTy).
We prove the intermediate claim HclSubRect: closure_of Z Tz V ⊆ setprod U0 V0.
rewrite the current goal using HclVeq (from left to right).
Apply (setprod_Subq (closure_of X Tx Ux) (closure_of Y Ty Vy) U0 V0) to the current goal.
An exact proof term for the current goal is HclUxSubU0.
An exact proof term for the current goal is HclVySubV0.
We prove the intermediate claim HrectSubU: setprod U0 V0 ⊆ U.
rewrite the current goal using (rectangle_set_def U0 V0) (from right to left).
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is HbsubU.
An exact proof term for the current goal is (Subq_tra (closure_of Z Tz V) (setprod U0 V0) U HclSubRect HrectSubU).
We prove the intermediate claim Hlemma: one_point_sets_closed Z Tz → (regular_space Z Tz ↔ ∀p U : set, p ∈ Z → U ∈ Tz → p ∈ U → ∃V : set, V ∈ Tz ∧ p ∈ V ∧ closure_of Z Tz V ⊆ U).
An exact proof term for the current goal is (andEL (one_point_sets_closed Z Tz → (regular_space Z Tz ↔ ∀p0 U0 : set, p0 ∈ Z → U0 ∈ Tz → p0 ∈ U0 → ∃V0 : set, V0 ∈ Tz ∧ p0 ∈ V0 ∧ closure_of Z Tz V0 ⊆ U0)) (one_point_sets_closed Z Tz → (normal_space Z Tz ↔ ∀A U0 : set, closed_in Z Tz A → U0 ∈ Tz → A ⊆ U0 → ∃V0 : set, V0 ∈ Tz ∧ A ⊆ V0 ∧ closure_of Z Tz V0 ⊆ U0)) (regular_normal_via_closure Z Tz HTz)).
We prove the intermediate claim Hiff: regular_space Z Tz ↔ ∀p U : set, p ∈ Z → U ∈ Tz → p ∈ U → ∃V : set, V ∈ Tz ∧ p ∈ V ∧ closure_of Z Tz V ⊆ U.
An exact proof term for the current goal is (Hlemma HT1z).
An exact proof term for the current goal is (iffER (regular_space Z Tz) (∀p U : set, p ∈ Z → U ∈ Tz → p ∈ U → ∃V : set, V ∈ Tz ∧ p ∈ V ∧ closure_of Z Tz V ⊆ U) Hiff Hclosure_prop).
∎