Let x be given.

Assume HxX: x ∈ X.

We use (component_of X Tx x) to witness the existential quantifier.

We will prove component_of X Tx x ∈ {component_of X Tx x0|x0 ∈ X} ∧ x ∈ component_of X Tx x.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ component_of X Tx x0) x HxX).

We will prove x ∈ component_of X Tx x.

We will prove x ∈ {y ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C}.

Apply SepI to the current goal.

An exact proof term for the current goal is HxX.

We will prove ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ x ∈ C.

We use {x} to witness the existential quantifier.

We will prove connected_space {x} (subspace_topology X Tx {x}) ∧ x ∈ {x} ∧ x ∈ {x}.

Apply andI to the current goal.

An exact proof term for the current goal is (singleton_subspace_connected X Tx x HTx HxX).

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

Let U and V be given.

Assume HU: U ∈ {component_of X Tx x|x ∈ X}.

Assume HV: V ∈ {component_of X Tx x|x ∈ X}.

Assume Hneq: U ≠ V.

We will prove U ∩ V = Empty.

Apply (ReplE_impred X (λx0 : set ⇒ component_of X Tx x0) U HU) to the current goal.

Let x1 be given.

Assume Hx1X: x1 ∈ X.

Assume HUeq: U = component_of X Tx x1.

Apply (ReplE_impred X (λx0 : set ⇒ component_of X Tx x0) V HV) to the current goal.

Let x2 be given.

Assume Hx2X: x2 ∈ X.

Assume HVeql: V = component_of X Tx x2.

Apply Empty_eq to the current goal.

Let z be given.

Assume Hz: z ∈ U ∩ V.

Apply (binintersectE U V z Hz) to the current goal.

Assume HzU: z ∈ U.

Assume HzV: z ∈ V.

We prove the intermediate claim HzComp1: z ∈ component_of X Tx x1.

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

An exact proof term for the current goal is HzU.

We prove the intermediate claim HzComp2: z ∈ component_of X Tx x2.

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

An exact proof term for the current goal is HzV.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x1 ∈ C ∧ y0 ∈ C) z HzComp1).

We prove the intermediate claim Heq1: component_of X Tx z = component_of X Tx x1.

An exact proof term for the current goal is (component_of_eq_if_in X Tx x1 z HTx Hx1X HzComp1).

We prove the intermediate claim Heq2: component_of X Tx z = component_of X Tx x2.

An exact proof term for the current goal is (component_of_eq_if_in X Tx x2 z HTx Hx2X HzComp2).

We prove the intermediate claim HcompEq: component_of X Tx x1 = component_of X Tx x2.

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

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

Use reflexivity.

We prove the intermediate claim HUVeq: U = V.

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

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

An exact proof term for the current goal is HcompEq.

Apply FalseE to the current goal.

An exact proof term for the current goal is (Hneq HUVeq).