Let X and Tx be given.
Assume Htop: topology_on X Tx.
We will prove Hausdorff_space X Tx ↔ closed_in (setprod X X) (product_topology X Tx X Tx) {(x,x)|x ∈ X}.
Apply iffI to the current goal.
Assume HH: Hausdorff_space X Tx.
We will prove closed_in (setprod X X) (product_topology X Tx X Tx) {(x,x)|x ∈ X}.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
We prove the intermediate claim HSep: ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
Set D to be the term {(t,t)|t ∈ X}.
Set U to be the term setprod X X ∖ D.
We prove the intermediate claim HTprod: topology_on (setprod X X) (product_topology X Tx X Tx).
An exact proof term for the current goal is (product_topology_is_topology X Tx X Tx HTx HTx).
We prove the intermediate claim HDsub: D ⊆ setprod X X.
Let p be given.
Assume HpD: p ∈ D.
Apply (ReplE X (λt : set ⇒ (t,t)) p HpD) to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (p = (x,x)) Hxpair).
We prove the intermediate claim Hpeq: p = (x,x).
An exact proof term for the current goal is (andER (x ∈ X) (p = (x,x)) Hxpair).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x x HxX HxX).
We prove the intermediate claim HUinProd: U ∈ product_topology X Tx X Tx.
We will prove U ∈ product_topology X Tx X Tx.
We will prove U ∈ generated_topology (setprod X X) (product_subbasis X Tx X Tx).
We prove the intermediate claim HUPow: U ∈ 𝒫 (setprod X X).
Apply PowerI (setprod X X) U to the current goal.
An exact proof term for the current goal is (setminus_Subq (setprod X X) D).
We prove the intermediate claim Hprop: ∀p ∈ U, ∃b ∈ product_subbasis X Tx X Tx, p ∈ b ∧ b ⊆ U.
Let p be given.
Assume HpU: p ∈ U.
We prove the intermediate claim HpXY: p ∈ setprod X X.
An exact proof term for the current goal is (setminusE1 (setprod X X) D p HpU).
We prove the intermediate claim HpnotD: p ∉ D.
An exact proof term for the current goal is (setminusE2 (setprod X X) D p HpU).
Apply (Sigma_E X (λ_ : set ⇒ X) p HpXY) to the current goal.
Let x be given.
Assume Hxpair.
Apply Hxpair to the current goal.
Assume HxX Hexy.
Apply Hexy to the current goal.
Let y be given.
Assume Hypair.
Apply Hypair to the current goal.
Assume HyX Hpeq.
We prove the intermediate claim Hxy: x ≠ y.
Assume HxyEq: x = y.
We prove the intermediate claim HpInD: p ∈ D.
We prove the intermediate claim Hex: ∃t ∈ X, p = (t,t).
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using HxyEq (from right to left).
An exact proof term for the current goal is (tuple_pair x x).
An exact proof term for the current goal is (iffER (p ∈ D) (∃t ∈ X, p = (t,t)) (ReplEq X (λt : set ⇒ (t,t)) p) Hex).
An exact proof term for the current goal is (HpnotD HpInD).
We prove the intermediate claim HexUV: ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ y ∈ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (HSep x y HxX HyX Hxy).
Apply HexUV to the current goal.
Let U0 be given.
Assume HexV0.
Apply HexV0 to the current goal.
Let V0 be given.
Assume HUV_conj.
Apply HUV_conj to the current goal.
Assume Hleft HUVempty.
Apply Hleft to the current goal.
Assume Hleft2 HyV0.
Apply Hleft2 to the current goal.
Assume Hleft3 HxU0.
Apply Hleft3 to the current goal.
Assume HU0 HV0.
Set b to be the term rectangle_set U0 V0.
We use b to witness the existential quantifier.
Apply andI to the current goal.
We will prove b ∈ product_subbasis X Tx X Tx.
We prove the intermediate claim HbV: rectangle_set U0 V0 ∈ {rectangle_set U0 V|V ∈ Tx}.
An exact proof term for the current goal is (ReplI Tx (λV : set ⇒ rectangle_set U0 V) V0 HV0).
An exact proof term for the current goal is (famunionI Tx (λU1 : set ⇒ {rectangle_set U1 V|V ∈ Tx}) U0 (rectangle_set U0 V0) HU0 HbV).
Apply andI to the current goal.
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (pair_Sigma U0 (λ_ : set ⇒ V0) x HxU0 y HyV0).
We will prove b ⊆ U.
Let q be given.
Assume Hqb: q ∈ b.
We will prove q ∈ U.
Apply setminusI to the current goal.
We prove the intermediate claim HU0subX: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0).
We prove the intermediate claim HV0subX: V0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V0 HTx HV0).
An exact proof term for the current goal is (setprod_Subq U0 V0 X X HU0subX HV0subX q Hqb).
Assume HqD: q ∈ D.
Apply (ReplE X (λt : set ⇒ (t,t)) q HqD) to the current goal.
Let z be given.
Assume Hzconj.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (q = (z,z)) Hzconj).
We prove the intermediate claim Hqeq: q = (z,z).
An exact proof term for the current goal is (andER (z ∈ X) (q = (z,z)) Hzconj).
We prove the intermediate claim Hsing: q ∈ setprod {z} {z}.
rewrite the current goal using Hqeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {z} {z} z z (SingI z) (SingI z)).
We prove the intermediate claim HzUV: z ∈ U0 ∧ z ∈ V0.
An exact proof term for the current goal is (setprod_coords_in z z U0 V0 q Hsing Hqb).
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (andEL (z ∈ U0) (z ∈ V0) HzUV).
We prove the intermediate claim HzV0: z ∈ V0.
An exact proof term for the current goal is (andER (z ∈ U0) (z ∈ V0) HzUV).
We prove the intermediate claim HzInt: z ∈ U0 ∩ V0.
An exact proof term for the current goal is (binintersectI U0 V0 z HzU0 HzV0).
We prove the intermediate claim HzE: z ∈ Empty.
rewrite the current goal using HUVempty (from right to left).
An exact proof term for the current goal is HzInt.
An exact proof term for the current goal is (EmptyE z HzE).
An exact proof term for the current goal is (SepI (𝒫 (setprod X X)) (λU0 : set ⇒ ∀p0 ∈ U0, ∃b ∈ product_subbasis X Tx X Tx, p0 ∈ b ∧ b ⊆ U0) U HUPow Hprop).
We will prove topology_on (setprod X X) (product_topology X Tx X Tx) ∧ (D ⊆ setprod X X ∧ ∃W ∈ product_topology X Tx X Tx, D = setprod X X ∖ W).
Apply andI to the current goal.
An exact proof term for the current goal is HTprod.
Apply andI to the current goal.
An exact proof term for the current goal is HDsub.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUinProd.
We will prove D = setprod X X ∖ U.
rewrite the current goal using (setminus_setminus_eq (setprod X X) D HDsub) (from left to right).
Use reflexivity.
Assume Hclosed: closed_in (setprod X X) (product_topology X Tx X Tx) {(x,x)|x ∈ X}.
We will prove Hausdorff_space X Tx.
Set D to be the term {(t,t)|t ∈ X}.
We prove the intermediate claim HDsub: D ⊆ setprod X X.
An exact proof term for the current goal is (andEL (D ⊆ setprod X X) (∃U ∈ product_topology X Tx X Tx, D = setprod X X ∖ U) (andER (topology_on (setprod X X) (product_topology X Tx X Tx)) (D ⊆ setprod X X ∧ ∃U ∈ product_topology X Tx X Tx, D = setprod X X ∖ U) Hclosed)).
We prove the intermediate claim HexU: ∃U ∈ product_topology X Tx X Tx, D = setprod X X ∖ U.
An exact proof term for the current goal is (andER (D ⊆ setprod X X) (∃U ∈ product_topology X Tx X Tx, D = setprod X X ∖ U) (andER (topology_on (setprod X X) (product_topology X Tx X Tx)) (D ⊆ setprod X X ∧ ∃U ∈ product_topology X Tx X Tx, D = setprod X X ∖ U) Hclosed)).
Apply HexU to the current goal.
Let U be given.
Assume HUconj.
We prove the intermediate claim HUopen: U ∈ product_topology X Tx X Tx.
An exact proof term for the current goal is (andEL (U ∈ product_topology X Tx X Tx) (D = setprod X X ∖ U) HUconj).
We prove the intermediate claim HDeq: D = setprod X X ∖ U.
An exact proof term for the current goal is (andER (U ∈ product_topology X Tx X Tx) (D = setprod X X ∖ U) HUconj).
We prove the intermediate claim HUsubXY: U ⊆ setprod X X.
An exact proof term for the current goal is (generated_topology_subset (setprod X X) (product_subbasis X Tx X Tx) U HUopen).
We prove the intermediate claim HcompEq: setprod X X ∖ D = U.
rewrite the current goal using HDeq (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq (setprod X X) U HUsubXY).
We will prove topology_on X Tx ∧ ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x1 ∈ U0 ∧ x2 ∈ V0 ∧ U0 ∩ V0 = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Let x1 and x2 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx2X: x2 ∈ X.
Assume Hx12: x1 ≠ x2.
We will prove ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x1 ∈ U0 ∧ x2 ∈ V0 ∧ U0 ∩ V0 = Empty.
Set p to be the term (x1,x2).
We prove the intermediate claim HpNotD: p ∉ D.
Assume HpD: p ∈ D.
Apply (ReplE X (λt : set ⇒ (t,t)) p HpD) to the current goal.
Let z be given.
Assume Hzconj.
We prove the intermediate claim Hpeq: p = (z,z).
An exact proof term for the current goal is (andER (z ∈ X) (p = (z,z)) Hzconj).
We prove the intermediate claim HpSing: p ∈ setprod {x1} {x2}.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x1} {x2} x1 x2 (SingI x1) (SingI x2)).
We prove the intermediate claim HzzIn: (z,z) ∈ setprod {x1} {x2}.
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is HpSing.
We prove the intermediate claim HzzSing: (z,z) ∈ setprod {z} {z}.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {z} {z} z z (SingI z) (SingI z)).
We prove the intermediate claim HzIn: z ∈ {x1} ∧ z ∈ {x2}.
An exact proof term for the current goal is (setprod_coords_in z z {x1} {x2} (z,z) HzzSing HzzIn).
We prove the intermediate claim Hzx1: z ∈ {x1}.
An exact proof term for the current goal is (andEL (z ∈ {x1}) (z ∈ {x2}) HzIn).
We prove the intermediate claim Hzx2: z ∈ {x2}.
An exact proof term for the current goal is (andER (z ∈ {x1}) (z ∈ {x2}) HzIn).
We prove the intermediate claim HzEqx1: z = x1.
An exact proof term for the current goal is (SingE x1 z Hzx1).
We prove the intermediate claim HzEqx2: z = x2.
An exact proof term for the current goal is (SingE x2 z Hzx2).
We prove the intermediate claim Hx12eq: x1 = x2.
rewrite the current goal using HzEqx1 (from right to left).
rewrite the current goal using HzEqx2 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (Hx12 Hx12eq).
We prove the intermediate claim HpInU: p ∈ U.
rewrite the current goal using HcompEq (from right to left).
An exact proof term for the current goal is (setminusI (setprod X X) D p (tuple_2_setprod_by_pair_Sigma X X x1 x2 Hx1X Hx2X) HpNotD).
We prove the intermediate claim HUprop: ∀z ∈ U, ∃b ∈ product_subbasis X Tx X Tx, z ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X X)) (λU0 : set ⇒ ∀p0 ∈ U0, ∃b ∈ product_subbasis X Tx X Tx, p0 ∈ b ∧ b ⊆ U0) U HUopen).
We prove the intermediate claim Hexb: ∃b ∈ product_subbasis X Tx X Tx, p ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop p HpInU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbconj.
We prove the intermediate claim HbSub: b ∈ product_subbasis X Tx X Tx.
An exact proof term for the current goal is (andEL (b ∈ product_subbasis X Tx X Tx) (p ∈ b ∧ b ⊆ U) Hbconj).
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 X Tx) (p ∈ b ∧ b ⊆ U) Hbconj)).
We prove the intermediate claim HbU: b ⊆ U.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ U) (andER (b ∈ product_subbasis X Tx X Tx) (p ∈ b ∧ b ⊆ U) Hbconj)).
Apply (famunionE Tx (λU1 : set ⇒ {rectangle_set U1 V|V ∈ Tx}) b HbSub) to the current goal.
Let U0 be given.
Assume HU0conj.
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 ∈ Tx}) HU0conj).
We prove the intermediate claim HbInRepl: b ∈ {rectangle_set U0 V|V ∈ Tx}.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (b ∈ {rectangle_set U0 V|V ∈ Tx}) HU0conj).
Apply (ReplE Tx (λV : set ⇒ rectangle_set U0 V) b HbInRepl) to the current goal.
Let V0 be given.
Assume HV0conj.
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (b = rectangle_set U0 V0) HV0conj).
We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (b = rectangle_set U0 V0) HV0conj).
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.
We prove the intermediate claim HpSing: p ∈ setprod {x1} {x2}.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x1} {x2} x1 x2 (SingI x1) (SingI x2)).
We prove the intermediate claim Hcoords: x1 ∈ U0 ∧ x2 ∈ V0.
An exact proof term for the current goal is (setprod_coords_in x1 x2 U0 V0 p HpSing HpbRect).
We prove the intermediate claim Hx1U0: x1 ∈ U0.
An exact proof term for the current goal is (andEL (x1 ∈ U0) (x2 ∈ V0) Hcoords).
We prove the intermediate claim Hx2V0: x2 ∈ V0.
An exact proof term for the current goal is (andER (x1 ∈ U0) (x2 ∈ V0) Hcoords).
We prove the intermediate claim HUVempty: U0 ∩ V0 = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ U0 ∩ V0.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 V0 z Hz).
We prove the intermediate claim HzV0: z ∈ V0.
An exact proof term for the current goal is (binintersectE2 U0 V0 z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 Htop HU0Tx z HzU0).
Set q to be the term (z,z).
We prove the intermediate claim HqInb: q ∈ rectangle_set U0 V0.
An exact proof term for the current goal is (tuple_2_rectangle_set U0 V0 z z HzU0 HzV0).
We prove the intermediate claim HqInb0: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is HqInb.
We prove the intermediate claim HqInU: q ∈ U.
An exact proof term for the current goal is (HbU q HqInb0).
We prove the intermediate claim HqInD: q ∈ D.
An exact proof term for the current goal is (ReplI X (λt : set ⇒ (t,t)) z HzX).
We prove the intermediate claim HqNotU: q ∉ U.
We prove the intermediate claim HqXYU: q ∈ setprod X X ∖ U.
rewrite the current goal using HDeq (from right to left).
An exact proof term for the current goal is HqInD.
An exact proof term for the current goal is (setminusE2 (setprod X X) U q HqXYU).
An exact proof term for the current goal is (HqNotU HqInU).
An exact proof term for the current goal is (Subq_Empty (U0 ∩ V0)).
We use U0 to witness the existential quantifier.
We use V0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0Tx.
An exact proof term for the current goal is HV0Tx.
An exact proof term for the current goal is Hx1U0.
An exact proof term for the current goal is Hx2V0.
An exact proof term for the current goal is HUVempty.
∎