Let X and Tx be given.
Assume Hlpc: locally_path_connected X Tx.
Let x be given.
Assume Hx: x ∈ X.
We will prove path_component_of X Tx x = component_of X Tx x.
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).
Set P to be the term path_component_of X Tx x.
Set C to be the term component_of X Tx x.
We prove the intermediate claim HCsubX: C ⊆ X.
Let y be given.
Assume Hy: y ∈ C.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃C0 : set, connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y0 ∈ C0) y Hy).
We prove the intermediate claim HopenP: open_in X Tx P.
An exact proof term for the current goal is (path_components_open X Tx Hlpc x Hx).
We prove the intermediate claim HPinTx: P ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx P HopenP).
We prove the intermediate claim HxP: x ∈ P.
An exact proof term for the current goal is (path_component_reflexive X Tx x HTx Hx).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (point_in_component X Tx x HTx Hx).
Apply set_ext to the current goal.
Let y be given.
Assume HyP: y ∈ P.
We will prove y ∈ C.
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 Hex: ∃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 = y.
An exact proof term for the current goal is (SepE2 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).
Apply Hex to the current goal.
Let p be given.
Assume Hp.
We prove the intermediate claim H01: 0 ∈ unit_interval ∧ 1 ∈ unit_interval.
An exact proof term for the current goal is zero_one_in_unit_interval.
We prove the intermediate claim H0I: 0 ∈ unit_interval.
An exact proof term for the current goal is (andEL (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
We prove the intermediate claim H1I: 1 ∈ unit_interval.
An exact proof term for the current goal is (andER (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
We prove the intermediate claim Htmp: ((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 = y.
An exact proof term for the current goal is 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 X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x) (apply_fun p 1 = y) Htmp).
We prove the intermediate claim Htmp2: (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) ∧ apply_fun p 0 = x.
An exact proof term for the current goal is (andEL ((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 = y) Htmp).
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 X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) Htmp2).
We prove the intermediate claim Hpfc: function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (andEL (function_on p unit_interval X ∧ continuous_map unit_interval unit_interval_topology X Tx p) (apply_fun p 0 = x) Htmp2).
We prove the intermediate claim Hpfun: function_on p unit_interval X.
An exact proof term for the current goal is (andEL (function_on p unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p) Hpfc).
We prove the intermediate claim Hpcont: continuous_map unit_interval unit_interval_topology X Tx p.
An exact proof term for the current goal is (andER (function_on p unit_interval X) (continuous_map unit_interval unit_interval_topology X Tx p) Hpfc).
Set Img to be the term image_of p unit_interval.
We prove the intermediate claim HimgConn: connected_space Img (subspace_topology X Tx Img).
An exact proof term for the current goal is (continuous_image_connected unit_interval unit_interval_topology X Tx p unit_interval_connected Hpcont).
We prove the intermediate claim HxImg: x ∈ Img.
We prove the intermediate claim Hpx: apply_fun p 0 ∈ Img.
An exact proof term for the current goal is (ReplI unit_interval (λt : set ⇒ apply_fun p t) 0 H0I).
rewrite the current goal using Hp0 (from right to left).
An exact proof term for the current goal is Hpx.
We prove the intermediate claim HyImg: y ∈ Img.
We prove the intermediate claim Hpy: apply_fun p 1 ∈ Img.
An exact proof term for the current goal is (ReplI unit_interval (λt : set ⇒ apply_fun p t) 1 H1I).
rewrite the current goal using Hp1 (from right to left).
An exact proof term for the current goal is Hpy.
We will prove y ∈ {y0 ∈ X|∃C0 : set, connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y0 ∈ C0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HyX.
We will prove ∃C0 : set, connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y ∈ C0.
We use Img to witness the existential quantifier.
We will prove connected_space Img (subspace_topology X Tx Img) ∧ x ∈ Img ∧ y ∈ Img.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HimgConn.
An exact proof term for the current goal is HxImg.
An exact proof term for the current goal is HyImg.
Let y be given.
Assume HyC: y ∈ C.
We will prove y ∈ P.
Set Tc to be the term subspace_topology X Tx C.
We prove the intermediate claim HCconn: connected_space C Tc.
An exact proof term for the current goal is (component_of_connected X Tx x HTx Hx).
We prove the intermediate claim HtopC: topology_on C Tc.
An exact proof term for the current goal is (andEL (topology_on C Tc) (¬ (∃U V : set, U ∈ Tc ∧ V ∈ Tc ∧ separation_of C U V)) HCconn).
Set A to be the term P ∩ C.
Set D to be the term C ∖ P.
We prove the intermediate claim HA_subC: A ⊆ C.
An exact proof term for the current goal is (binintersect_Subq_2 P C).
We prove the intermediate claim HAopen: open_in C Tc A.
We prove the intermediate claim Hiff: open_in C Tc A ↔ ∃V ∈ Tx, A = V ∩ C.
An exact proof term for the current goal is (open_in_subspace_iff X Tx C A HTx HCsubX HA_subC).
Apply (iffER (open_in C Tc A) (∃V ∈ Tx, A = V ∩ C) Hiff) to the current goal.
We will prove ∃V ∈ Tx, A = V ∩ C.
We use P to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HPinTx.
Use reflexivity.
Set UFam to be the term {W ∈ Tc|W ⊆ D}.
We prove the intermediate claim HUFsub: UFam ⊆ Tc.
Let W be given.
Assume HW: W ∈ UFam.
An exact proof term for the current goal is (SepE1 Tc (λW0 : set ⇒ W0 ⊆ D) W HW).
We prove the intermediate claim HUnionTc: ⋃ UFam ∈ Tc.
An exact proof term for the current goal is (topology_union_closed C Tc UFam HtopC HUFsub).
We prove the intermediate claim HUnionEq: ⋃ UFam = D.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ ⋃ UFam.
Apply (UnionE UFam z Hz) to the current goal.
Let W be given.
Assume HexW: z ∈ W ∧ W ∈ UFam.
We prove the intermediate claim HzW: z ∈ W.
An exact proof term for the current goal is (andEL (z ∈ W) (W ∈ UFam) HexW).
We prove the intermediate claim HWUF: W ∈ UFam.
An exact proof term for the current goal is (andER (z ∈ W) (W ∈ UFam) HexW).
We prove the intermediate claim HWsubD: W ⊆ D.
An exact proof term for the current goal is (SepE2 Tc (λW0 : set ⇒ W0 ⊆ D) W HWUF).
An exact proof term for the current goal is (HWsubD z HzW).
Let z be given.
Assume HzD: z ∈ D.
We prove the intermediate claim HzC: z ∈ C.
An exact proof term for the current goal is (setminusE1 C P z HzD).
We prove the intermediate claim HzNotP: z ∉ P.
An exact proof term for the current goal is (setminusE2 C P z HzD).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HCsubX z HzC).
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 ∧ z ∈ V ∧ V ⊆ X ∧ path_connected_space V (subspace_topology X Tx V).
An exact proof term for the current goal is (Hlpcprop z HzX X HXTx HzX).
Apply HexV to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ z ∈ V ∧ V ⊆ X ∧ path_connected_space V (subspace_topology X Tx V).
We prove the intermediate claim HVpre: ((V ∈ Tx ∧ z ∈ V) ∧ V ⊆ X).
An exact proof term for the current goal is (andEL ((V ∈ Tx ∧ z ∈ 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 ∧ z ∈ V) ∧ V ⊆ X) (path_connected_space V (subspace_topology X Tx V)) HV).
We prove the intermediate claim HVTx_z: V ∈ Tx ∧ z ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ z ∈ V) (V ⊆ X) HVpre).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (z ∈ V) HVTx_z).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (z ∈ V) HVTx_z).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ z ∈ V) (V ⊆ X) HVpre).
Set W to be the term V ∩ C.
We prove the intermediate claim HW_Tc: W ∈ Tc.
We will prove W ∈ {U ∈ 𝒫 C|∃V0 ∈ Tx, U = V0 ∩ C}.
Apply SepI to the current goal.
Apply PowerI to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 V C).
We will prove ∃V0 ∈ Tx, W = V0 ∩ C.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVTx.
Use reflexivity.
We prove the intermediate claim HzW: z ∈ W.
An exact proof term for the current goal is (binintersectI V C z HzV HzC).
We prove the intermediate claim HWsubD: W ⊆ D.
Let t be given.
Assume HtW: t ∈ W.
Apply (binintersectE V C t HtW) to the current goal.
Assume HtV: t ∈ V.
Assume HtC: t ∈ C.
We will prove t ∈ D.
We will prove t ∈ C ∖ P.
Apply setminusI to the current goal.
An exact proof term for the current goal is HtC.
Assume HtP: t ∈ P.
We prove the intermediate claim HzPc_t: z ∈ path_component_of X Tx t.
An exact proof term for the current goal is (subspace_path_connected_implies_in_path_component X Tx V t z HTx HVsubX HVpath HtV HzV).
We prove the intermediate claim HtX: t ∈ X.
An exact proof term for the current goal is (HCsubX t HtC).
We prove the intermediate claim HzPc_x: z ∈ path_component_of X Tx x.
An exact proof term for the current goal is (path_component_transitive_axiom X Tx x t z HTx Hx HtX HzX HtP HzPc_t).
An exact proof term for the current goal is (HzNotP HzPc_x).
We prove the intermediate claim HWUF: W ∈ UFam.
We will prove W ∈ {W0 ∈ Tc|W0 ⊆ D}.
Apply SepI to the current goal.
An exact proof term for the current goal is HW_Tc.
An exact proof term for the current goal is HWsubD.
An exact proof term for the current goal is (UnionI UFam z W HzW HWUF).
We prove the intermediate claim HD_Tc: D ∈ Tc.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionTc.
We prove the intermediate claim HDopen: open_in C Tc D.
An exact proof term for the current goal is (open_inI C Tc D HtopC HD_Tc).
We prove the intermediate claim HAeq: A = C ∖ D.
Apply set_ext to the current goal.
Let t be given.
Assume HtA: t ∈ A.
Apply (binintersectE P C t HtA) to the current goal.
Assume HtP: t ∈ P.
Assume HtC: t ∈ C.
We will prove t ∈ C ∖ D.
Apply setminusI to the current goal.
An exact proof term for the current goal is HtC.
Assume HtD: t ∈ D.
We prove the intermediate claim HtNotP: t ∉ P.
An exact proof term for the current goal is (setminusE2 C P t HtD).
An exact proof term for the current goal is (HtNotP HtP).
Let t be given.
Assume HtCD: t ∈ C ∖ D.
We prove the intermediate claim HtC: t ∈ C.
An exact proof term for the current goal is (setminusE1 C D t HtCD).
We prove the intermediate claim HtNotD: t ∉ D.
An exact proof term for the current goal is (setminusE2 C D t HtCD).
We prove the intermediate claim HtP: t ∈ P.
Apply (xm (t ∈ P)) to the current goal.
Assume HtP0: t ∈ P.
An exact proof term for the current goal is HtP0.
Assume HtNotP: t ∉ P.
Apply FalseE to the current goal.
Apply HtNotD to the current goal.
An exact proof term for the current goal is (setminusI C P t HtC HtNotP).
An exact proof term for the current goal is (binintersectI P C t HtP HtC).
We prove the intermediate claim HAclosed: closed_in C Tc A.
We prove the intermediate claim HDinTc: D ∈ Tc.
An exact proof term for the current goal is HD_Tc.
We prove the intermediate claim Hcl: closed_in C Tc (C ∖ D).
An exact proof term for the current goal is (closed_of_open_complement C Tc D HtopC HDinTc).
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is Hcl.
We prove the intermediate claim HnoClopen: ¬ (∃B : set, B ≠ Empty ∧ B ≠ C ∧ open_in C Tc B ∧ closed_in C Tc B).
An exact proof term for the current goal is (iffEL (connected_space C Tc) (¬ (∃B : set, B ≠ Empty ∧ B ≠ C ∧ open_in C Tc B ∧ closed_in C Tc B)) (connected_iff_no_nontrivial_clopen C Tc HtopC) HCconn).
We prove the intermediate claim HAne: A ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A x (binintersectI P C x HxP HxC)).
We prove the intermediate claim HAeqC: A = C.
Apply (xm (A = C)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hneq: A ≠ C.
Apply FalseE to the current goal.
Apply HnoClopen to the current goal.
We use A to witness the existential quantifier.
We will prove A ≠ Empty ∧ A ≠ C ∧ open_in C Tc A ∧ closed_in C Tc A.
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 HAne.
An exact proof term for the current goal is Hneq.
An exact proof term for the current goal is HAopen.
An exact proof term for the current goal is HAclosed.
We prove the intermediate claim HyA: y ∈ A.
rewrite the current goal using HAeqC (from left to right).
An exact proof term for the current goal is HyC.
Apply (binintersectE P C y HyA) to the current goal.
Assume HyP: y ∈ P.
Assume HyC0: y ∈ C.
An exact proof term for the current goal is HyP.
∎