Let X and Tx be given.
Assume Hlpc: locally_path_connected X Tx.
Let x be given.
Assume Hx: x ∈ X.
We will prove open_in X Tx (path_component_of X Tx x).
We will prove topology_on X Tx ∧ path_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_path_connected_topology X Tx Hlpc).
We prove the intermediate claim Hlpcprop: ∀x0 : set, x0 ∈ X → ∀U : set, U ∈ Tx → x0 ∈ U → ∃V : set, V ∈ Tx ∧ x0 ∈ V ∧ V ⊆ U ∧ path_connected_space V (subspace_topology X Tx V).
Let x0 be given.
Assume Hx0: x0 ∈ X.
Let U be given.
Assume HU: U ∈ Tx.
Assume Hx0U: x0 ∈ U.
An exact proof term for the current goal is (locally_path_connected_local X Tx x0 U Hlpc Hx0 HU Hx0U).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Set P to be the term path_component_of X Tx x.
Set Fam to be the term {V ∈ Tx|V ⊆ P ∧ path_connected_space V (subspace_topology X Tx V)}.
We prove the intermediate claim HFsub: Fam ⊆ Tx.
Let V be given.
Assume HV: V ∈ Fam.
An exact proof term for the current goal is (SepE1 Tx (λV0 : set ⇒ V0 ⊆ P ∧ path_connected_space V0 (subspace_topology X Tx V0)) V HV).
We prove the intermediate claim HUnionTx: ⋃ Fam ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx Fam HTx HFsub).
We prove the intermediate claim HUnionEq: ⋃ Fam = P.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ Fam.
Apply (UnionE Fam y Hy) to the current goal.
Let V be given.
Assume Hex: y ∈ V ∧ V ∈ Fam.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andEL (y ∈ V) (V ∈ Fam) Hex).
We prove the intermediate claim HVFam: V ∈ Fam.
An exact proof term for the current goal is (andER (y ∈ V) (V ∈ Fam) Hex).
We prove the intermediate claim HVpair: V ⊆ P ∧ path_connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (SepE2 Tx (λV0 : set ⇒ V0 ⊆ P ∧ path_connected_space V0 (subspace_topology X Tx V0)) V HVFam).
We prove the intermediate claim HVsubP: V ⊆ P.
An exact proof term for the current goal is (andEL (V ⊆ P) (path_connected_space V (subspace_topology X Tx V)) HVpair).
An exact proof term for the current goal is (HVsubP y HyV).
Let y be given.
Assume HyP: y ∈ P.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃p : set, function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) y HyP).
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 ∧ path_connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (Hlpcprop y HyX X HXTx HyX).
Apply HexV to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ y ∈ V ∧ V ⊆ X ∧ path_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) (path_connected_space V (subspace_topology X Tx V)) HV).
We prove the intermediate claim HVpath: path_connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (andER ((V ∈ Tx ∧ y ∈ V) ∧ V ⊆ X) (path_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 HVsubP: V ⊆ P.
Let z be given.
Assume HzV: z ∈ V.
We will prove z ∈ P.
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 HzPcy: z ∈ path_component_of X Tx y.
An exact proof term for the current goal is (subspace_path_connected_implies_in_path_component X Tx V y z HTx HVsubX HVpath HyV HzV).
An exact proof term for the current goal is (path_component_transitive_axiom X Tx x y z HTx Hx HyX HzX HyP HzPcy).
We prove the intermediate claim HVinFam: V ∈ Fam.
We will prove V ∈ {V0 ∈ Tx|V0 ⊆ P ∧ path_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 ⊆ P ∧ path_connected_space V (subspace_topology X Tx V).
Apply andI to the current goal.
An exact proof term for the current goal is HVsubP.
An exact proof term for the current goal is HVpath.
An exact proof term for the current goal is (UnionI Fam y V HyV HVinFam).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionTx.
∎