Let X, Tx and U be given.
Assume Hlpc: locally_path_connected X Tx.
Assume HU: open_in X Tx U.
Assume Hconn: connected_space U (subspace_topology X Tx U).
We will prove path_connected_space U (subspace_topology X Tx U).
Set Tu to be the term subspace_topology X Tx U.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → ∀V : set, V ∈ Tx → x ∈ V → ∃W : set, W ∈ Tx ∧ x ∈ W ∧ W ⊆ V ∧ path_connected_space W (subspace_topology X Tx W)) Hlpc).
We prove the intermediate claim Hlpcprop: ∀x : set, x ∈ X → ∀V : set, V ∈ Tx → x ∈ V → ∃W : set, W ∈ Tx ∧ x ∈ W ∧ W ⊆ V ∧ path_connected_space W (subspace_topology X Tx W).
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → ∀V : set, V ∈ Tx → x ∈ V → ∃W : set, W ∈ Tx ∧ x ∈ W ∧ W ⊆ V ∧ path_connected_space W (subspace_topology X Tx W)) Hlpc).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (open_in_subset X Tx U HU).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HU).
We prove the intermediate claim HtopU: topology_on U Tu.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx U HTx HUsubX).
We prove the intermediate claim HlpcU: locally_path_connected U Tu.
We will prove topology_on U Tu ∧ ∀x : set, x ∈ U → ∀V : set, V ∈ Tu → x ∈ V → ∃W : set, W ∈ Tu ∧ x ∈ W ∧ W ⊆ V ∧ path_connected_space W (subspace_topology U Tu W).
Apply andI to the current goal.
An exact proof term for the current goal is HtopU.
Let x be given.
Assume HxU: x ∈ U.
Let V be given.
Assume HV: V ∈ Tu.
Assume HxV: x ∈ V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate claim HVpowU: V ∈ 𝒫 U.
An exact proof term for the current goal is (SepE1 (𝒫 U) (λV0 : set ⇒ ∃W0 ∈ Tx, V0 = W0 ∩ U) V HV).
We prove the intermediate claim HVrep: ∃W0 ∈ Tx, V = W0 ∩ U.
An exact proof term for the current goal is (SepE2 (𝒫 U) (λV0 : set ⇒ ∃W0 ∈ Tx, V0 = W0 ∩ U) V HV).
Apply HVrep to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0: W0 ∈ Tx.
An exact proof term for the current goal is (andEL (W0 ∈ Tx) (V = W0 ∩ U) HW0pair).
We prove the intermediate claim HVeql: V = W0 ∩ U.
An exact proof term for the current goal is (andER (W0 ∈ Tx) (V = W0 ∩ U) HW0pair).
We prove the intermediate claim HxWU: x ∈ W0 ∩ U.
rewrite the current goal using HVeql (from right to left).
An exact proof term for the current goal is HxV.
We prove the intermediate claim HxW0: x ∈ W0.
An exact proof term for the current goal is (binintersectE1 W0 U x HxWU).
We prove the intermediate claim HWUinTx: (W0 ∩ U) ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx W0 U HTx HW0 HUinTx).
We prove the intermediate claim HexW: ∃W : set, W ∈ Tx ∧ x ∈ W ∧ W ⊆ (W0 ∩ U) ∧ path_connected_space W (subspace_topology X Tx W).
An exact proof term for the current goal is (Hlpcprop x HxX (W0 ∩ U) HWUinTx HxWU).
Apply HexW to the current goal.
Let W be given.
Assume HW.
We prove the intermediate claim HWL: (W ∈ Tx ∧ x ∈ W) ∧ W ⊆ (W0 ∩ U).
An exact proof term for the current goal is (andEL ((W ∈ Tx ∧ x ∈ W) ∧ W ⊆ (W0 ∩ U)) (path_connected_space W (subspace_topology X Tx W)) HW).
We prove the intermediate claim HWpath: path_connected_space W (subspace_topology X Tx W).
An exact proof term for the current goal is (andER ((W ∈ Tx ∧ x ∈ W) ∧ W ⊆ (W0 ∩ U)) (path_connected_space W (subspace_topology X Tx W)) HW).
We prove the intermediate claim HW12: W ∈ Tx ∧ x ∈ W.
An exact proof term for the current goal is (andEL (W ∈ Tx ∧ x ∈ W) (W ⊆ (W0 ∩ U)) HWL).
We prove the intermediate claim HWsubWU: W ⊆ (W0 ∩ U).
An exact proof term for the current goal is (andER (W ∈ Tx ∧ x ∈ W) (W ⊆ (W0 ∩ U)) HWL).
We prove the intermediate claim HWTx: W ∈ Tx.
An exact proof term for the current goal is (andEL (W ∈ Tx) (x ∈ W) HW12).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (andER (W ∈ Tx) (x ∈ W) HW12).
We prove the intermediate claim HWsubU: W ⊆ U.
Let z be given.
Assume HzW: z ∈ W.
We prove the intermediate claim HzWU: z ∈ W0 ∩ U.
An exact proof term for the current goal is (HWsubWU z HzW).
An exact proof term for the current goal is (binintersectE2 W0 U z HzWU).
We prove the intermediate claim HWpowU: W ∈ 𝒫 U.
An exact proof term for the current goal is (PowerI U W HWsubU).
We prove the intermediate claim HWUeq: W = W ∩ U.
Apply set_ext to the current goal.
Let z be given.
Assume HzW: z ∈ W.
An exact proof term for the current goal is (binintersectI W U z HzW (HWsubU z HzW)).
Let z be given.
Assume HzWU: z ∈ W ∩ U.
An exact proof term for the current goal is (binintersectE1 W U z HzWU).
We prove the intermediate claim HWTu: W ∈ Tu.
We prove the intermediate claim HexWopen: open_in U Tu W.
We prove the intermediate claim Hex: ∃V0 ∈ Tx, W = V0 ∩ U.
We use W to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HWTx.
An exact proof term for the current goal is HWUeq.
An exact proof term for the current goal is (iffER (open_in U Tu W) (∃V0 ∈ Tx, W = V0 ∩ U) (open_in_subspace_iff X Tx U W HTx HUsubX HWsubU) Hex).
An exact proof term for the current goal is (open_in_elem U Tu W HexWopen).
We prove the intermediate claim Hsubtrans: subspace_topology U Tu W = subspace_topology X Tx W.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx U W HTx HUsubX HWsubU).
We prove the intermediate claim HWpathU: path_connected_space W (subspace_topology U Tu W).
rewrite the current goal using Hsubtrans (from left to right).
An exact proof term for the current goal is HWpath.
We use W to witness the existential quantifier.
We will prove W ∈ Tu ∧ x ∈ W ∧ W ⊆ V ∧ path_connected_space W (subspace_topology U Tu W).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HWTu.
An exact proof term for the current goal is HxW.
We will prove W ⊆ V.
rewrite the current goal using HVeql (from left to right).
An exact proof term for the current goal is HWsubWU.
An exact proof term for the current goal is HWpathU.
We will prove topology_on U Tu ∧ ∀x y : set, x ∈ U → y ∈ U → ∃p : set, path_between U x y p ∧ continuous_map unit_interval unit_interval_topology U Tu p.
Apply andI to the current goal.
An exact proof term for the current goal is HtopU.
Let x and y be given.
Assume HxU: x ∈ U.
Assume HyU: y ∈ U.
Set Pc to be the term path_component_of U Tu x.
We prove the intermediate claim HPcOpen: open_in U Tu Pc.
An exact proof term for the current goal is (path_components_open U Tu HlpcU x HxU).
We prove the intermediate claim HPcInTu: Pc ∈ Tu.
An exact proof term for the current goal is (open_in_elem U Tu Pc HPcOpen).
We prove the intermediate claim HxPc: x ∈ Pc.
An exact proof term for the current goal is (path_component_reflexive U Tu x HtopU HxU).
We prove the intermediate claim HPcNe: Pc ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty Pc x HxPc).
Set D to be the term U ∖ Pc.
Set Fam to be the term {path_component_of U Tu z|z ∈ D}.
We prove the intermediate claim HFsub: Fam ⊆ Tu.
Let W be given.
Assume HW: W ∈ Fam.
Apply (ReplE_impred D (λz : set ⇒ path_component_of U Tu z) W HW) to the current goal.
Let z be given.
Assume HzD: z ∈ D.
Assume HWeq: W = path_component_of U Tu z.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (setminusE1 U Pc z HzD).
We prove the intermediate claim Hopenz: open_in U Tu (path_component_of U Tu z).
An exact proof term for the current goal is (path_components_open U Tu HlpcU z HzU).
We prove the intermediate claim HinTu: path_component_of U Tu z ∈ Tu.
An exact proof term for the current goal is (open_in_elem U Tu (path_component_of U Tu z) Hopenz).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HinTu.
We prove the intermediate claim HUnionTu: ⋃ Fam ∈ Tu.
An exact proof term for the current goal is (topology_union_closed U Tu Fam HtopU HFsub).
We prove the intermediate claim HUnionEq: ⋃ Fam = D.
We prove the intermediate claim Heqrel: (∀z : set, z ∈ U → z ∈ path_component_of U Tu z) ∧ (∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b) ∧ (∀a b c : set, a ∈ U → b ∈ U → c ∈ U → b ∈ path_component_of U Tu a → c ∈ path_component_of U Tu b → c ∈ path_component_of U Tu a).
An exact proof term for the current goal is (path_components_equivalence_relation U Tu HtopU).
We prove the intermediate claim H12: (∀z : set, z ∈ U → z ∈ path_component_of U Tu z) ∧ (∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b).
An exact proof term for the current goal is (andEL ((∀z : set, z ∈ U → z ∈ path_component_of U Tu z) ∧ (∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b)) (∀a b c : set, a ∈ U → b ∈ U → c ∈ U → b ∈ path_component_of U Tu a → c ∈ path_component_of U Tu b → c ∈ path_component_of U Tu a) Heqrel).
We prove the intermediate claim Hrefl: ∀z : set, z ∈ U → z ∈ path_component_of U Tu z.
An exact proof term for the current goal is (andEL (∀z : set, z ∈ U → z ∈ path_component_of U Tu z) (∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b) H12).
We prove the intermediate claim Hsym: ∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b.
An exact proof term for the current goal is (andER (∀z : set, z ∈ U → z ∈ path_component_of U Tu z) (∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b) H12).
We prove the intermediate claim Htrans: ∀a b c : set, a ∈ U → b ∈ U → c ∈ U → b ∈ path_component_of U Tu a → c ∈ path_component_of U Tu b → c ∈ path_component_of U Tu a.
An exact proof term for the current goal is (andER ((∀z : set, z ∈ U → z ∈ path_component_of U Tu z) ∧ (∀a b : set, a ∈ U → b ∈ U → b ∈ path_component_of U Tu a → a ∈ path_component_of U Tu b)) (∀a b c : set, a ∈ U → b ∈ U → c ∈ U → b ∈ path_component_of U Tu a → c ∈ path_component_of U Tu b → c ∈ path_component_of U Tu a) Heqrel).
Apply set_ext to the current goal.
Let t be given.
Assume HtU: t ∈ ⋃ Fam.
Apply (UnionE Fam t HtU) to the current goal.
Let W be given.
Assume Hex: t ∈ W ∧ W ∈ Fam.
We prove the intermediate claim HWt: t ∈ W.
An exact proof term for the current goal is (andEL (t ∈ W) (W ∈ Fam) Hex).
We prove the intermediate claim HWFam: W ∈ Fam.
An exact proof term for the current goal is (andER (t ∈ W) (W ∈ Fam) Hex).
We prove the intermediate claim HWdef: ∃z ∈ D, W = path_component_of U Tu z.
An exact proof term for the current goal is (ReplE D (λz : set ⇒ path_component_of U Tu z) W HWFam).
Apply HWdef to the current goal.
Let z be given.
Assume Hzpair.
We prove the intermediate claim HzD: z ∈ D.
An exact proof term for the current goal is (andEL (z ∈ D) (W = path_component_of U Tu z) Hzpair).
We prove the intermediate claim HWeq: W = path_component_of U Tu z.
An exact proof term for the current goal is (andER (z ∈ D) (W = path_component_of U Tu z) Hzpair).
We prove the intermediate claim HtW: t ∈ W.
An exact proof term for the current goal is HWt.
We prove the intermediate claim HtPc_z: t ∈ path_component_of U Tu z.
rewrite the current goal using HWeq (from right to left).
An exact proof term for the current goal is HtW.
We prove the intermediate claim HtU0: t ∈ U.
An exact proof term for the current goal is (SepE1 U (λy0 : set ⇒ ∃p : set, function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p ∧ apply_fun p 0 = z ∧ apply_fun p 1 = y0) t HtPc_z).
We will prove t ∈ D.
We will prove t ∈ U ∖ Pc.
Apply setminusI to the current goal.
An exact proof term for the current goal is HtU0.
Assume HtPc: t ∈ Pc.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (setminusE1 U Pc z HzD).
We prove the intermediate claim HzNotPc: z ∉ Pc.
An exact proof term for the current goal is (setminusE2 U Pc z HzD).
We prove the intermediate claim HzPc_t: z ∈ path_component_of U Tu t.
An exact proof term for the current goal is (Hsym z t HzU HtU0 HtPc_z).
We prove the intermediate claim HzPc_x: z ∈ path_component_of U Tu x.
An exact proof term for the current goal is (Htrans x t z HxU HtU0 HzU HtPc HzPc_t).
An exact proof term for the current goal is (HzNotPc HzPc_x).
Let t be given.
Assume HtD: t ∈ D.
We will prove t ∈ ⋃ Fam.
We prove the intermediate claim HtU0: t ∈ U.
An exact proof term for the current goal is (setminusE1 U Pc t HtD).
We prove the intermediate claim HtFam: path_component_of U Tu t ∈ Fam.
An exact proof term for the current goal is (ReplI D (λz : set ⇒ path_component_of U Tu z) t HtD).
We prove the intermediate claim HtPc_t: t ∈ path_component_of U Tu t.
An exact proof term for the current goal is (Hrefl t HtU0).
An exact proof term for the current goal is (UnionI Fam t (path_component_of U Tu t) HtPc_t HtFam).
We prove the intermediate claim HDinTu: D ∈ Tu.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionTu.
We prove the intermediate claim HPcClosed: closed_in U Tu Pc.
Apply (closed_inI U Tu Pc) to the current goal.
An exact proof term for the current goal is HtopU.
We will prove Pc ⊆ U.
Let t be given.
Assume HtPc: t ∈ Pc.
An exact proof term for the current goal is (SepE1 U (λy0 : set ⇒ ∃p : set, function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) t HtPc).
We use D to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HDinTu.
Apply set_ext to the current goal.
Let t be given.
Assume HtPc: t ∈ Pc.
We will prove t ∈ U ∖ D.
Apply setminusI to the current goal.
An exact proof term for the current goal is (SepE1 U (λy0 : set ⇒ ∃p : set, function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) t HtPc).
Assume HtD: t ∈ D.
We prove the intermediate claim HtNotPc: t ∉ Pc.
An exact proof term for the current goal is (setminusE2 U Pc t HtD).
An exact proof term for the current goal is (HtNotPc HtPc).
Let t be given.
Assume HtUD: t ∈ U ∖ D.
We prove the intermediate claim HtU: t ∈ U.
An exact proof term for the current goal is (setminusE1 U D t HtUD).
We prove the intermediate claim HtNotD: t ∉ D.
An exact proof term for the current goal is (setminusE2 U D t HtUD).
Apply (xm (t ∈ Pc)) to the current goal.
Assume HtPc: t ∈ Pc.
An exact proof term for the current goal is HtPc.
Assume HtNotPc: t ∉ Pc.
Apply FalseE to the current goal.
Apply HtNotD to the current goal.
An exact proof term for the current goal is (setminusI U Pc t HtU HtNotPc).
We prove the intermediate claim HnoClopen: ¬ (∃B : set, B ≠ Empty ∧ B ≠ U ∧ open_in U Tu B ∧ closed_in U Tu B).
An exact proof term for the current goal is (iffEL (connected_space U Tu) (¬ (∃B : set, B ≠ Empty ∧ B ≠ U ∧ open_in U Tu B ∧ closed_in U Tu B)) (connected_iff_no_nontrivial_clopen U Tu HtopU) Hconn).
We prove the intermediate claim HPcEqU: Pc = U.
Apply (xm (Pc = U)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hneq: Pc ≠ U.
Apply FalseE to the current goal.
Apply HnoClopen to the current goal.
We use Pc to witness the existential quantifier.
We will prove Pc ≠ Empty ∧ Pc ≠ U ∧ open_in U Tu Pc ∧ closed_in U Tu Pc.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HPcNe.
An exact proof term for the current goal is Hneq.
An exact proof term for the current goal is HPcOpen.
An exact proof term for the current goal is HPcClosed.
We prove the intermediate claim HyPc: y ∈ Pc.
rewrite the current goal using HPcEqU (from left to right).
An exact proof term for the current goal is HyU.
We prove the intermediate claim HexPath: ∃p : set, function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y.
An exact proof term for the current goal is (SepE2 U (λy0 : set ⇒ ∃p : set, function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y0) y HyPc).
Apply HexPath to the current goal.
Let p be given.
Assume Hp.
We use p to witness the existential quantifier.
We will prove path_between U x y p ∧ continuous_map unit_interval unit_interval_topology U Tu p.
We prove the intermediate claim HpAB0: (function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p) ∧ apply_fun p 0 = x.
An exact proof term for the current goal is (andEL ((function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) Hp).
We prove the intermediate claim Hp1: apply_fun p 1 = y.
An exact proof term for the current goal is (andER ((function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) Hp).
We prove the intermediate claim HpAB: function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p.
An exact proof term for the current goal is (andEL (function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p) (apply_fun p 0 = x) HpAB0).
We prove the intermediate claim Hp0: apply_fun p 0 = x.
An exact proof term for the current goal is (andER (function_on p unit_interval U ∧ continuous_map unit_interval unit_interval_topology U Tu p) (apply_fun p 0 = x) HpAB0).
We prove the intermediate claim HpFun: function_on p unit_interval U.
An exact proof term for the current goal is (andEL (function_on p unit_interval U) (continuous_map unit_interval unit_interval_topology U Tu p) HpAB).
We prove the intermediate claim HpCont: continuous_map unit_interval unit_interval_topology U Tu p.
An exact proof term for the current goal is (andER (function_on p unit_interval U) (continuous_map unit_interval unit_interval_topology U Tu p) HpAB).
Apply andI to the current goal.
We will prove function_on p unit_interval U ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpFun.
An exact proof term for the current goal is Hp0.
An exact proof term for the current goal is Hp1.
An exact proof term for the current goal is HpCont.
∎