An exact proof term for the current goal is (Hausdorff_space_topology X Tx HH).

Let x1 and x2 be given.

Assume Hx1: x1 ∈ X.

Assume Hx2: x2 ∈ X.

Assume Hneq: x1 ≠ x2.

An exact proof term for the current goal is (Hausdorff_space_separation X Tx x1 x2 HH Hx1 Hx2 Hneq).

Let V be given.

Assume HV: V ∈ UFam.

We prove the intermediate claim HVpred: ∃y : set, y ∈ X ∧ y ≠ x ∧ V ∈ Tx ∧ y ∈ V ∧ x ∉ V.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λV0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x ∧ V0 ∈ Tx ∧ y ∈ V0 ∧ x ∉ V0) V HV).

Apply HVpred to the current goal.

Let y be given.

Assume Hy_conj: y ∈ X ∧ y ≠ x ∧ V ∈ Tx ∧ y ∈ V ∧ x ∉ V.

We prove the intermediate claim H0: ((y ∈ X ∧ y ≠ x) ∧ V ∈ Tx) ∧ y ∈ V.

An exact proof term for the current goal is (andEL (((y ∈ X ∧ y ≠ x) ∧ V ∈ Tx) ∧ y ∈ V) (x ∉ V) Hy_conj).

We prove the intermediate claim H1: (y ∈ X ∧ y ≠ x) ∧ V ∈ Tx.

An exact proof term for the current goal is (andEL ((y ∈ X ∧ y ≠ x) ∧ V ∈ Tx) (y ∈ V) H0).

An exact proof term for the current goal is (andER (y ∈ X ∧ y ≠ x) (V ∈ Tx) H1).

An exact proof term for the current goal is (topology_union_closed X Tx UFam Htop HUFam_sub).

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ ⋃ UFam.

We will prove z ∈ X ∖ {x}.

Apply (UnionE_impred UFam z Hz (z ∈ X ∖ {x})) to the current goal.

Let V be given.

Assume HzV: z ∈ V.

Assume HV: V ∈ UFam.

We prove the intermediate claim HVpow: V ∈ 𝒫 X.

An exact proof term for the current goal is (SepE1 (𝒫 X) (λV0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x ∧ V0 ∈ Tx ∧ y ∈ V0 ∧ x ∉ V0) V HV).

We prove the intermediate claim HVsubX: V ⊆ X.

An exact proof term for the current goal is (PowerE X V HVpow).

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (HVsubX z HzV).

We prove the intermediate claim HVpred: ∃y : set, y ∈ X ∧ y ≠ x ∧ V ∈ Tx ∧ y ∈ V ∧ x ∉ V.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λV0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x ∧ V0 ∈ Tx ∧ y ∈ V0 ∧ x ∉ V0) V HV).

Apply HVpred to the current goal.

Let y be given.

Assume Hy_conj: y ∈ X ∧ y ≠ x ∧ V ∈ Tx ∧ y ∈ V ∧ x ∉ V.

We prove the intermediate claim HxNotV: x ∉ V.

An exact proof term for the current goal is (andER (((y ∈ X ∧ y ≠ x) ∧ V ∈ Tx) ∧ y ∈ V) (x ∉ V) Hy_conj).

We prove the intermediate claim HznotSing: z ∉ {x}.

Assume HzSing: z ∈ {x}.

We prove the intermediate claim Hzeq: z = x.

An exact proof term for the current goal is (SingE x z HzSing).

We prove the intermediate claim HxV: x ∈ V.

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

An exact proof term for the current goal is HzV.

An exact proof term for the current goal is (HxNotV HxV).

An exact proof term for the current goal is (setminusI X {x} z HzX HznotSing).

Let z be given.

Assume Hz: z ∈ X ∖ {x}.

We will prove z ∈ ⋃ UFam.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (setminusE1 X {x} z Hz).

We prove the intermediate claim HznotSing: z ∉ {x}.

An exact proof term for the current goal is (setminusE2 X {x} z Hz).

We prove the intermediate claim Hzneq: z ≠ x.

Assume Hzeq: z = x.

We prove the intermediate claim HzSing: z ∈ {x}.

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

An exact proof term for the current goal is (SingI x).

An exact proof term for the current goal is (HznotSing HzSing).

We prove the intermediate claim HexUV: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ z ∈ V ∧ U ∩ V = Empty.

An exact proof term for the current goal is (HSep x z HxX HzX (neq_i_sym z x Hzneq)).

Apply HexUV to the current goal.

Let U be given.

Assume HexV: ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ z ∈ V ∧ U ∩ V = Empty.

Apply HexV to the current goal.

Let V be given.

Assume Hconj: U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ z ∈ V ∧ U ∩ V = Empty.

We prove the intermediate claim Hconj1: ((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) ∧ z ∈ V.

An exact proof term for the current goal is (andEL (((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) ∧ z ∈ V) (U ∩ V = Empty) Hconj).

We prove the intermediate claim HUVempty: U ∩ V = Empty.

An exact proof term for the current goal is (andER (((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) ∧ z ∈ V) (U ∩ V = Empty) Hconj).

We prove the intermediate claim Hconj2: (U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U.

An exact proof term for the current goal is (andEL ((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) (z ∈ V) Hconj1).

We prove the intermediate claim HUV1: U ∈ Tx ∧ V ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ V ∈ Tx) (x ∈ U) Hconj2).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ V ∈ Tx) (x ∈ U) Hconj2).

We prove the intermediate claim HVTx: V ∈ Tx.

An exact proof term for the current goal is (andER (U ∈ Tx) (V ∈ Tx) HUV1).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (andER ((U ∈ Tx ∧ V ∈ Tx) ∧ x ∈ U) (z ∈ V) Hconj1).

We prove the intermediate claim HxNotV: x ∉ V.

Assume HxV: x ∈ V.

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 HxEmp: 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 HxEmp False).

We prove the intermediate claim HVpow: V ∈ 𝒫 X.

We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.

An exact proof term for the current goal is (topology_subset_axiom X Tx Htop).

An exact proof term for the current goal is (HTsub V HVTx).

We prove the intermediate claim HVin: V ∈ UFam.

Apply (SepI (𝒫 X) (λV0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x ∧ V0 ∈ Tx ∧ y ∈ V0 ∧ x ∉ V0) V HVpow) to the current goal.

We use z to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HzX.

An exact proof term for the current goal is Hzneq.

An exact proof term for the current goal is HVTx.

An exact proof term for the current goal is HzV.

An exact proof term for the current goal is HxNotV.

An exact proof term for the current goal is (UnionI UFam z V HzV HVin).