Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove (∀x : set, component_of X Tx x ⊆ quasicomponent_of X Tx x) ∧ (locally_connected X Tx → ∀x : set, x ∈ X → component_of X Tx x = quasicomponent_of X Tx x).
We prove the intermediate claim Hsub: ∀x : set, component_of X Tx x ⊆ quasicomponent_of X Tx x.
Let x be given.
We will prove component_of X Tx x ⊆ quasicomponent_of X Tx x.
Let y be given.
Assume Hy: y ∈ component_of X Tx x.
We will prove y ∈ quasicomponent_of X Tx x.
We will prove y ∈ {y0 ∈ X|∀U : set, open_in X Tx U → closed_in X Tx U → x ∈ U → y0 ∈ U}.
Apply SepI to the current goal.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C) y Hy).
Let U be given.
Assume HUopen: open_in X Tx U.
Assume HUclosed: closed_in X Tx U.
Assume HxU: x ∈ U.
We will prove y ∈ U.
Apply (xm (U = X)) to the current goal.
Assume HUeqX: U = X.
rewrite the current goal using HUeqX (from left to right).
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C) y Hy).
Assume HUnX: U ≠ X.
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (open_in_subset X Tx U HUopen).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty U x HxU).
We prove the intermediate claim HsepUX: separation_of X U (X ∖ U).
An exact proof term for the current goal is (separation_of_complement X U HUsubX HUne HUnX).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (U ∈ Tx) HUopen).
We prove the intermediate claim HcompOpen: open_in X Tx (X ∖ U).
An exact proof term for the current goal is (open_of_closed_complement X Tx U HUclosed).
We prove the intermediate claim HcompinTx: (X ∖ U) ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) ((X ∖ U) ∈ Tx) HcompOpen).
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.
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 Hside: C ⊆ U ∨ C ⊆ (X ∖ U).
An exact proof term for the current goal is (connected_subset_in_separation_side X Tx U (X ∖ U) C HTx HCsubX HCconn HUinTx HcompinTx HsepUX).
Apply (Hside (y ∈ U)) to the current goal.
Assume HCsubU: C ⊆ U.
An exact proof term for the current goal is (HCsubU y HyC).
Assume HCsubComp: C ⊆ (X ∖ U).
We prove the intermediate claim HxComp: x ∈ X ∖ U.
An exact proof term for the current goal is (HCsubComp x HxC).
We prove the intermediate claim HxNotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxComp).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotU HxU).
We prove the intermediate claim Heq: locally_connected X Tx → ∀x : set, x ∈ X → component_of X Tx x = quasicomponent_of X Tx x.
Assume Hloc: locally_connected X Tx.
Let x be given.
Assume HxX: x ∈ X.
We will prove component_of X Tx x = quasicomponent_of X Tx x.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ component_of X Tx x.
An exact proof term for the current goal is (Hsub x y Hy).
Let y be given.
Assume HyQ: y ∈ quasicomponent_of X Tx x.
We will prove y ∈ component_of X Tx x.
We prove the intermediate claim HUopen: open_in X Tx (component_of X Tx x).
An exact proof term for the current goal is (components_are_open_in_locally_connected X Tx Hloc x HxX).
We prove the intermediate claim HUclosed: closed_in X Tx (component_of X Tx x).
An exact proof term for the current goal is (components_are_closed X Tx HTx x HxX).
We prove the intermediate claim HxU: x ∈ component_of X Tx x.
An exact proof term for the current goal is (point_in_component X Tx x HTx HxX).
We prove the intermediate claim Hprop: ∀U : set, open_in X Tx U → closed_in X Tx U → x ∈ U → y ∈ U.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∀U : set, open_in X Tx U → closed_in X Tx U → x ∈ U → y0 ∈ U) y HyQ).
An exact proof term for the current goal is (Hprop (component_of X Tx x) HUopen HUclosed HxU).
Apply andI to the current goal.
An exact proof term for the current goal is Hsub.
An exact proof term for the current goal is Heq.
∎