Let X and Tx be given.
Assume Hloc: locally_connected X Tx.
Let x be given.
Assume HxX: x ∈ X.
We will prove open_in X Tx (component_of X Tx x).
We will prove topology_on X Tx ∧ component_of X Tx x ∈ Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_connected_topology X Tx Hloc).
We prove the intermediate claim Hlocprop: ∀y : set, y ∈ X → ∀U : set, U ∈ Tx → y ∈ U → ∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ U ∧ connected_space V (subspace_topology X Tx V).
Let y be given.
Assume Hy: y ∈ X.
Let U be given.
Assume HU: U ∈ Tx.
Assume HyU: y ∈ U.
An exact proof term for the current goal is (locally_connected_local X Tx y U Hloc Hy HU HyU).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Set Comp to be the term component_of X Tx x.
Set UFam to be the term {V ∈ Tx|V ⊆ Comp ∧ connected_space V (subspace_topology X Tx V)}.
We prove the intermediate claim HUFsub: UFam ⊆ Tx.
Let V be given.
Assume HV: V ∈ UFam.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ V0 ⊆ Comp ∧ connected_space V0 (subspace_topology X Tx V0)) V HV).
We prove the intermediate claim HUnionTx: ⋃ UFam ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx UFam HTx HUFsub).
We prove the intermediate claim HUnionEq: ⋃ UFam = Comp.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ UFam.
Apply (UnionE UFam y Hy) to the current goal.
Let V be given.
Assume Hex: y ∈ V ∧ V ∈ UFam.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andEL (y ∈ V) (V ∈ UFam) Hex).
We prove the intermediate claim HVUF: V ∈ UFam.
An exact proof term for the current goal is (andER (y ∈ V) (V ∈ UFam) Hex).
We prove the intermediate claim HVpair: V ⊆ Comp ∧ connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ V0 ⊆ Comp ∧ connected_space V0 (subspace_topology X Tx V0)) V HVUF).
We prove the intermediate claim HVsubComp: V ⊆ Comp.
An exact proof term for the current goal is (andEL (V ⊆ Comp) (connected_space V (subspace_topology X Tx V)) HVpair).
An exact proof term for the current goal is (HVsubComp y HyV).
Let y be given.
Assume Hy: y ∈ Comp.
We prove the intermediate claim HyX: y ∈ X.
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).
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ X ∧ connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (Hlocprop y HyX X HXTx HyX).
Apply HexV to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ y ∈ V ∧ V ⊆ X ∧ connected_space V (subspace_topology X Tx V).
We prove the intermediate claim HVpre: ((V ∈ Tx ∧ y ∈ V) ∧ V ⊆ X).
An exact proof term for the current goal is (andEL ((V ∈ Tx ∧ y ∈ V) ∧ V ⊆ X) (connected_space V (subspace_topology X Tx V)) HV).
We prove the intermediate claim HVconn: connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (andER ((V ∈ Tx ∧ y ∈ V) ∧ V ⊆ X) (connected_space V (subspace_topology X Tx V)) HV).
We prove the intermediate claim HVTx_y: V ∈ Tx ∧ y ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ y ∈ V) (V ⊆ X) HVpre).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (y ∈ V) HVTx_y).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (y ∈ V) HVTx_y).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ y ∈ V) (V ⊆ X) HVpre).
We prove the intermediate claim HcompEq: component_of X Tx y = component_of X Tx x.
An exact proof term for the current goal is (component_of_eq_if_in X Tx x y HTx HxX Hy).
We prove the intermediate claim HVsubComp: V ⊆ Comp.
Let z be given.
Assume HzV: z ∈ V.
We will prove z ∈ Comp.
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 HzCompy: z ∈ component_of X Tx y.
We will prove z ∈ {y0 ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ y ∈ C ∧ y0 ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is HzX.
We will prove ∃C : set, connected_space C (subspace_topology X Tx C) ∧ y ∈ C ∧ z ∈ C.
We use V to witness the existential quantifier.
We will prove connected_space V (subspace_topology X Tx V) ∧ y ∈ V ∧ z ∈ V.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HVconn.
An exact proof term for the current goal is HyV.
An exact proof term for the current goal is HzV.
rewrite the current goal using HcompEq (from right to left).
An exact proof term for the current goal is HzCompy.
We prove the intermediate claim HVinUFam: V ∈ UFam.
We will prove V ∈ {V0 ∈ Tx|V0 ⊆ Comp ∧ connected_space V0 (subspace_topology X Tx V0)}.
Apply SepI to the current goal.
An exact proof term for the current goal is HVTx.
We will prove V ⊆ Comp ∧ connected_space V (subspace_topology X Tx V).
Apply andI to the current goal.
An exact proof term for the current goal is HVsubComp.
An exact proof term for the current goal is HVconn.
An exact proof term for the current goal is (UnionI UFam y V HyV HVinUFam).
We prove the intermediate claim HCompTx: Comp ∈ Tx.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionTx.
An exact proof term for the current goal is HCompTx.
∎