Let X, Tx and x be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
Set F to be the term {C ∈ 𝒫 X|connected_space C (subspace_topology X Tx C) ∧ x ∈ C}.
We prove the intermediate claim HFsub: ∀C : set, C ∈ F → C ⊆ X.
Let C be given.
Assume HCinF: C ∈ F.
We prove the intermediate claim HCpow: C ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0) C HCinF).
An exact proof term for the current goal is (PowerE X C HCpow).
We prove the intermediate claim HFconn: ∀C : set, C ∈ F → connected_space C (subspace_topology X Tx C).
Let C be given.
Assume HCinF: C ∈ F.
We prove the intermediate claim HCpair: connected_space C (subspace_topology X Tx C) ∧ x ∈ C.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0) C HCinF).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C)) (x ∈ C) HCpair).
We prove the intermediate claim Hcommon: ∃w : set, ∀C : set, C ∈ F → w ∈ C.
We use x to witness the existential quantifier.
Let C be given.
Assume HCinF: C ∈ F.
We prove the intermediate claim HCpair: connected_space C (subspace_topology X Tx C) ∧ x ∈ C.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0) C HCinF).
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C)) (x ∈ C) HCpair).
We prove the intermediate claim HUnionConn: connected_space (⋃ F) (subspace_topology X Tx (⋃ F)).
An exact proof term for the current goal is (union_connected_common_point X Tx F HTx HFsub HFconn Hcommon).
We prove the intermediate claim Heq: component_of X Tx x = ⋃ F.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ component_of X Tx x.
We will prove y ∈ ⋃ F.
We prove the intermediate claim HexC: ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C) y Hy).
Apply HexC to the current goal.
Let C be given.
Assume HC: connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
We prove the intermediate claim HCconn: connected_space C (subspace_topology X Tx C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C)) (x ∈ C) (andEL (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC)).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C)) (x ∈ C) (andEL (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC)).
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (connected_subspace_subset X Tx C HTx HCconn).
We prove the intermediate claim HCpow: C ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X C HCsubX).
We prove the intermediate claim HCinF: C ∈ F.
We will prove C ∈ {C0 ∈ 𝒫 X|connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HCpow.
We will prove connected_space C (subspace_topology X Tx C) ∧ x ∈ C.
Apply andI to the current goal.
An exact proof term for the current goal is HCconn.
An exact proof term for the current goal is HxC.
An exact proof term for the current goal is (UnionI F y C HyC HCinF).
Let y be given.
Assume Hy: y ∈ ⋃ F.
We will prove y ∈ component_of X Tx x.
Apply (UnionE F y Hy) to the current goal.
Let C be given.
Assume Hex: y ∈ C ∧ C ∈ F.
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (andEL (y ∈ C) (C ∈ F) Hex).
We prove the intermediate claim HCinF: C ∈ F.
An exact proof term for the current goal is (andER (y ∈ C) (C ∈ F) Hex).
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (HFsub C HCinF).
We prove the intermediate claim HCpair: connected_space C (subspace_topology X Tx C) ∧ x ∈ C.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0) C HCinF).
We prove the intermediate claim HCconn: connected_space C (subspace_topology X Tx C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C)) (x ∈ C) HCpair).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C)) (x ∈ C) HCpair).
We will prove y ∈ {y0 ∈ X|∃D : set, connected_space D (subspace_topology X Tx D) ∧ x ∈ D ∧ y0 ∈ D}.
Apply SepI to the current goal.
An exact proof term for the current goal is (HCsubX y HyC).
We will prove ∃D : set, connected_space D (subspace_topology X Tx D) ∧ x ∈ D ∧ y ∈ D.
We use C to witness the existential quantifier.
We will prove connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HCconn.
An exact proof term for the current goal is HxC.
An exact proof term for the current goal is HyC.
We will prove connected_space (component_of X Tx x) (subspace_topology X Tx (component_of X Tx x)).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HUnionConn.
∎