Apply andI to the current goal.

Let Y be given.

Assume HYsub: Y ⊆ X.

Assume HH: Hausdorff_space X Tx.

We will prove Hausdorff_space Y (subspace_topology X Tx Y).

An exact proof term for the current goal is (ex17_12_subspace_Hausdorff X Tx Y HH HYsub).

Let I and Xi be given.

Assume HHfam: Hausdorff_spaces_family I Xi.

An exact proof term for the current goal is (product_topology_full_Hausdorff_axiom I Xi HHfam).

Let Y be given.

Assume HYsub: Y ⊆ X.

Assume Hreg: regular_space X Tx.

We will prove one_point_sets_closed Y (subspace_topology X Tx Y) ∧ ∀y0 : set, y0 ∈ Y → ∀F0 : set, closed_in Y (subspace_topology X Tx Y) F0 → y0 ∉ F0 → ∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ y0 ∈ U ∧ F0 ⊆ V ∧ U ∩ V = Empty.

We prove the intermediate claim HTy: topology_on Y (subspace_topology X Tx Y).

An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).

We prove the intermediate claim HT1X: 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 HsingX: ∀x : set, x ∈ X → closed_in X Tx {x}.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → closed_in X Tx {x}) HT1X).

We prove the intermediate claim HsepX: ∀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.

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).

Apply andI to the current goal.

We will prove topology_on Y (subspace_topology X Tx Y) ∧ ∀y : set, y ∈ Y → closed_in Y (subspace_topology X Tx Y) {y}.

Apply andI to the current goal.

An exact proof term for the current goal is HTy.

Let y be given.

Assume HyY: y ∈ Y.

We will prove closed_in Y (subspace_topology X Tx Y) {y}.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HYsub y HyY).

Apply (iffER (closed_in Y (subspace_topology X Tx Y) {y}) (∃C : set, closed_in X Tx C ∧ {y} = C ∩ Y) (closed_in_subspace_iff_intersection X Tx Y {y} HTx HYsub)) to the current goal.

We use {y} to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (HsingX y HyX).

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ {y}.

We will prove z ∈ {y} ∩ Y.

We prove the intermediate claim Hzeq: z = y.

An exact proof term for the current goal is (SingE y z Hz).

rewrite the current goal using Hzeq (from left to right).

An exact proof term for the current goal is (binintersectI {y} Y y (SingI y) HyY).

Let z be given.

Assume Hz: z ∈ {y} ∩ Y.

We will prove z ∈ {y}.

An exact proof term for the current goal is (binintersectE1 {y} Y z Hz).

Let y be given.

Assume HyY: y ∈ Y.

Let F be given.

Assume HFcl: closed_in Y (subspace_topology X Tx Y) F.

Assume HynotF: y ∉ F.

We will prove ∃U V : set, U ∈ subspace_topology X Tx Y ∧ V ∈ subspace_topology X Tx Y ∧ y ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (HYsub y HyY).

We prove the intermediate claim HexC: ∃C : set, closed_in X Tx C ∧ F = C ∩ Y.

An exact proof term for the current goal is (iffEL (closed_in Y (subspace_topology X Tx Y) F) (∃C : set, closed_in X Tx C ∧ F = C ∩ Y) (closed_in_subspace_iff_intersection X Tx Y F HTx HYsub) HFcl).

Set C0 to be the term Eps_i (λC : set ⇒ closed_in X Tx C ∧ F = C ∩ Y).

We prove the intermediate claim HC0prop: closed_in X Tx C0 ∧ F = C0 ∩ Y.

An exact proof term for the current goal is (Eps_i_ex (λC : set ⇒ closed_in X Tx C ∧ F = C ∩ Y) HexC).

We prove the intermediate claim HC0cl: closed_in X Tx C0.

An exact proof term for the current goal is (andEL (closed_in X Tx C0) (F = C0 ∩ Y) HC0prop).

We prove the intermediate claim HFeq: F = C0 ∩ Y.

An exact proof term for the current goal is (andER (closed_in X Tx C0) (F = C0 ∩ Y) HC0prop).

We prove the intermediate claim HynotC0: y ∉ C0.

Assume HyC0: y ∈ C0.

We will prove False.

We prove the intermediate claim HyF: y ∈ F.

rewrite the current goal using HFeq (from left to right).

An exact proof term for the current goal is (binintersectI C0 Y y HyC0 HyY).

An exact proof term for the current goal is (HynotF HyF).

We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ y ∈ U ∧ C0 ⊆ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (HsepX y HyX C0 HC0cl HynotC0).

Set Ux to be the term Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ y ∈ U ∧ C0 ⊆ V ∧ U ∩ V = Empty).

We prove the intermediate claim HUxprop: ∃V : set, Ux ∈ Tx ∧ V ∈ Tx ∧ y ∈ Ux ∧ C0 ⊆ V ∧ Ux ∩ V = Empty.

An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ y ∈ U ∧ C0 ⊆ V ∧ U ∩ V = Empty) HexUV).

Set Vx to be the term Eps_i (λV : set ⇒ Ux ∈ Tx ∧ V ∈ Tx ∧ y ∈ Ux ∧ C0 ⊆ V ∧ Ux ∩ V = Empty).

We prove the intermediate claim HVxprop: Ux ∈ Tx ∧ Vx ∈ Tx ∧ y ∈ Ux ∧ C0 ⊆ Vx ∧ Ux ∩ Vx = Empty.

An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ Ux ∈ Tx ∧ V ∈ Tx ∧ y ∈ Ux ∧ C0 ⊆ V ∧ Ux ∩ V = Empty) HUxprop).

We prove the intermediate claim H1234: ((Ux ∈ Tx ∧ Vx ∈ Tx) ∧ y ∈ Ux) ∧ C0 ⊆ Vx.

An exact proof term for the current goal is (andEL (((Ux ∈ Tx ∧ Vx ∈ Tx) ∧ y ∈ Ux) ∧ C0 ⊆ Vx) (Ux ∩ Vx = Empty) HVxprop).

We prove the intermediate claim HdisjUV: Ux ∩ Vx = Empty.

An exact proof term for the current goal is (andER (((Ux ∈ Tx ∧ Vx ∈ Tx) ∧ y ∈ Ux) ∧ C0 ⊆ Vx) (Ux ∩ Vx = Empty) HVxprop).

We prove the intermediate claim H123: (Ux ∈ Tx ∧ Vx ∈ Tx) ∧ y ∈ Ux.

An exact proof term for the current goal is (andEL ((Ux ∈ Tx ∧ Vx ∈ Tx) ∧ y ∈ Ux) (C0 ⊆ Vx) H1234).

We prove the intermediate claim HC0subVx: C0 ⊆ Vx.

An exact proof term for the current goal is (andER ((Ux ∈ Tx ∧ Vx ∈ Tx) ∧ y ∈ Ux) (C0 ⊆ Vx) H1234).

We prove the intermediate claim H12: Ux ∈ Tx ∧ Vx ∈ Tx.

An exact proof term for the current goal is (andEL (Ux ∈ Tx ∧ Vx ∈ Tx) (y ∈ Ux) H123).

We prove the intermediate claim HyUx: y ∈ Ux.

An exact proof term for the current goal is (andER (Ux ∈ Tx ∧ Vx ∈ Tx) (y ∈ Ux) H123).

We prove the intermediate claim HUxTx: Ux ∈ Tx.

An exact proof term for the current goal is (andEL (Ux ∈ Tx) (Vx ∈ Tx) H12).

We prove the intermediate claim HVxTx: Vx ∈ Tx.

An exact proof term for the current goal is (andER (Ux ∈ Tx) (Vx ∈ Tx) H12).

Set U0 to be the term Ux ∩ Y.

Set V0 to be the term Vx ∩ Y.

We use U0 to witness the existential quantifier.

We use V0 to witness the existential quantifier.

Apply andI to the current goal.

We will prove U0 ∈ subspace_topology X Tx Y.

We prove the intermediate claim HU0subY: U0 ⊆ Y.

An exact proof term for the current goal is (binintersect_Subq_2 Ux Y).

We prove the intermediate claim HU0pow: U0 ∈ 𝒫 Y.

An exact proof term for the current goal is (PowerI Y U0 HU0subY).

We prove the intermediate claim HU0ex: ∃V ∈ Tx, U0 = V ∩ Y.

We use Ux to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HUxTx.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Y) (λU : set ⇒ ∃V ∈ Tx, U = V ∩ Y) U0 HU0pow HU0ex).

We will prove V0 ∈ subspace_topology X Tx Y.

We prove the intermediate claim HV0subY: V0 ⊆ Y.

An exact proof term for the current goal is (binintersect_Subq_2 Vx Y).

We prove the intermediate claim HV0pow: V0 ∈ 𝒫 Y.

An exact proof term for the current goal is (PowerI Y V0 HV0subY).

We prove the intermediate claim HV0ex: ∃V ∈ Tx, V0 = V ∩ Y.

We use Vx to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HVxTx.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Y) (λU : set ⇒ ∃V ∈ Tx, U = V ∩ Y) V0 HV0pow HV0ex).

An exact proof term for the current goal is (binintersectI Ux Y y HyUx HyY).

Let z be given.

Assume HzF: z ∈ F.

We will prove z ∈ V0.

We prove the intermediate claim HzCY: z ∈ C0 ∩ Y.

rewrite the current goal using HFeq (from right to left).

An exact proof term for the current goal is HzF.

We prove the intermediate claim HzC0: z ∈ C0.

An exact proof term for the current goal is (binintersectE1 C0 Y z HzCY).

We prove the intermediate claim HzY: z ∈ Y.

An exact proof term for the current goal is (binintersectE2 C0 Y z HzCY).

We prove the intermediate claim HzVx: z ∈ Vx.

An exact proof term for the current goal is (HC0subVx z HzC0).

An exact proof term for the current goal is (binintersectI Vx Y z HzVx HzY).

Apply Empty_Subq_eq to the current goal.

Let z be given.

Assume Hz: z ∈ U0 ∩ V0.

We will prove z ∈ Empty.

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 HzUx: z ∈ Ux.

An exact proof term for the current goal is (binintersectE1 Ux Y z HzU0).

We prove the intermediate claim HzVx: z ∈ Vx.

An exact proof term for the current goal is (binintersectE1 Vx Y z HzV0).

We prove the intermediate claim HzUV: z ∈ Ux ∩ Vx.

An exact proof term for the current goal is (binintersectI Ux Vx z HzUx HzVx).

rewrite the current goal using HdisjUV (from right to left).

An exact proof term for the current goal is HzUV.