Let X, Tx, x and y be given.
Assume Hreg: regular_space X Tx.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
Assume Hneq: x ≠ y.
We will prove ∃U V : set, open_in X Tx U ∧ open_in X Tx V ∧ x ∈ U ∧ y ∈ V ∧ closure_of X Tx U ∩ closure_of X Tx V = Empty.
We prove the intermediate claim HT1: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).
We prove the intermediate claim Hsing: ∀t : set, t ∈ X → closed_in X Tx {t}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1).
We prove the intermediate claim HSepReg: ∀t : set, t ∈ X → ∀F : set, closed_in X Tx F → t ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ t ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim Hcly: closed_in X Tx {y}.
An exact proof term for the current goal is (Hsing y Hy).
We prove the intermediate claim Hxnoty: x ∉ {y}.
Assume Hxy: x ∈ {y}.
We prove the intermediate claim Heq: x = y.
An exact proof term for the current goal is (SingE y x Hxy).
An exact proof term for the current goal is (Hneq Heq).
We prove the intermediate claim Hex1: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ {y} ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSepReg x Hx {y} Hcly Hxnoty).
Set U0 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ {y} ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HU0ex: ∃V : set, U0 ∈ Tx ∧ V ∈ Tx ∧ x ∈ U0 ∧ {y} ⊆ V ∧ U0 ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ {y} ⊆ V ∧ U ∩ V = Empty) Hex1).
Set V0 to be the term Eps_i (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ x ∈ U0 ∧ {y} ⊆ V ∧ U0 ∩ V = Empty).
We prove the intermediate claim HV0prop: U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ {y} ⊆ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U0 ∈ Tx ∧ V ∈ Tx ∧ x ∈ U0 ∧ {y} ⊆ V ∧ U0 ∩ V = Empty) HU0ex).
We prove the intermediate claim H1234: (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ∧ {y} ⊆ V0).
An exact proof term for the current goal is (andEL ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ∧ {y} ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim Hdisj0: U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER ((((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ∧ {y} ⊆ V0)) (U0 ∩ V0 = Empty) HV0prop).
We prove the intermediate claim H123: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0).
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ({y} ⊆ V0) H1234).
We prove the intermediate claim H12: (U0 ∈ Tx ∧ V0 ∈ Tx).
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (x ∈ U0) H123).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (x ∈ U0) H123).
We prove the intermediate claim HysubV0: {y} ⊆ V0.
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ({y} ⊆ V0) H1234).
We prove the intermediate claim HyV0: y ∈ V0.
Apply HysubV0 to the current goal.
An exact proof term for the current goal is (SingI y).
We prove the intermediate claim Hcliffy: y ∈ closure_of X Tx U0 ↔ (∀W ∈ Tx, y ∈ W → W ∩ U0 ≠ Empty).
An exact proof term for the current goal is (closure_characterization X Tx U0 y HTx Hy).
We prove the intermediate claim HyNotClU0: y ∉ closure_of X Tx U0.
Assume HyCl: y ∈ closure_of X Tx U0.
We prove the intermediate claim Hneigh: ∀W ∈ Tx, y ∈ W → W ∩ U0 ≠ Empty.
An exact proof term for the current goal is (iffEL (y ∈ closure_of X Tx U0) (∀W ∈ Tx, y ∈ W → W ∩ U0 ≠ Empty) Hcliffy HyCl).
We prove the intermediate claim Hempty: V0 ∩ U0 = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ V0 ∩ U0.
We will prove z ∈ Empty.
We prove the intermediate claim HzV: z ∈ V0.
An exact proof term for the current goal is (binintersectE1 V0 U0 z Hz).
We prove the intermediate claim HzU: z ∈ U0.
An exact proof term for the current goal is (binintersectE2 V0 U0 z Hz).
We prove the intermediate claim HzUV: z ∈ U0 ∩ V0.
An exact proof term for the current goal is (binintersectI U0 V0 z HzU HzV).
We prove the intermediate claim HzE: z ∈ Empty.
rewrite the current goal using Hdisj0 (from right to left).
An exact proof term for the current goal is HzUV.
An exact proof term for the current goal is HzE.
We prove the intermediate claim Hcontr: V0 ∩ U0 ≠ Empty.
An exact proof term for the current goal is (Hneigh V0 HV0Tx HyV0).
Apply FalseE to the current goal.
Apply FalseE to the current goal.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontr Hempty).
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HU0sub: U0 ⊆ X.
An exact proof term for the current goal is (PowerE X U0 (HTsub U0 HU0Tx)).
We prove the intermediate claim HclU0: closed_in X Tx (closure_of X Tx U0).
An exact proof term for the current goal is (closure_is_closed X Tx U0 HTx HU0sub).
We prove the intermediate claim Hex2: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ y ∈ U ∧ closure_of X Tx U0 ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HSepReg y Hy (closure_of X Tx U0) HclU0 HyNotClU0).
Set U1 to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ y ∈ U ∧ closure_of X Tx U0 ⊆ V ∧ U ∩ V = Empty).
We prove the intermediate claim HU1ex: ∃V : set, U1 ∈ Tx ∧ V ∈ Tx ∧ y ∈ U1 ∧ closure_of X Tx U0 ⊆ V ∧ U1 ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ y ∈ U ∧ closure_of X Tx U0 ⊆ V ∧ U ∩ V = Empty) Hex2).
Set V1 to be the term Eps_i (λV : set ⇒ U1 ∈ Tx ∧ V ∈ Tx ∧ y ∈ U1 ∧ closure_of X Tx U0 ⊆ V ∧ U1 ∩ V = Empty).
We prove the intermediate claim HV1prop: U1 ∈ Tx ∧ V1 ∈ Tx ∧ y ∈ U1 ∧ closure_of X Tx U0 ⊆ V1 ∧ U1 ∩ V1 = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ U1 ∈ Tx ∧ V ∈ Tx ∧ y ∈ U1 ∧ closure_of X Tx U0 ⊆ V ∧ U1 ∩ V = Empty) HU1ex).
We prove the intermediate claim H1234b: (((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ y ∈ U1) ∧ closure_of X Tx U0 ⊆ V1).
An exact proof term for the current goal is (andEL ((((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ y ∈ U1) ∧ closure_of X Tx U0 ⊆ V1)) (U1 ∩ V1 = Empty) HV1prop).
We prove the intermediate claim Hdisj1: U1 ∩ V1 = Empty.
An exact proof term for the current goal is (andER ((((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ y ∈ U1) ∧ closure_of X Tx U0 ⊆ V1)) (U1 ∩ V1 = Empty) HV1prop).
We prove the intermediate claim H123b: ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ y ∈ U1).
An exact proof term for the current goal is (andEL ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ y ∈ U1) (closure_of X Tx U0 ⊆ V1) H1234b).
We prove the intermediate claim H12b: (U1 ∈ Tx ∧ V1 ∈ Tx).
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ V1 ∈ Tx) (y ∈ U1) H123b).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (V1 ∈ Tx) H12b).
We prove the intermediate claim HV1Tx: V1 ∈ Tx.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (V1 ∈ Tx) H12b).
We prove the intermediate claim HyU1: y ∈ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ V1 ∈ Tx) (y ∈ U1) H123b).
We prove the intermediate claim HclU0subV1: closure_of X Tx U0 ⊆ V1.
An exact proof term for the current goal is (andER ((U1 ∈ Tx ∧ V1 ∈ Tx) ∧ y ∈ U1) (closure_of X Tx U0 ⊆ V1) H1234b).
We prove the intermediate claim Hcliff: ∀z : set, z ∈ X → (z ∈ closure_of X Tx U1 ↔ (∀W ∈ Tx, z ∈ W → W ∩ U1 ≠ Empty)).
Let z be given.
Assume HzX: z ∈ X.
An exact proof term for the current goal is (closure_characterization X Tx U1 z HTx HzX).
We prove the intermediate claim Hcldisj: closure_of X Tx U0 ∩ closure_of X Tx U1 = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ closure_of X Tx U0 ∩ closure_of X Tx U1.
We will prove z ∈ Empty.
We prove the intermediate claim Hzcl0: z ∈ closure_of X Tx U0.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx U0) (closure_of X Tx U1) z Hz).
We prove the intermediate claim Hzcl1: z ∈ closure_of X Tx U1.
An exact proof term for the current goal is (binintersectE2 (closure_of X Tx U0) (closure_of X Tx U1) z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∀W : set, W ∈ Tx → z0 ∈ W → W ∩ U0 ≠ Empty) z Hzcl0).
We prove the intermediate claim HzV1: z ∈ V1.
Apply HclU0subV1 to the current goal.
An exact proof term for the current goal is Hzcl0.
We prove the intermediate claim Hneigh: ∀W ∈ Tx, z ∈ W → W ∩ U1 ≠ Empty.
An exact proof term for the current goal is (iffEL (z ∈ closure_of X Tx U1) (∀W ∈ Tx, z ∈ W → W ∩ U1 ≠ Empty) (Hcliff z HzX) Hzcl1).
We prove the intermediate claim Hcontr: V1 ∩ U1 ≠ Empty.
An exact proof term for the current goal is (Hneigh V1 HV1Tx HzV1).
We prove the intermediate claim Hempty: V1 ∩ U1 = Empty.
Apply Empty_Subq_eq to the current goal.
Let w be given.
Assume Hw: w ∈ V1 ∩ U1.
We will prove w ∈ Empty.
We prove the intermediate claim HwV: w ∈ V1.
An exact proof term for the current goal is (binintersectE1 V1 U1 w Hw).
We prove the intermediate claim HwU: w ∈ U1.
An exact proof term for the current goal is (binintersectE2 V1 U1 w Hw).
We prove the intermediate claim HwUV: w ∈ U1 ∩ V1.
An exact proof term for the current goal is (binintersectI U1 V1 w HwU HwV).
We prove the intermediate claim HwE: w ∈ Empty.
rewrite the current goal using Hdisj1 (from right to left).
An exact proof term for the current goal is HwUV.
An exact proof term for the current goal is HwE.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hcontr Hempty).
We use U0 to witness the existential quantifier.
We use U1 to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is (andI (topology_on X Tx) (U0 ∈ Tx) HTx HU0Tx).
An exact proof term for the current goal is (andI (topology_on X Tx) (U1 ∈ Tx) HTx HU1Tx).
An exact proof term for the current goal is HxU0.
An exact proof term for the current goal is HyU1.
An exact proof term for the current goal is Hcldisj.
∎